diff --git a/doc/source/advanced_topics.rst b/doc/source/advanced_topics.rst index bc32885..62142be 100644 --- a/doc/source/advanced_topics.rst +++ b/doc/source/advanced_topics.rst @@ -12,6 +12,7 @@ This guide is a collection of examples meant to bridge the gap between the getti doc/engines doc/exploration doc/reward_models + doc/schedulers doc/shortest_paths doc/parametric_models doc/dfts \ No newline at end of file diff --git a/doc/source/doc/schedulers.rst b/doc/source/doc/schedulers.rst new file mode 100644 index 0000000..b60bdd1 --- /dev/null +++ b/doc/source/doc/schedulers.rst @@ -0,0 +1,60 @@ +*********************** +Working with Schedulers +*********************** + +In non-deterministic models the notion of a scheduler (or policy) is important. +The scheduler determines which action to take at each state. + +For a given reachability property, Storm can return the scheduler realizing the resulting probability. + +Examining Schedulers +==================== + +.. seealso:: `01-schedulers.py `_ + +As in :doc:`../getting_started`, we import some required modules and build a model from the example files:: + + >>> import stormpy + >>> import stormpy.core + >>> import stormpy.examples + >>> import stormpy.examples.files + + >>> path = stormpy.examples.files.prism_mdp_coin_2_2 + >>> formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" + >>> program = stormpy.parse_prism_program(path) + >>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + >>> model = stormpy.build_model(program, formulas) + +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: + >>> assert result.has_scheduler + >>> scheduler = result.scheduler + >>> assert scheduler.memoryless + >>> assert scheduler.deterministic + >>> print(scheduler) + ___________________________________________________________________ + Fully defined memoryless deterministic scheduler: + model state: choice(s) + 0 0 + 1 0 + 2 1 + 3 0 + -etc- + +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) + ... action = choice.get_deterministic_choice() + ... print("In state {} choose action {}".format(state, action)) + In state 0 choose action 0 + In state 1 choose action 0 + In state 2 choose action 1 + In state 3 choose action 0 + In state 4 choose action 0 + In state 5 choose action 0 + -etc- + diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 6a0b2bd..14a8069 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -15,15 +15,17 @@ def example_schedulers_01(): model = stormpy.build_model(program, formulas) initial_state = model.initial_states[0] assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0], extract_scheduler = True) + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler - print(result.scheduler) - assert result.scheduler.memoryless - assert result.scheduler.deterministic - - for i in range(0,model.nr_states): - print("In state {} choose action {}".format(i,result.scheduler.get_choice(i).get_deterministic_choice())) - + scheduler = result.scheduler + print(scheduler) + assert scheduler.memoryless + assert scheduler.deterministic + + for state in model.states: + choice = scheduler.get_choice(state) + action = choice.get_deterministic_choice() + print("In state {} choose action {}".format(state, action)) if __name__ == '__main__':