# HG changeset patch
# User sybila
# Date 1665067188 0
# Node ID 213df1fd884f96702b00747c1aeec0ac5a9d19c8
planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
diff -r 000000000000 -r 213df1fd884f ebcsgen_ctl_model_checking.py
--- /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)
diff -r 000000000000 -r 213df1fd884f ebcsgen_ctl_model_checking.xml
--- /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 @@
+
+ - explicit CTL model checking of transition system
+
+ macros.xml
+
+
+
+ sybila/ebcsgen:v@TOOL_VERSION@
+
+
+
+ python3 ${__tool_directory__}/ebcsgen_ctl_model_checking.py
+ --transition_file '$transition_file'
+ --formula '$formula'
+ --output '$output'
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff -r 000000000000 -r 213df1fd884f macros.xml
--- /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 @@
+
+ 2.0.3
+
+
+
+
+
+
+
+
diff -r 000000000000 -r 213df1fd884f test-data/simple.bcsl.ts
--- /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