From 4ab6277e3f95984044eb51441e33743f5e4fc59d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 24 Oct 2018 17:50:26 +0200 Subject: [PATCH] Fixed some typos --- doc/source/doc/building_models.rst | 2 +- doc/source/doc/exploration.rst | 5 ++--- doc/source/doc/parametric_models.rst | 1 - doc/source/doc/shortest_paths.rst | 4 ++-- doc/source/getting_started.rst | 14 +++++++------- 5 files changed, 12 insertions(+), 14 deletions(-) diff --git a/doc/source/doc/building_models.rst b/doc/source/doc/building_models.rst index 690e491..02229b3 100644 --- a/doc/source/doc/building_models.rst +++ b/doc/source/doc/building_models.rst @@ -17,7 +17,7 @@ We use some standard examples:: >>> import stormpy.examples >>> import stormpy.examples.files -Storm supports the DRN format. +Storm supports the explicit DRN format. From this, models can be built directly:: >>> path = stormpy.examples.files.drn_ctmc_dft diff --git a/doc/source/doc/exploration.rst b/doc/source/doc/exploration.rst index 5285b2a..383d4f2 100644 --- a/doc/source/doc/exploration.rst +++ b/doc/source/doc/exploration.rst @@ -37,7 +37,7 @@ The iteration over the model is as before, but now, for every action, we can hav ... print("From state {} by action {}, with probability {}, go to state {}".format(state, action, transition.value(), transition.column)) -etc- -The output (omitted for brievety) contains sentences like: +The output (omitted for brievety) contains sentences like:: From state 1 by action 0, with probability 1.0, go to state 2 From state 1 by action 1, with probability 1.0, go to state 1 @@ -48,7 +48,7 @@ Internally, storm can hold hints to the origin of the actions, which may be help As the availability and the encoding of this data depends on the input model, we discuss these features in :doc:`highlevel_models`. -Storm currently supports deterministic rewards on states or actions. More information can be found in that :doc:`reward_models`. +Storm currently supports deterministic rewards on states or actions. More information can be found in :doc:`reward_models`. Reading POMDPs @@ -63,7 +63,6 @@ Internally, POMDPs extend MDPs. Thus, iterating over the MDP is done as before. >>> import stormpy.examples.files >>> program = stormpy.parse_prism_program(stormpy.examples.files.prism_pomdp_maze) >>> prop = "R=? [F \"goal\"]" - >>> properties = stormpy.parse_properties_for_prism_program(prop, program, None) >>> model = stormpy.build_model(program, properties) diff --git a/doc/source/doc/parametric_models.rst b/doc/source/doc/parametric_models.rst index c4376c4..d16b597 100644 --- a/doc/source/doc/parametric_models.rst +++ b/doc/source/doc/parametric_models.rst @@ -18,7 +18,6 @@ If the constants only influence the probabilities or rates, but not the topology >>> 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: diff --git a/doc/source/doc/shortest_paths.rst b/doc/source/doc/shortest_paths.rst index aca96fa..a727950 100644 --- a/doc/source/doc/shortest_paths.rst +++ b/doc/source/doc/shortest_paths.rst @@ -29,7 +29,7 @@ As in :doc:`../getting_started`, we import some required modules and build a mod >>> model = stormpy.build_model(prism_program) -We also import the `ShortestPathsGenerator`:: +We also import the ``ShortestPathsGenerator``:: >>> from stormpy.utility import ShortestPathsGenerator @@ -40,7 +40,7 @@ and choose a target state (by its ID) to which we want to compute the shortest p It is also possible to specify a set of target states (as a list, e.g., ``[8, 10, 11]``) or a label in the model if applicable (e.g., ``"observe0Greater1"``). For simplicity, we will stick to using a single state for now. -We initialize a `ShortestPathsGenerator` instance:: +We initialize a ``ShortestPathsGenerator`` instance:: >>> spg = ShortestPathsGenerator(model, state_id) diff --git a/doc/source/getting_started.rst b/doc/source/getting_started.rst index abf1c57..e35acc1 100644 --- a/doc/source/getting_started.rst +++ b/doc/source/getting_started.rst @@ -41,7 +41,7 @@ With this, we can now import the path of our prism file:: >>> path = stormpy.examples.files.prism_dtmc_die >>> prism_program = stormpy.parse_prism_program(path) -The `prism_program` can be translated into Markov chains:: +The ``prism_program`` can be translated into a Markov chain:: >>> model = stormpy.build_model(prism_program) >>> print("Number of states: {}".format(model.nr_states)) @@ -56,7 +56,7 @@ Moreover, initial states and deadlocks are indicated with a labelling function. >>> print("Labels: {}".format(model.labeling.get_labels())) Labels: ... -We will investigate ways to examine the model in more detail in :ref:`getting-started-investigating-the-model`. +We will investigate ways to examine the model in more detail later in :ref:`getting-started-investigating-the-model`. .. _getting-started-building-properties: @@ -65,7 +65,7 @@ Building properties .. seealso:: `02-getting-started.py `_ 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 2, one would formulate:: +To express that one is interested in the reachability of any state where the prism program variable ``s`` is 2, one would formulate:: P=? [F s=2] @@ -76,7 +76,7 @@ Stormpy can be used to parse this. As the variables in the property refer to a p Notice that properties is now a list of properties containing a single element. -However, if we build the model as before, then the appropriate information that the variable s=2 in some states is not present. +However, if we build the model as before, then the appropriate information that the variable ``s=2`` in some states is not present. In order to label the states accordingly, we should notify Storm upon building the model that we would like to preserve given properties. Storm will then add the labels accordingly:: @@ -85,7 +85,7 @@ Storm will then add the labels accordingly:: Labels in the model: ['(s = 2)', 'deadlock', 'init'] Model building however now behaves slightly different: Only the properties passed are preserved, which means that model building might skip parts of the model. -In particular, to check the probability of eventually reaching a state x where s=2, successor states of x are not relevant:: +In particular, to check the probability of eventually reaching a state ``x`` where ``s=2``, successor states of ``x`` are not relevant:: >>> print("Number of states: {}".format(model.nr_states)) Number of states: 8 @@ -94,7 +94,7 @@ If we consider another property, however, such as:: P=? [F s=7 & d=2] -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. +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: @@ -180,7 +180,7 @@ Thus:: ... assert len(state.actions) <= 1 -We can also check if a state is indeed an initial state. Notice that model.initial_states contains state ids, not states.:: +We can also check if a state is indeed an initial state. Notice that ``model.initial_states`` contains state ids, not states.:: >>> for state in model.states: ... if state.id in model.initial_states: