From 0595ee1d64d3ebef4444c8a2cb9590eea253b23b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Apr 2019 11:51:08 +0200 Subject: [PATCH] Added documentation for MA scheduler extraction --- doc/source/doc/schedulers.rst | 43 ++++++++++++++++++++++++++-- examples/schedulers/01-schedulers.py | 1 - examples/schedulers/02-schedulers.py | 37 ++++++++++++++++++++++++ lib/stormpy/examples/files.py | 2 ++ 4 files changed, 80 insertions(+), 3 deletions(-) create mode 100644 examples/schedulers/02-schedulers.py diff --git a/doc/source/doc/schedulers.rst b/doc/source/doc/schedulers.rst index b60bdd1..00b03bb 100644 --- a/doc/source/doc/schedulers.rst +++ b/doc/source/doc/schedulers.rst @@ -7,8 +7,8 @@ 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 -==================== +Examining Schedulers for MDPs +============================= .. seealso:: `01-schedulers.py `_ @@ -30,6 +30,7 @@ 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 @@ -58,3 +59,41 @@ To get the information which action the scheduler chooses in which state, we can In state 5 choose action 0 -etc- + +Examining Schedulers for Markov automata +======================================== + +.. seealso:: `02-schedulers.py `_ + +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: + + >>> path = stormpy.examples.files.prism_ma_simple + >>> formula_str = "Tmin=? [ F s=4 ]" + + >>> program = stormpy.parse_prism_program(path, False, True) + >>> formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + >>> 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. + + >>> 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: + + >>> result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) + >>> scheduler = result.scheduler + >>> print(scheduler) + ___________________________________________________________________ + Fully defined memoryless deterministic scheduler: + model state: choice(s) + 0 1 + 1 0 + 2 0 + 3 0 + 4 0 + -etc- diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 14a8069..3cc40bc 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -7,7 +7,6 @@ import stormpy.examples.files def example_schedulers_01(): path = stormpy.examples.files.prism_mdp_coin_2_2 - formula_str = "Pmin=? [F \"finished\" & \"all_coins_equal_1\"]" program = stormpy.parse_prism_program(path) diff --git a/examples/schedulers/02-schedulers.py b/examples/schedulers/02-schedulers.py new file mode 100644 index 0000000..9ab79a7 --- /dev/null +++ b/examples/schedulers/02-schedulers.py @@ -0,0 +1,37 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + + +def example_schedulers_02(): + path = stormpy.examples.files.prism_ma_simple + formula_str = "Tmin=? [ F s=4 ]" + + program = stormpy.parse_prism_program(path, False, True) + formulas = stormpy.parse_properties_for_prism_program(formula_str, program) + ma = stormpy.build_model(program, formulas) + assert ma.model_type == stormpy.ModelType.MA + + # Convert MA to MDP + mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) + assert mdp.model_type == stormpy.ModelType.MDP + initial_state = mdp.initial_states[0] + assert initial_state == 0 + + result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) + assert result.has_scheduler + scheduler = result.scheduler + print(scheduler) + assert scheduler.memoryless + assert scheduler.deterministic + + for state in mdp.states: + choice = scheduler.get_choice(state) + action = choice.get_deterministic_choice() + print("In state {} choose action {}".format(state, action)) + + +if __name__ == '__main__': + example_schedulers_02() diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 5e7a447..48a51e5 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -19,6 +19,8 @@ prism_pdtmc_die = _path("pdtmc", "parametric_die.pm") """Knuth Yao Die -- 2 unfair coins Example""" prism_dtmc_brp = _path("dtmc", "brp-16-2.pm") """Bounded Retransmission Protocol""" +prism_ma_simple = _path("ma", "simple.ma") +"""Prism file for a simple Markov automaton""" drn_ctmc_dft = _path("ctmc", "dft.drn") """DRN format for a CTMC from a DFT""" drn_pdtmc_die = _path("pdtmc", "die.drn")