1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
#!/usr/bin/env python3
from argparse import ArgumentParser, FileType
import stormpy
# as in https://github.com/moves-rwth/stormpy/blob/master/examples//parametric_models/02-parametric-models.py, but no idea why
import stormpy.info
if stormpy.info.storm_ratfunc_use_cln():
import pycarl.cln.formula
else:
import pycarl.gmp.formula
def main():
parser = ArgumentParser(description='Model Repair tool')
parser.add_argument('--program', '-p', type=FileType('r'), required=True,
help='Path to the PRISM program to check and repair')
parser.add_argument('--properties', '-f', type=FileType('r'), required=True,
help='Path to the properties to check')
args = parser.parse_args()
program = stormpy.parse_prism_program(args.program.name)
properties = args.properties.read()
properties = stormpy.parse_properties_for_prism_program(properties, program)
model = stormpy.build_parametric_model(program, properties)
print('Built a model with {} states and {} transitions'.format(
model.nr_states, model.nr_transitions))
params = model.collect_probability_parameters()
print('Parameter(s): ' + ', '.join([str(p) for p in params]))
for prop in properties:
print('Checking:', prop)
result = stormpy.model_checking(model, prop)
init = model.initial_states[0]
func = result.at(init)
collector = stormpy.ConstraintCollector(model)
print('Well-formed constraints:')
for formula in collector.wellformed_constraints:
print(formula.get_constraint())
print('Graph preserving constraints:')
for formula in collector.graph_preserving_constraints:
print(formula.get_constraint())
if __name__ == '__main__':
main()
|
