--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ebcsgen_ctl_model_checking.py	Thu Oct 06 14:39:48 2022 +0000
@@ -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)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ebcsgen_ctl_model_checking.xml	Thu Oct 06 14:39:48 2022 +0000
@@ -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>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/macros.xml	Thu Oct 06 14:39:48 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/simple.bcsl.ts	Thu Oct 06 14:39:48 2022 +0000
@@ -0,0 +1,98 @@
+{
+    "nodes": {
+        "1": "(0, 0, 0, 0, 0, 1, 0, 0)",
+        "2": "(0, 0, 1, 0, 0, 0, 0, 0)",
+        "3": "(1, 0, 0, 0, 0, 0, 0, 0)",
+        "4": "(0, 0, 0, 1, 0, 0, 0, 0)",
+        "5": "(0, 0, 0, 0, 0, 0, 1, 0)",
+        "6": "(0, 0, 0, 0, 0, 0, 0, 1)",
+        "7": "(0, 0, 0, 0, 1, 0, 0, 0)",
+        "8": "(0, 1, 0, 0, 0, 0, 0, 0)"
+    },
+    "edges": [
+        {
+            "s": 8,
+            "t": 8,
+            "p": 1,
+            "label": "\u03b5"
+        },
+        {
+            "s": 3,
+            "t": 8,
+            "p": 1.0,
+            "label": "r2"
+        },
+        {
+            "s": 5,
+            "t": 6,
+            "p": 0.3333333333333333,
+            "label": "r2"
+        },
+        {
+            "s": 6,
+            "t": 6,
+            "p": 1,
+            "label": "\u03b5"
+        },
+        {
+            "s": 2,
+            "t": 3,
+            "p": 0.5,
+            "label": "r1_T"
+        },
+        {
+            "s": 7,
+            "t": 1,
+            "p": 0.5,
+            "label": "r2"
+        },
+        {
+            "s": 5,
+            "t": 2,
+            "p": 0.3333333333333333,
+            "label": "r1_S"
+        },
+        {
+            "s": 7,
+            "t": 3,
+            "p": 0.5,
+            "label": "r1_S"
+        },
+        {
+            "s": 4,
+            "t": 4,
+            "p": 1,
+            "label": "\u03b5"
+        },
+        {
+            "s": 1,
+            "t": 1,
+            "p": 1,
+            "label": "\u03b5"
+        },
+        {
+            "s": 5,
+            "t": 7,
+            "p": 0.3333333333333333,
+            "label": "r1_T"
+        },
+        {
+            "s": 2,
+            "t": 4,
+            "p": 0.5,
+            "label": "r2"
+        }
+    ],
+    "ordering": [
+        "P(S{a},T{a})::cell",
+        "P(S{a},T{a})::out",
+        "P(S{a},T{i})::cell",
+        "P(S{a},T{i})::out",
+        "P(S{i},T{a})::cell",
+        "P(S{i},T{a})::out",
+        "P(S{i},T{i})::cell",
+        "P(S{i},T{i})::out"
+    ],
+    "initial": 5,
+    "bound": 1
+}
\ No newline at end of file