Consistent use of literal blocks in doc

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)

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<doc/models/building_dtmcs:Labeling>`.
+The state labeling is created analogously to the previous example in :ref:`building DTMCs<doc/models/building_dtmcs:Labeling>`::
 
     >>> state_labeling = stormpy.storage.StateLabeling(4)
     >>> state_labels = {'empty', 'init', 'deadlock', 'full'}

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:

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