Mercurial > repos > sybila > ebcsgen_pctl_parameter_synthesis

changeset 0:cf609f659b21 draft

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
author sybila
date Fri, 07 Oct 2022 12:37:22 +0000
parents
children f280183d1289
files ebcsgen_pctl_parameter_synthesis.py ebcsgen_pctl_parameter_synthesis.xml macros.xml test-data/parametrised.bcsl.ts
diffstat 4 files changed, 579 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ebcsgen_pctl_parameter_synthesis.py	Fri Oct 07 12:37:22 2022 +0000
@@ -0,0 +1,50 @@
+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='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)
+    f = open(args.output, "w")
+    f.write(result.decode("utf-8"))
+    f.close()
+else:
+    raise FormulaParsingError(formula.data, args.formula)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ebcsgen_pctl_parameter_synthesis.xml	Fri Oct 07 12:37:22 2022 +0000
@@ -0,0 +1,82 @@
+<tool id="eBCSgen_PCTL_parameter_synthesis" name="eBCSgen PCTL parameter synthesis" version="@TOOL_VERSION@_galaxy0">
+    <description>- PCTL parameter synthesis of given parametric 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_parameter_synthesis.py
+        --transition_file '$transition_file'
+        #if len($regions) > 0:
+        --output '$output_regions'
+        #else:
+        --output '$output_sample'
+        #end if
+        --formula '$formula'
+
+        #set parameters = ",".join([str($s.from) + "=" + str($s.param) + "=" + str($s.to) for $s in $regions])
+        #if $parameters:
+        --region '$parameters'
+        #end if
+    </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>
+
+        <repeat name="regions" title="Parameter intervals">
+            <param name="param" value="" type="text" label="Parameter name:">
+                <validator type="empty_field"/>
+            </param>
+            <param name="from" type="float" value="" label="Interval start:"/>
+            <param name="to" type="float" value="" label="Interval end:"/>
+        </repeat>
+    </inputs>
+
+    <outputs>
+        <data format="txt" name="output_regions">
+            <filter>"?" not in formula</filter>
+        </data>
+        <data format="storm.sample" name="output_sample">
+            <filter>"?" in formula</filter>
+        </data>
+    </outputs>
+
+    <tests>
+        <test>
+            <param name="transition_file" value="parametrised.bcsl.ts" ftype="bcsl.ts"/>
+            <param name="formula" value="P&lt;=0.2 [F P2(active{on})::cell &gt; 0]"/>
+            <repeat name="regions">
+                <param name="param" value="param_sig"/>
+                <param name="from" value="0.1"/>
+                <param name="to" value="0.6"/>
+            </repeat>
+            <repeat name="regions">
+                <param name="param" value="param_block"/>
+                <param name="from" value="0.05"/>
+                <param name="to" value="1.0"/>
+            </repeat>
+            <output name="output_regions" ftype="txt">
+                <assert_contents>
+                    <has_text text="Region results:"/>
+                </assert_contents>
+             </output>
+        </test>
+        <test>
+            <param name="transition_file" value="parametrised.bcsl.ts" ftype="bcsl.ts"/>
+            <param name="formula" value="P=? [F P2(active{on})::cell &gt; 0]"/>
+            <output name="output_sample" ftype="storm.sample">
+                <assert_contents>
+                    <has_text text="Result (initial states):"/>
+                </assert_contents>
+             </output>
+        </test>
+    </tests>
+
+</tool>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/macros.xml	Fri Oct 07 12:37:22 2022 +0000
@@ -0,0 +1,17 @@
+<macros>
+    <token name="@TOOL_VERSION@">2.0.3</token>
+
+    <xml name="creator">
+        <creator>
+            <person
+                givenName="Matej"
+                familyName="Troják"
+                url="https://github.com/xtrojak"
+                identifier="0000-0003-0841-2707" />
+            <organization
+                url="https://sybila.fi.muni.cz/"
+                email="sybila@fi.muni.cz"
+                name="SYBILA MUNI" />
+        </creator>
+    </xml>
+</macros>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/test-data/parametrised.bcsl.ts	Fri Oct 07 12:37:22 2022 +0000
@@ -0,0 +1,430 @@
+{
+    "bound": 1,
+    "parameters": [
+        "param_sig",
+        "param_block"
+    ],
+    "nodes": {
+        "1": "(0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0)",
+        "2": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 1)",
+        "3": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0, 1, 1, 0, 0, 0)",
+        "4": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0)",
+        "5": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0)",
+        "6": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1, 0, 0)",
+        "7": "(0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 0)",
+        "8": "(0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0)",
+        "9": "(0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1)",
+        "10": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 0)",
+        "11": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1, 0, 0)",
+        "12": "(0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0)",
+        "13": "(0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0)",
+        "14": "(0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0)",
+        "15": "(0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0)",
+        "16": "(0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0)",
+        "17": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0, 0)",
+        "18": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 1)",
+        "19": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0, 1, 0, 0, 0)",
+        "20": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0)",
+        "21": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0)",
+        "22": "(0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0)",
+        "23": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 0)",
+        "24": "(0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0)",
+        "25": "(0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0)",
+        "26": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 1, 0, 1, 0, 0, 0)",
+        "27": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 1)",
+        "28": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 0, 1, 0, 1, 0, 0, 0)",
+        "29": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0)",
+        "30": "(0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0)",
+        "31": "(0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0)",
+        "32": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0, 0, 0, 0)",
+        "33": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0)",
+        "34": "(0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 1, 0, 0, 0)",
+        "35": "(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0, 0, 0)"
+    },
+    "initial": 2,
+    "ordering": [
+        "P1(active{off}).P2(active{off})::cell",
+        "P1(active{off}).P2(active{on})::cell",
+        "block{a}.P1(active{off})::cell",
+        "sig{a}.P1(active{off})::cell",
+        "sig{i}.P1(active{off})::cell",
+        "P1(active{off})::cell",
+        "P1(active{on}).P2(active{off})::cell",
+        "P1(active{on}).P2(active{on})::cell",
+        "block{a}.P1(active{on})::cell",
+        "sig{a}.P1(active{on})::cell",
+        "sig{i}.P1(active{on})::cell",
+        "P1(active{on})::cell",
+        "P2(active{off})::cell",
+        "P2(active{on})::cell",
+        "block{a}::cell",
+        "block{a}::ext",
+        "block{i}::ext",
+        "sig{a}::cell",
+        "sig{a}::ext",
+        "sig{i}::cell",
+        "sig{i}::ext"
+    ],
+    "edges": [
+        {
+            "s": 10,
+            "p": "(1.0*param_block)/(1.0*param_block + 1.0*param_sig)",
+            "t": 13
+        },
+        {
+            "s": 10,
+            "p": "(1.0*param_sig)/(1.0*param_block + 1.0*param_sig)",
+            "t": 8
+        },
+        {
+            "s": 4,
+            "p": 0.6666666666666667,
+            "t": 26
+        },
+        {
+            "s": 2,
+            "p": 0.5294117647058824,
+            "t": 27
+        },
+        {
+            "s": 15,
+            "p": 0.35714285714285715,
+            "t": 5
+        },
+        {
+            "s": 27,
+            "p": 0.2727272727272727,
+            "t": 18
+        },
+        {
+            "s": 19,
+            "p": "(1.0*param_sig)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 33
+        },
+        {
+            "s": 5,
+            "p": 0.33333333333333337,
+            "t": 33
+        },
+        {
+            "s": 17,
+            "p": "(1.0*param_sig)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 32
+        },
+        {
+            "s": 5,
+            "p": 0.6666666666666667,
+            "t": 28
+        },
+        {
+            "s": 9,
+            "p": 1.0,
+            "t": 24
+        },
+        {
+            "s": 35,
+            "p": "(0.9)/(1.0*param_sig + 1.3)",
+            "t": 26
+        },
+        {
+            "s": 32,
+            "p": 1.0,
+            "t": 17
+        },
+        {
+            "s": 3,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 1.3)",
+            "t": 21
+        },
+        {
+            "s": 17,
+            "p": "(1.0*param_block)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 12
+        },
+        {
+            "s": 31,
+            "p": 0.3,
+            "t": 34
+        },
+        {
+            "s": 12,
+            "p": 1,
+            "t": 12
+        },
+        {
+            "s": 20,
+            "p": 0.39999999999999997,
+            "t": 35
+        },
+        {
+            "s": 6,
+            "p": "(1.0*param_block)/(1.0*param_block + 0.1)",
+            "t": 24
+        },
+        {
+            "s": 18,
+            "p": "(0.8)/(1.0*param_block + 0.8)",
+            "t": 6
+        },
+        {
+            "s": 19,
+            "p": "(1.0*param_block)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 16
+        },
+        {
+            "s": 18,
+            "p": "(1.0*param_block)/(1.0*param_block + 0.8)",
+            "t": 9
+        },
+        {
+            "s": 35,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 1.3)",
+            "t": 20
+        },
+        {
+            "s": 22,
+            "p": 0.6666666666666667,
+            "t": 26
+        },
+        {
+            "s": 19,
+            "p": "(0.4)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 25
+        },
+        {
+            "s": 25,
+            "p": 0.33333333333333337,
+            "t": 19
+        },
+        {
+            "s": 24,
+            "p": 1.0,
+            "t": 13
+        },
+        {
+            "s": 6,
+            "p": "(0.1)/(1.0*param_block + 0.1)",
+            "t": 10
+        },
+        {
+            "s": 23,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 0.15)",
+            "t": 15
+        },
+        {
+            "s": 28,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 0.55)",
+            "t": 5
+        },
+        {
+            "s": 8,
+            "p": 0.5454545454545454,
+            "t": 10
+        },
+        {
+            "s": 11,
+            "p": 0.4,
+            "t": 23
+        },
+        {
+            "s": 14,
+            "p": 0.5714285714285715,
+            "t": 22
+        },
+        {
+            "s": 8,
+            "p": 0.45454545454545453,
+            "t": 33
+        },
+        {
+            "s": 3,
+            "p": "(0.9)/(1.0*param_sig + 1.3)",
+            "t": 28
+        },
+        {
+            "s": 14,
+            "p": 0.14285714285714288,
+            "t": 25
+        },
+        {
+            "s": 30,
+            "p": 1.0,
+            "t": 17
+        },
+        {
+            "s": 29,
+            "p": 0.8181818181818181,
+            "t": 11
+        },
+        {
+            "s": 15,
+            "p": 0.4285714285714286,
+            "t": 23
+        },
+        {
+            "s": 22,
+            "p": 0.33333333333333337,
+            "t": 30
+        },
+        {
+            "s": 13,
+            "p": 1,
+            "t": 13
+        },
+        {
+            "s": 16,
+            "p": 1,
+            "t": 16
+        },
+        {
+            "s": 7,
+            "p": 0.25,
+            "t": 35
+        },
+        {
+            "s": 27,
+            "p": 0.7272727272727273,
+            "t": 11
+        },
+        {
+            "s": 35,
+            "p": "(0.4)/(1.0*param_sig + 1.3)",
+            "t": 7
+        },
+        {
+            "s": 34,
+            "p": "(0.9)/(1.0*param_sig + 0.9)",
+            "t": 23
+        },
+        {
+            "s": 14,
+            "p": 0.28571428571428575,
+            "t": 28
+        },
+        {
+            "s": 31,
+            "p": 0.45,
+            "t": 15
+        },
+        {
+            "s": 1,
+            "p": 0.33333333333333337,
+            "t": 7
+        },
+        {
+            "s": 33,
+            "p": 1.0,
+            "t": 19
+        },
+        {
+            "s": 21,
+            "p": 0.39999999999999997,
+            "t": 3
+        },
+        {
+            "s": 29,
+            "p": 0.18181818181818182,
+            "t": 34
+        },
+        {
+            "s": 1,
+            "p": 0.5000000000000001,
+            "t": 14
+        },
+        {
+            "s": 25,
+            "p": 0.6666666666666667,
+            "t": 30
+        },
+        {
+            "s": 26,
+            "p": "(0.4)/(1.0*param_sig + 0.55)",
+            "t": 22
+        },
+        {
+            "s": 26,
+            "p": "(0.15)/(1.0*param_sig + 0.55)",
+            "t": 17
+        },
+        {
+            "s": 28,
+            "p": "(0.15)/(1.0*param_sig + 0.55)",
+            "t": 19
+        },
+        {
+            "s": 4,
+            "p": 0.33333333333333337,
+            "t": 32
+        },
+        {
+            "s": 20,
+            "p": 0.6,
+            "t": 4
+        },
+        {
+            "s": 17,
+            "p": "(0.4)/(1.0*param_block + 1.0*param_sig + 0.4)",
+            "t": 30
+        },
+        {
+            "s": 26,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 0.55)",
+            "t": 4
+        },
+        {
+            "s": 3,
+            "p": "(0.4)/(1.0*param_sig + 1.3)",
+            "t": 1
+        },
+        {
+            "s": 15,
+            "p": 0.2142857142857143,
+            "t": 8
+        },
+        {
+            "s": 34,
+            "p": "(1.0*param_sig)/(1.0*param_sig + 0.9)",
+            "t": 31
+        },
+        {
+            "s": 2,
+            "p": 0.47058823529411764,
+            "t": 29
+        },
+        {
+            "s": 31,
+            "p": 0.25,
+            "t": 21
+        },
+        {
+            "s": 23,
+            "p": "(0.15)/(1.0*param_sig + 0.15)",
+            "t": 10
+        },
+        {
+            "s": 21,
+            "p": 0.6,
+            "t": 5
+        },
+        {
+            "s": 1,
+            "p": 0.16666666666666669,
+            "t": 3
+        },
+        {
+            "s": 7,
+            "p": 0.75,
+            "t": 22
+        },
+        {
+            "s": 11,
+            "p": 0.6,
+            "t": 6
+        },
+        {
+            "s": 28,
+            "p": "(0.4)/(1.0*param_sig + 0.55)",
+            "t": 14
+        }
+    ]
+}
\ No newline at end of file