Mercurial > repos > sybila > ebcsgen_ctl_model_checking

annotate ebcsgen_ctl_model_checking.py @ 2:56c967442e3b draft default tip

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 4719a69f514aed27d90c7017f052463b0b43cbb0
author sybila
date Sat, 15 Oct 2022 09:19:23 +0000
parents a92e774c4cc9
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
1 import argparse
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
2
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
3 from eBCSgen.Analysis.CTL import CTL
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
4 from eBCSgen.Errors.FormulaParsingError import FormulaParsingError
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
5 from eBCSgen.Errors.InvalidInputError import InvalidInputError
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
6 from eBCSgen.Parsing.ParseBCSL import load_TS_from_json
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
7 from eBCSgen.Parsing.ParseCTLformula import CTLparser
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
8
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
9 args_parser = argparse.ArgumentParser(description='Model checking')
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
10
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
11 args_parser._action_groups.pop()
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
12 required = args_parser.add_argument_group('required arguments')
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
13
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
14 required.add_argument('--transition_file', required=True)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
15 required.add_argument('--output', type=str, required=True)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
16 required.add_argument('--formula', type=str, required=True)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
17
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
18 args = args_parser.parse_args()
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
19
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
20 ts = load_TS_from_json(args.transition_file)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
21
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
22 if len(ts.params) != 0:
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
23 raise InvalidInputError("Provided transition system is parametrised - model checking cannot be executed.")
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
24
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
25 formula = CTLparser().parse(args.formula)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
26 if formula.success:
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
27 result, states = CTL.model_checking(ts, formula)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
28 output = 'Result: {}\nNumber of satisfying states: {}'.format(result, len(states))
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
29 f = open(args.output, "w")
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
30 f.write(output)
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
31 f.close()
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
32 else:
a92e774c4cc9 planemo upload for repository https://github.com/sybila/galaxytools/tree/master/tools/ebcsgen commit ab45353a4e518f67057a1789aa527fb3bf1e74d5
sybila
parents:
diff changeset
33 raise FormulaParsingError(formula.data, args.formula)