From afddae71ebab15a70ba1b301ad1c822daf40c5e3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 17 Jan 2017 13:46:46 +0100 Subject: [PATCH] text about properties added --- doc/source/getting_started.rst | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index 655aa94..27d2d81 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -37,8 +37,22 @@ The `prism_program` can be translated into Markov chains:: print("Number of states: {}".format(model.nr_states)) -Building formulae +Building properties -------------------------- +Storm takes properties in the prism-property format. To express that one is interested in the reachability of any state where the prism program variable s is 7 and d is 2, one would formulate:: + + P=? [F s=7 & d=2] + +Stormpy can be used to parse this. As the variables in the property refer to a program, the program has to be passed as an additional parameter:: + + formula_str = "P=? [F s=7 & d=2]" + properties = parse_properties_for_prism_program(formula_str, prism_program) + +Notice that properties is now a list of properties containing a single element. + + + +