annotate ebcsgen_pctl_parameter_synthesis.py @ 0:f1b47d8bcbf9 draft

planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
author sybila
date Fri, 07 Oct 2022 12:35:23 +0000
parents
children 5668805ac1c2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
1 import argparse
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
2
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
3 from eBCSgen.Analysis.PCTL import PCTL
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
4 from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
5 from eBCSgen.Errors.InvalidInputError import InvalidInputError
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
6 from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
7 from eBCSgen.Parsing.ParsePCTLformula import PCTLparser
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
8
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
9
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
10 args_parser = argparse.ArgumentParser(description='Parameter synthesis')
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
11
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
12 args_parser._action_groups.pop()
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
13 required = args_parser.add_argument_group('required arguments')
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
14 optional = args_parser.add_argument_group('optional arguments')
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
15
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
16 required.add_argument('--transition_file', required=True)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
17 required.add_argument('--output', type=str, required=True)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
18 required.add_argument('--formula', type=str, required=True)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
19 optional.add_argument('--region', type=str)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
20
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
21 args = args_parser.parse_args()
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
22
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
23 if args.region:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
24 region = args.region.replace("=", "<=")
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
25 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
26 region = None
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
27
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
28 ts = load_TS_from_json(args.transition_file)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
29
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
30 if len(ts.params) == 0:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
31 raise InvalidInputError("Provided model is not parametrised - parameter synthesis cannot be executed.")
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
32
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
33 if "?" not in args.formula:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
34 if not region:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
35 params = set()
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
36 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
37 params = {param.split("<=")[1] for param in region.split(",")}
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
38
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
39 undefined = set(ts.params) - params
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
40 if undefined:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
41 raise InvalidInputError("Intervals undefined for parameters: {}.".format(", ".join(undefined)))
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
42
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
43 formula = PCTLparser().parse(args.formula)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
44 if formula.success:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
45 result = PCTL.parameter_synthesis(ts, formula, region)
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
46 f = open(args.output, "w")
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
47 f.write(result.decode("utf-8"))
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
48 f.close()
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
49 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
50 raise FormulaParsingError(formula.data, args.formula)