Mercurial > repos > sybila > ebcsgen_pctl_parameter_synthesis

comparison ebcsgen_pctl_parameter_synthesis.py @ 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 3bb6c1e9252e
comparison
equal deleted inserted replaced
-1:000000000000 0:cf609f659b21
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='Parameter synthesis')
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 optional.add_argument('--region', type=str)
20
21 args = args_parser.parse_args()
22
23 if args.region:
24 region = args.region.replace("=", "<=")
25 else:
26 region = None
27
28 ts = load_TS_from_json(args.transition_file)
29
30 if len(ts.params) == 0:
31 raise InvalidInputError("Provided model is not parametrised - parameter synthesis cannot be executed.")
32
33 if "?" not in args.formula:
34 if not region:
35 params = set()
36 else:
37 params = {param.split("<=")[1] for param in region.split(",")}
38
39 undefined = set(ts.params) - params
40 if undefined:
41 raise InvalidInputError("Intervals undefined for parameters: {}.".format(", ".join(undefined)))
42
43 formula = PCTLparser().parse(args.formula)
44 if formula.success:
45 result = PCTL.parameter_synthesis(ts, formula, region)
46 f = open(args.output, "w")
47 f.write(result.decode("utf-8"))
48 f.close()
49 else:
50 raise FormulaParsingError(formula.data, args.formula)