From 4daa73372750292c1dca3bb944786822a8608870 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 1 May 2018 20:28:13 +0200 Subject: [PATCH] Moved documentation for parametric models into own file --- doc/source/advanced_topics.rst | 3 +- doc/source/doc/parametric_models.rst | 61 +++++++++++++++++++ doc/source/getting_started.rst | 49 +-------------- examples/04-getting-started.py | 37 ++++------- examples/06-getting-started.py | 26 -------- .../parametric_models/01-parametric-models.py | 41 +++++++++++++ .../02-parametric-models.py} | 4 +- 7 files changed, 119 insertions(+), 102 deletions(-) create mode 100644 doc/source/doc/parametric_models.rst delete mode 100644 examples/06-getting-started.py create mode 100644 examples/parametric_models/01-parametric-models.py rename examples/{05-getting-started.py => parametric_models/02-parametric-models.py} (95%) diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index 7c5d0c0..765149a 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -10,4 +10,5 @@ This guide is a collection of examples meant to bridge the gap between the getti doc/building_models doc/reward_models - doc/shortest_paths \ No newline at end of file + doc/shortest_paths + doc/parametric_models \ No newline at end of file diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst new file mode 100644 index 0000000..c4376c4 --- /dev/null +++ b/doc/source/doc/parametric_models.rst @@ -0,0 +1,61 @@ +***************** +Parametric Models +***************** + + + +Instantiating parametric models +=============================== +.. seealso:: `01-parametric-models.py `_ + +Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters. +If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:: + + >>> import stormpy + >>> import stormpy.examples + >>> import stormpy.examples.files + >>> path = stormpy.examples.files.prism_dtmc_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) + >>> parameters = model.collect_probability_parameters() + >>> for x in parameters: + ... print(x) + +In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator:: + + >>> import stormpy.pars + >>> instantiator = stormpy.pars.PDtmcInstantiator(model) + +Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:: + + >>> point = dict() + >>> for x in parameters: + ... print(x.name) + ... point[x] = 0.4 + >>> instantiated_model = instantiator.instantiate(point) + >>> result = stormpy.model_checking(instantiated_model, properties[0]) + +Initial states and labels are set as for the parameter-free case. + + +Checking parametric models +========================== +.. seealso:: `02-parametric-models.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) + diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index 1649cc6..947036a 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -126,58 +126,11 @@ A good way to get the result for the initial states is as follows:: >>> print(result.at(initial_state)) 0.5 -Instantiating parametric models ------------------------------------- -.. seealso:: `04-getting-started.py `_ - -Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters. -If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models:: - - >>> model = stormpy.build_parametric_model(prism_program, properties) - >>> parameters = model.collect_probability_parameters() - >>> for x in parameters: - ... print(x) - -In order to obtain a standard DTMC, MDP or other Markov model, we need to instantiate these models by means of a model instantiator:: - - >>> import stormpy.pars - >>> instantiator = stormpy.pars.PDtmcInstantiator(model) - -Before we obtain an instantiated model, we need to map parameters to values: We build such a dictionary as follows:: - - >>> point = dict() - >>> for x in parameters: - ... print(x.name) - ... point[x] = 0.4 - >>> instantiated_model = instantiator.instantiate(point) - >>> result = stormpy.model_checking(instantiated_model, properties[0]) - -Initial states and labels are set as for the parameter-free case. - - -Checking parametric models ------------------------------------- -.. 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: Investigating the model ------------------------------------- -.. seealso:: `06-getting-started.py `_ +.. seealso:: `04-getting-started.py `_ One powerful part of the Storm model checker is to quickly create the Markov chain from higher-order descriptions, as seen above:: diff --git a/examples/04-getting-started.py b/examples/04-getting-started.py index a5c0d60..e1fcd66 100644 --- a/examples/04-getting-started.py +++ b/examples/04-getting-started.py @@ -1,40 +1,27 @@ import stormpy import stormpy.core -import pycarl -import pycarl.core - import stormpy.examples import stormpy.examples.files -import stormpy._config as config - def example_getting_started_04(): - # Check support for parameters - if not config.storm_with_pars: - print("Support parameters is missing. Try building storm-pars.") - return - - import stormpy.pars - path = stormpy.examples.files.prism_pdtmc_die + path = stormpy.examples.files.prism_dtmc_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) - print("Model supports parameters: {}".format(model.supports_parameters)) - parameters = model.collect_probability_parameters() - assert len(parameters) == 2 - - instantiator = stormpy.pars.PDtmcInstantiator(model) - point = dict() - for x in parameters: - print(x.name) - point[x] = stormpy.RationalRF(0.4) - instantiated_model = instantiator.instantiate(point) - result = stormpy.model_checking(instantiated_model, properties[0]) - print(result) + model = stormpy.build_model(prism_program, properties) + + print(model.model_type) + + for state in model.states: + if state.id in model.initial_states: + print(state) + for action in state.actions: + for transition in action.transitions: + print("From state {}, with probability {}, go to state {}".format(state, transition.value(), + transition.column)) if __name__ == '__main__': diff --git a/examples/06-getting-started.py b/examples/06-getting-started.py deleted file mode 100644 index e8d1378..0000000 --- a/examples/06-getting-started.py +++ /dev/null @@ -1,26 +0,0 @@ -import stormpy -import stormpy.core - -import stormpy.examples -import stormpy.examples.files - -def example_getting_started_06(): - path = stormpy.examples.files.prism_dtmc_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_model(prism_program, properties) - - print(model.model_type) - - for state in model.states: - if state.id in model.initial_states: - print(state) - for action in state.actions: - for transition in action.transitions: - print("From state {}, with probability {}, go to state {}".format(state, transition.value(), transition.column)) - - -if __name__ == '__main__': - example_getting_started_06() \ No newline at end of file diff --git a/examples/parametric_models/01-parametric-models.py b/examples/parametric_models/01-parametric-models.py new file mode 100644 index 0000000..30c2d4e --- /dev/null +++ b/examples/parametric_models/01-parametric-models.py @@ -0,0 +1,41 @@ +import stormpy +import stormpy.core + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy._config as config + + +def example_parametric_models_01(): + # Check support for parameters + if not config.storm_with_pars: + print("Support parameters is missing. Try building storm-pars.") + return + + import stormpy.pars + 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) + print("Model supports parameters: {}".format(model.supports_parameters)) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + + instantiator = stormpy.pars.PDtmcInstantiator(model) + point = dict() + for x in parameters: + print(x.name) + point[x] = stormpy.RationalRF(0.4) + instantiated_model = instantiator.instantiate(point) + result = stormpy.model_checking(instantiated_model, properties[0]) + print(result) + + +if __name__ == '__main__': + example_parametric_models_01() diff --git a/examples/05-getting-started.py b/examples/parametric_models/02-parametric-models.py similarity index 95% rename from examples/05-getting-started.py rename to examples/parametric_models/02-parametric-models.py index 29403f6..d273c0b 100644 --- a/examples/05-getting-started.py +++ b/examples/parametric_models/02-parametric-models.py @@ -11,7 +11,7 @@ import stormpy.examples.files import stormpy._config as config -def example_getting_started_05(): +def example_parametric_models_02(): # Check support for parameters if not config.storm_with_pars: print("Support parameters is missing. Try building storm-pars.") @@ -45,4 +45,4 @@ def example_getting_started_05(): if __name__ == '__main__': - example_getting_started_05() + example_parametric_models_02()