diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index 3f2505b..fcb48ee 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -93,7 +93,7 @@ If we consider another property, however, such as:: then Storm is only skipping exploration of successors of the particular state y where s=7 and d=2. In this model, state y has a self-loop, so effectively, the whole model is explored. - +.. _getting-started-checking-properties: Checking properties ------------------------------------ .. seealso:: `03-getting-started.py `_ @@ -152,10 +152,21 @@ Before we obtain an instantiated model, we need to map parameters to values: We Checking parametric models ------------------------------------ -.. seealso:: ``05-getting-started.py`` +.. seealso:: `05-getting-started.py `_ + +It is also possible to check the parametric model directly, similar as before in :ref:` _getting-started-checking-properties`:: + >>> result = stormpy.model_checking(model, properties[0]) + >>> initial_state = model.initial_states[0] + >>> func = result.at(initial_state) +We collect the constraints ensuring that underlying model is well-formed and the graph structure does not change. + >>> collector = stormpy.ConstraintCollector(model) + >>> for formula in collector.wellformed_constraints: + ... print(formula) + >>> for formula in collector.graph_preserving_constraints: + ... print(formula) .. _getting-started-investigating-the-model: diff --git a/examples/05-getting-started.py b/examples/05-getting-started.py new file mode 100644 index 0000000..29403f6 --- /dev/null +++ b/examples/05-getting-started.py @@ -0,0 +1,48 @@ +import stormpy +import stormpy.core +import stormpy.info + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy._config as config + + +def example_getting_started_05(): + # Check support for parameters + if not config.storm_with_pars: + print("Support parameters is missing. Try building storm-pars.") + return + + import stormpy.pars + from pycarl.formula import FormulaType, Relation + if stormpy.info.storm_ratfunc_use_cln(): + import pycarl.cln.formula + else: + import pycarl.gmp.formula + + path = stormpy.examples.files.prism_pdtmc_die + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [F s=7 & d=2]" + properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + model = stormpy.build_parametric_model(prism_program, properties) + + initial_state = model.initial_states[0] + result = stormpy.model_checking(model, properties[0]) + print("Result: {}".format(result.at(initial_state))) + + 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__': + example_getting_started_05()