summaryrefslogtreecommitdiff
path: root/Assignment2/src/run.py
diff options
context:
space:
mode:
authorCamil Staps2018-07-04 12:35:06 +0200
committerCamil Staps2018-07-04 12:35:06 +0200
commit7ea998e3ba942dcecf8a26b4ebf8c58711999bc9 (patch)
treea5e566ab225ac8757626c3d5e66d13d3ca5015af /Assignment2/src/run.py
parentImprove dockerfile (diff)
Add properties and simple program with stormpy bindings
Diffstat (limited to 'Assignment2/src/run.py')
-rwxr-xr-xAssignment2/src/run.py47
1 files changed, 47 insertions, 0 deletions
diff --git a/Assignment2/src/run.py b/Assignment2/src/run.py
new file mode 100755
index 0000000..94862bf
--- /dev/null
+++ b/Assignment2/src/run.py
@@ -0,0 +1,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()