annotate ebcsgen_pctl_parameter_synthesis.py @ 2:5668805ac1c2 draft default tip

planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
author sybila
date Sat, 15 Oct 2022 09:19:56 +0000
parents f1b47d8bcbf9
children
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
2
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
10 class FakeFile:
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
11 def __init__(self, content):
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
12 self.content = content.decode("utf-8")
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
13
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
14 def read(self):
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
15 return self.content
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
16
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
17
0
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
18 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
19
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
20 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
21 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
22 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
23
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
24 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
25 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
26 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
27 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
28
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
29 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
30
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
31 if args.region:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
32 region = args.region.replace("=", "<=")
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
33 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
34 region = None
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
35
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
36 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
37
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
38 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
39 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
40
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
41 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
42 if not region:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
43 params = set()
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
44 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
45 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
46
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
47 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
48 if undefined:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
49 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
50
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
51 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
52 if formula.success:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
53 result = PCTL.parameter_synthesis(ts, formula, region)
2
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
54 if "?" not in args.formula:
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
55 result = FakeFile(result)
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
56 df = PCTL.process_output(result)
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
57 df.to_csv(args.output, index=False)
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
58 else:
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
59 with open(args.output, "w") as f:
5668805ac1c2 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit 4719a69f514aed27d90c7017f052463b0b43cbb0
sybila
parents: 0
diff changeset
60 f.write(result.decode("utf-8"))
0
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
61 else:
f1b47d8bcbf9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit a7263af5f87e39dd0d3d29924e530c88d83a5ee6
sybila
parents:
diff changeset
62 raise FormulaParsingError(formula.data, args.formula)