Fixed some typos

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

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)
 

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:

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)
 

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 <https://github.com/moves-rwth/stormpy/blob/master/examples/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: