Move Galaxy tools to the eBCSgen repository

Galaxy/tools/ebcsgen/.shed.yml

@@ -0,0 +1,57 @@
+owner: sybila
+remote_repository_url: "https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen"
+homepage_url: "https://github.com/sybila/eBCSgen"
+categories:
+  - Systems Biology
+repositories:
+  ebcsgen_generate_transition_system:
+    description: "Generate transition system of the given BCSL model."
+    include:
+      - ebcsgen_generate_ts.xml
+      - ebcsgen_generate_ts.py
+      - test-data/simple.bcsl.model
+      - macros.xml
+  ebcsgen_pctl_model_checking:
+    description: "Explicit PCTL model checking of given transition system."
+    include:
+      - ebcsgen_pctl_model_checking.xml
+      - ebcsgen_pctl_model_checking.py
+      - test-data/pctl_model_checking.bcsl.ts
+      - macros.xml
+  ebcsgen_simulation:
+    description: "Simulation of the given BCSL model."
+    include:
+      - ebcsgen_simulate.xml
+      - ebcsgen_simulate.py
+      - test-data/repressilator.bcsl.model
+      - test-data/simulation_determ.csv
+      - macros.xml
+  ebcsgen_ctl_model_checking:
+    description: "Explicit CTL model checking of given transition system."
+    include:
+      - ebcsgen_ctl_model_checking.xml
+      - ebcsgen_ctl_model_checking.py
+      - test-data/simple.bcsl.ts
+      - macros.xml
+  ebcsgen_pctl_parameter_synthesis:
+    description: "PCTL parameter synthesis of given parametric transition system."
+    include:
+      - ebcsgen_pctl_parameter_synthesis.xml
+      - ebcsgen_pctl_parameter_synthesis.py
+      - test-data/parametrised.bcsl.ts
+      - macros.xml
+  ebcsgen_sbml_export:
+    description: "Export given BCSL model to SBML with usage of SBML-multi package."
+    include:
+      - ebcsgen_sbml_export.xml
+      - ebcsgen_sbml_export.py
+      - test-data/simple.bcsl.model
+      - macros.xml
+  ebcsgen_static_analysis:
+    description: "Run static analysis techniques on given BCSL model."
+    include:
+      - ebcsgen_static_analysis.xml
+      - ebcsgen_static_analysis.py
+      - test-data/redundant.bcsl.model
+      - test-data/reduced.bcsl.model
+      - macros.xml

Galaxy/tools/ebcsgen/ebcsgen_ctl_model_checking.py

@@ -0,0 +1,33 @@
+import argparse
+
+from eBCSgen.Analysis.CTL import CTL
+from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
+from eBCSgen.Errors.InvalidInputError import InvalidInputError
+from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
+from eBCSgen.Parsing.ParseCTLformula import CTLparser
+
+args_parser = argparse.ArgumentParser(description='Model checking')
+
+args_parser._action_groups.pop()
+required = args_parser.add_argument_group('required arguments')
+
+required.add_argument('--transition_file', required=True)
+required.add_argument('--output', type=str, required=True)
+required.add_argument('--formula', type=str, required=True)
+
+args = args_parser.parse_args()
+
+ts = load_TS_from_json(args.transition_file)
+
+if len(ts.params) != 0:
+    raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.")
+
+formula = CTLparser().parse(args.formula)
+if formula.success:
+    result, states = CTL.model_checking(ts, formula)
+    output = 'Result: {}\nNumber of satisfying states: {}'.format(result, len(states))
+    f = open(args.output, "w")
+    f.write(output)
+    f.close()
+else:
+    raise FormulaParsingError(formula.data, args.formula)

Galaxy/tools/ebcsgen/ebcsgen_ctl_model_checking.xml

@@ -0,0 +1,42 @@
+<tool id="eBCSgen_CTL_model_checking" name="eBCSgen CTL model checking" version="@TOOL_VERSION@_galaxy0">
+    <description>- explicit CTL model checking of transition system</description>
+    <macros>
+        <import>macros.xml</import>
+    </macros>
+    <expand macro="creator"/>
+    <requirements>
+        <container type="docker">sybila/ebcsgen:v@TOOL_VERSION@</container>
+    </requirements>
+
+    <options sanitize="False"/>
+    <command>python3 ${__tool_directory__}/ebcsgen_ctl_model_checking.py
+        --transition_file '$transition_file'
+        --formula '$formula'
+        --output '$output'
+    </command>
+
+    <inputs>
+        <param format="bcsl.ts" name="transition_file" type="data" label="Computed Transition system"/>
+        <param name="formula" type="text" label="CTL formula">
+            <validator type="empty_field"/>
+        </param>
+    </inputs>
+
+    <outputs>
+        <data label="CTL model checking of ${on_string}" format="ctl.result" name="output"/>
+    </outputs>
+
+    <tests>
+        <test>
+            <param name="transition_file" value="simple.bcsl.ts" ftype="bcsl.ts"/>
+            <param name="formula" value="E(F([P(S{a},T{a})::cell &gt; 0]))"/>
+            <output name="output" ftype="ctl.result">
+                <assert_contents>
+                    <has_text text="Result: True"/>
+                    <has_text text="Number of satisfying states: 4"/>
+                </assert_contents>
+             </output>
+        </test>
+    </tests>
+
+</tool>

Galaxy/tools/ebcsgen/ebcsgen_generate_ts.py

@@ -0,0 +1,43 @@
+import argparse
+
+from eBCSgen.Errors.ModelParsingError import ModelParsingError
+from eBCSgen.Errors.UnspecifiedParsingError import UnspecifiedParsingError
+from eBCSgen.Parsing.ParseBCSL import Parser
+
+import numpy as np
+
+
+args_parser = argparse.ArgumentParser(description='Transition system generating')
+
+args_parser._action_groups.pop()
+required = args_parser.add_argument_group('required arguments')
+optional = args_parser.add_argument_group('optional arguments')
+
+required.add_argument('--model', type=str, required=True)
+required.add_argument('--output', type=str, required=True)
+required.add_argument('--direct', required=True)
+
+optional.add_argument('--max_time', type=float, default=np.inf)
+optional.add_argument('--max_size', type=float, default=np.inf)
+optional.add_argument('--bound', type=int, default=None)
+
+args = args_parser.parse_args()
+
+model_parser = Parser("model")
+model_str = open(args.model, "r").read()
+
+model = model_parser.parse(model_str)
+if model.success:
+    if eval(args.direct):
+        ts = model.data.generate_direct_transition_system(args.max_time,
+                                                          args.max_size,
+                                                          args.bound)
+        ts.change_to_vector_backend()
+    else:
+        vm = model.data.to_vector_model(args.bound)
+        ts = vm.generate_transition_system(None, args.max_time, args.max_size)
+    ts.save_to_json(args.output, model.data.params)
+else:
+    if "error" in model.data:
+        raise UnspecifiedParsingError(model.data["error"])
+    raise ModelParsingError(model.data, model_str)

Galaxy/tools/ebcsgen/ebcsgen_generate_ts.xml

@@ -0,0 +1,58 @@
+<tool id="eBCSgen_generate_transition_system" name="eBCSgen transition system generator" version="@TOOL_VERSION@_galaxy0">
+    <description>- generate transition system of the given model</description>
+    <macros>
+        <import>macros.xml</import>
+    </macros>
+    <expand macro="creator"/>
+    <requirements>
+        <container type="docker">sybila/ebcsgen:v@TOOL_VERSION@</container>
+    </requirements>
+
+    <command>python3 ${__tool_directory__}/ebcsgen_generate_ts.py
+        --model '$model'
+        --output '$output'
+        --direct '$network_free_choice'
+        #if $adv.bound != "":
+        --bound '$adv.bound'
+        #end if
+        #if $adv.max_time != "":
+        --max_time '$adv.max_time'
+        #end if
+        #if $adv.max_size != "":
+        --max_size '$adv.max_size'
+        #end if
+    </command>
+
+    <inputs>
+        <param format="bcsl.model" name="model" type="data" label="Model file" help="Provide a BCSL model file"/>
+        <param name="network_free_choice" type="select" label="Choose network-free approach:">
+            <option value="False" selected="true">Indirect</option>
+            <option value="True">Direct</option>
+        </param>
+        <section name="adv" title="Advanced Options" expanded="false">
+            <param name="bound" min="0" type="integer" value="" label="Bound [optional]" optional="true"/>
+            <param name="max_time" min="0" type="float" value=""
+                   label="Maximal computation time (in seconds) [optional]" optional="true"/>
+            <param name="max_size" min="1" type="integer" value="" label="Maximal TS size [optional]" optional="true"/>
+        </section>
+    </inputs>
+
+    <outputs>
+        <data label="Transition system of ${on_string}" format="bcsl.ts" name="output"/>
+    </outputs>
+
+    <tests>
+        <test>
+            <param name="model" value="simple.bcsl.model" ftype="bcsl.model"/>
+            <output name="output" ftype="bcsl.ts">
+                <assert_contents>
+                    <has_text text="nodes"/>
+                    <has_text text="edges"/>
+                    <has_text text="ordering"/>
+                    <has_text text="initial"/>
+                    <has_n_lines n="98" />
+                </assert_contents>
+            </output>
+        </test>
+    </tests>
+</tool>

Galaxy/tools/ebcsgen/ebcsgen_pctl_model_checking.py

@@ -0,0 +1,33 @@
+import argparse
+
+from eBCSgen.Analysis.PCTL import PCTL
+from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
+from eBCSgen.Errors.InvalidInputError import InvalidInputError
+from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
+from eBCSgen.Parsing.ParsePCTLformula import PCTLparser
+
+
+args_parser = argparse.ArgumentParser(description='Model checking')
+
+args_parser._action_groups.pop()
+required = args_parser.add_argument_group('required arguments')
+
+required.add_argument('--transition_file', required=True)
+required.add_argument('--output', type=str, required=True)
+required.add_argument('--formula', type=str, required=True)
+
+args = args_parser.parse_args()
+
+ts = load_TS_from_json(args.transition_file)
+
+if len(ts.params) != 0:
+    raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.")
+
+formula = PCTLparser().parse(args.formula)
+if formula.success:
+    result = PCTL.model_checking(ts, formula)
+    f = open(args.output, "w")
+    f.write(result.decode("utf-8"))
+    f.close()
+else:
+    raise FormulaParsingError(formula.data, args.formula)

Galaxy/tools/ebcsgen/ebcsgen_pctl_model_checking.xml

@@ -0,0 +1,41 @@
+<tool id="eBCSgen_PCTL_model_checking" name="eBCSgen PCTL model checking" version="@TOOL_VERSION@_galaxy0">
+    <description>- explicit PCTL model checking of transition system</description>
+    <macros>
+        <import>macros.xml</import>
+    </macros>
+    <expand macro="creator"/>
+    <requirements>
+        <container type="docker">sybila/ebcsgen:v@TOOL_VERSION@</container>
+    </requirements>
+
+    <options sanitize="False"/>
+    <command>python3 ${__tool_directory__}/ebcsgen_pctl_model_checking.py
+        --transition_file '$transition_file'
+        --output '$output'
+        --formula '$formula'
+    </command>
+
+    <inputs>
+        <param format="bcsl.ts" name="transition_file" type="data" label="Computed Transition system"/>
+        <param name="formula" type="text" label="PCTL formula">
+            <validator type="empty_field"/>
+        </param>
+    </inputs>
+
+    <outputs>
+        <data label="PCTL model checking of ${on_string}" format="storm.check" name="output"/>
+    </outputs>
+
+    <tests>
+        <test>
+            <param name="transition_file" value="pctl_model_checking.bcsl.ts" ftype="bcsl.ts"/>
+            <param name="formula" value="P &lt;= 0.5[F X()::rep=1]"/>
+            <output name="output" ftype="storm.check">
+                <assert_contents>
+                    <has_text text="Result (for initial states): false"/>
+                </assert_contents>
+             </output>
+        </test>
+    </tests>
+
+</tool>

Galaxy/tools/ebcsgen/ebcsgen_pctl_parameter_synthesis.py

@@ -0,0 +1,62 @@
+import argparse
+
+from eBCSgen.Analysis.PCTL import PCTL
+from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
+from eBCSgen.Errors.InvalidInputError import InvalidInputError
+from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
+from eBCSgen.Parsing.ParsePCTLformula import PCTLparser
+
+
+class FakeFile:
+    def __init__(self, content):
+        self.content = content.decode("utf-8")
+
+    def read(self):
+        return self.content
+
+
+args_parser = argparse.ArgumentParser(description='Parameter synthesis')
+
+args_parser._action_groups.pop()
+required = args_parser.add_argument_group('required arguments')
+optional = args_parser.add_argument_group('optional arguments')
+
+required.add_argument('--transition_file', required=True)
+required.add_argument('--output', type=str, required=True)
+required.add_argument('--formula', type=str, required=True)
+optional.add_argument('--region', type=str)
+
+args = args_parser.parse_args()
+
+if args.region:
+    region = args.region.replace("=", "<=")
+else:
+    region = None
+
+ts = load_TS_from_json(args.transition_file)
+
+if len(ts.params) == 0:
+    raise InvalidInputError("Provided model is not parametrised - parameter synthesis cannot be executed.")
+
+if "?" not in args.formula:
+    if not region:
+        params = set()
+    else:
+        params = {param.split("<=")[1] for param in region.split(",")}
+
+    undefined = set(ts.params) - params
+    if undefined:
+        raise InvalidInputError("Intervals undefined for parameters: {}.".format(", ".join(undefined)))
+
+formula = PCTLparser().parse(args.formula)
+if formula.success:
+    result = PCTL.parameter_synthesis(ts, formula, region)
+    if "?" not in args.formula:
+        result = FakeFile(result)
+        df = PCTL.process_output(result)
+        df.to_csv(args.output, index=False)
+    else:
+        with open(args.output, "w") as f:
+            f.write(result.decode("utf-8"))
+else:
+    raise FormulaParsingError(formula.data, args.formula)