diff options
| author | Camil Staps | 2018-07-04 12:35:06 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-04 12:35:06 +0200 |
| commit | 7ea998e3ba942dcecf8a26b4ebf8c58711999bc9 (patch) | |
| tree | a5e566ab225ac8757626c3d5e66d13d3ca5015af | |
| parent | Improve dockerfile (diff) | |
Add properties and simple program with stormpy bindings
| -rw-r--r-- | Assignment2/src/die.prism | 19 | ||||
| -rw-r--r-- | Assignment2/src/die.properties | 1 | ||||
| -rwxr-xr-x | Assignment2/src/run.py | 47 |
3 files changed, 67 insertions, 0 deletions
diff --git a/Assignment2/src/die.prism b/Assignment2/src/die.prism new file mode 100644 index 0000000..4c8d0de --- /dev/null +++ b/Assignment2/src/die.prism @@ -0,0 +1,19 @@ +dtmc + +const double p; + +module die + s : [0..7] init 0; + d : [0..6] init 0; + + [] s=0 -> p : (s'=1) + (1-p) : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> 1 : (s'=7); +endmodule + +label "done" = s=7; diff --git a/Assignment2/src/die.properties b/Assignment2/src/die.properties new file mode 100644 index 0000000..c53d02c --- /dev/null +++ b/Assignment2/src/die.properties @@ -0,0 +1 @@ +P=? [F s=7 & d=2] 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() |