Mercurial > repos > sybila > ebcsgen_pctl_model_checking
comparison ebcsgen_pctl_model_checking.py @ 0:ea5108514910 draft
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 |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:ea5108514910 |
---|---|
1 import argparse | |
2 | |
3 from eBCSgen.Analysis.PCTL import PCTL | |
4 from eBCSgen.Errors.FormulaParsingError import FormulaParsingError | |
5 from eBCSgen.Errors.InvalidInputError import InvalidInputError | |
6 from eBCSgen.Parsing.ParseBCSL import load_TS_from_json | |
7 from eBCSgen.Parsing.ParsePCTLformula import PCTLparser | |
8 | |
9 | |
10 args_parser = argparse.ArgumentParser(description='Model checking') | |
11 | |
12 args_parser._action_groups.pop() | |
13 required = args_parser.add_argument_group('required arguments') | |
14 optional = args_parser.add_argument_group('optional arguments') | |
15 | |
16 required.add_argument('--transition_file', required=True) | |
17 required.add_argument('--output', type=str, required=True) | |
18 required.add_argument('--formula', type=str, required=True) | |
19 | |
20 args = args_parser.parse_args() | |
21 | |
22 ts = load_TS_from_json(args.transition_file) | |
23 | |
24 if len(ts.params) != 0: | |
25 raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.") | |
26 | |
27 formula = PCTLparser().parse(args.formula) | |
28 if formula.success: | |
29 result = PCTL.model_checking(ts, formula, storm_local=True) | |
30 f = open(args.output, "w") | |
31 f.write(result.decode("utf-8")) | |
32 f.close() | |
33 else: | |
34 raise FormulaParsingError(formula.data, args.formula) |