Mercurial > repos > sybila > ebcsgen_pctl_model_checking

annotate ebcsgen_pctl_model_checking.py @ 0:ea5108514910 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 d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
author sybila
date Fri, 09 Sep 2022 17:04:25 +0000
parents
children 141b9c2bc816
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
1 import argparse
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
2
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
3 from eBCSgen.Analysis.PCTL import PCTL
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
4 from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
5 from eBCSgen.Errors.InvalidInputError import InvalidInputError
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
6 from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
7 from eBCSgen.Parsing.ParsePCTLformula import PCTLparser
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
8
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
9
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
10 args_parser = argparse.ArgumentParser(description='Model checking')
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
11
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
12 args_parser._action_groups.pop()
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
13 required = args_parser.add_argument_group('required arguments')
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
14 optional = args_parser.add_argument_group('optional arguments')
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
15
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
16 required.add_argument('--transition_file', required=True)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
17 required.add_argument('--output', type=str, required=True)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
18 required.add_argument('--formula', type=str, required=True)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
19
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
20 args = args_parser.parse_args()
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
21
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
22 ts = load_TS_from_json(args.transition_file)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
23
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
24 if len(ts.params) != 0:
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
25 raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.")
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
26
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
27 formula = PCTLparser().parse(args.formula)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
28 if formula.success:
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
29 result = PCTL.model_checking(ts, formula, storm_local=True)
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
30 f = open(args.output, "w")
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
31 f.write(result.decode("utf-8"))
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
32 f.close()
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
33 else:
ea5108514910 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit d80d8e9710cba50aab3e6a1e10a527d26fc7e72b
sybila
parents:
diff changeset
34 raise FormulaParsingError(formula.data, args.formula)