diff --git a/doc/source/doc/building_models.rst b/doc/source/doc/building_models.rst index 02229b3..9a8c052 100644 --- a/doc/source/doc/building_models.rst +++ b/doc/source/doc/building_models.rst @@ -33,7 +33,7 @@ And the same for parametric models:: ModelType.DTMC Another option are JANI descriptions. These are another high-level description format. -Building models from JANI is done in two steps. First the Jani-description is parsed, and then the model is built from this description. +Building models from JANI is done in two steps. First the Jani-description is parsed, and then the model is built from this description:: >>> path = stormpy.examples.files.jani_dtmc_die >>> jani_program, properties = stormpy.parse_jani_model(path) diff --git a/doc/source/doc/models/building_ctmcs.rst b/doc/source/doc/models/building_ctmcs.rst index 97fa418..ed0dc06 100644 --- a/doc/source/doc/models/building_ctmcs.rst +++ b/doc/source/doc/models/building_ctmcs.rst @@ -28,7 +28,9 @@ First, we import Stormpy:: Transition Matrix ===================== -In this example, we build the transition matrix using a numpy array:: +In this example, we build the transition matrix using a numpy array + + >>> import numpy as np @@ -56,7 +58,7 @@ The following function call returns a sparse matrix with default row groups:: Labeling ================ -The state labeling is created analogously to the previous example in :ref:`building DTMCs`. +The state labeling is created analogously to the previous example in :ref:`building DTMCs`:: >>> state_labeling = stormpy.storage.StateLabeling(4) >>> state_labels = {'empty', 'init', 'deadlock', 'full'} diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst index 870284c..f200e17 100644 --- a/doc/source/doc/parametric_models.rst +++ b/doc/source/doc/parametric_models.rst @@ -50,7 +50,7 @@ It is also possible to check the parametric model directly, similar as before in >>> 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. +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: diff --git a/doc/source/doc/schedulers.rst b/doc/source/doc/schedulers.rst index a06fdcb..9f147b4 100644 --- a/doc/source/doc/schedulers.rst +++ b/doc/source/doc/schedulers.rst @@ -25,11 +25,11 @@ As in :doc:`../getting_started`, we import some required modules and build a mod >>> formulas = stormpy.parse_properties(formula_str, program) >>> model = stormpy.build_model(program, formulas) -Next we check the model and make sure to extract the scheduler: +Next we check the model and make sure to extract the scheduler:: >>> result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) -The result then contains the scheduler we want: +The result then contains the scheduler we want:: >>> assert result.has_scheduler >>> scheduler = result.scheduler @@ -45,7 +45,7 @@ The result then contains the scheduler we want: 3 0 -etc- -To get the information which action the scheduler chooses in which state, we can simply iterate over the states: +To get the information which action the scheduler chooses in which state, we can simply iterate over the states:: >>> for state in model.states: ... choice = scheduler.get_choice(state) @@ -68,7 +68,7 @@ Examining Schedulers for Markov automata Currently there is no support yet for scheduler extraction on MAs. However, if the timing information is not relevant for the property, we can circumvent this lack by first transforming the MA to an MDP. -We build the model as before: +We build the model as before:: >>> path = stormpy.examples.files.prism_ma_simple >>> formula_str = "Tmin=? [ F s=4 ]" @@ -78,12 +78,12 @@ We build the model as before: >>> ma = stormpy.build_model(program, formulas) Next we transform the continuous-time model into a discrete-time model. -Note that all timing information is lost at this point. +Note that all timing information is lost at this point:: >>> mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) >>> assert mdp.model_type == stormpy.ModelType.MDP -After the transformation we have obtained an MDP where we can extract the scheduler as shown before: +After the transformation we have obtained an MDP where we can extract the scheduler as shown before:: >>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) >>> scheduler = result.scheduler