From 341bd544e3d1afd9281ac19de2b2274769b6f52d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 5 Apr 2019 11:47:10 +0200 Subject: [PATCH] Added tests for MAs: scheduler extraction and transformation to MDPs --- tests/core/test_transformation.py | 28 ++++++++++++++++++++--- tests/storage/test_scheduler.py | 37 ++++++++++++++++++++++++++++++- 2 files changed, 61 insertions(+), 4 deletions(-) diff --git a/tests/core/test_transformation.py b/tests/core/test_transformation.py index 803c57e..b1ffe99 100644 --- a/tests/core/test_transformation.py +++ b/tests/core/test_transformation.py @@ -6,6 +6,7 @@ import math class TestTransformation: + def test_transform_symbolic_dtmc_to_sparse(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) symbolic_model = stormpy.build_symbolic_model(program) @@ -36,10 +37,9 @@ class TestTransformation: assert symbolic_model.supports_parameters assert type(symbolic_model) is stormpy.SparseParametricDtmc - def test_transform_continuous_to_discrete_time_model(self): + def test_transform_continuous_to_discrete_time_model_ctmc(self): ctmc = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") - print(formulas) assert ctmc.nr_states == 16 assert ctmc.nr_transitions == 33 assert len(ctmc.initial_states) == 1 @@ -49,7 +49,6 @@ class TestTransformation: assert math.isclose(result.at(initial_state), 4.166666667) dtmc, dtmc_formulas = stormpy.transform_to_discrete_time_model(ctmc, formulas) - print(dtmc_formulas) assert dtmc.nr_states == 16 assert dtmc.nr_transitions == 33 assert len(dtmc.initial_states) == 1 @@ -57,3 +56,26 @@ class TestTransformation: assert initial_state == 1 result = stormpy.model_checking(dtmc, dtmc_formulas[0]) assert math.isclose(result.at(initial_state), 4.166666667) + + def test_transform_continuous_to_discrete_time_model_ma(self): + program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) + formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program) + ma = stormpy.build_model(program, formulas) + assert ma.nr_states == 5 + assert ma.nr_transitions == 8 + assert ma.model_type == stormpy.ModelType.MA + assert len(ma.initial_states) == 1 + initial_state = ma.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(ma, formulas[0]) + assert math.isclose(result.at(initial_state), 0.08333333333) + + mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) + assert mdp.nr_states == 5 + assert mdp.nr_transitions == 8 + assert mdp.model_type == stormpy.ModelType.MDP + assert len(mdp.initial_states) == 1 + initial_state = mdp.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(mdp, mdp_formulas[0]) + assert math.isclose(result.at(initial_state), 0.08333333333) diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index b1bbefe..c1ec7c8 100644 --- a/tests/storage/test_scheduler.py +++ b/tests/storage/test_scheduler.py @@ -1,7 +1,8 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path -import pytest + +import math class TestScheduler: @@ -28,3 +29,37 @@ class TestScheduler: action = choice.get_deterministic_choice() assert 0 <= action assert action < len(state.actions) + + def test_scheduler_ma_via_mdp(self): + program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) + formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program) + ma = stormpy.build_model(program, formulas) + assert ma.nr_states == 5 + assert ma.nr_transitions == 8 + assert ma.model_type == stormpy.ModelType.MA + + # Convert MA to MDP + mdp, mdp_formulas = stormpy.transform_to_discrete_time_model(ma, formulas) + assert mdp.nr_states == 5 + assert mdp.nr_transitions == 8 + assert mdp.model_type == stormpy.ModelType.MDP + assert len(mdp.initial_states) == 1 + initial_state = mdp.initial_states[0] + assert initial_state == 0 + + result = stormpy.model_checking(mdp, mdp_formulas[0], extract_scheduler=True) + assert math.isclose(result.at(initial_state), 0.08333333333) + assert result.has_scheduler + scheduler = result.scheduler + assert scheduler.memoryless + assert scheduler.memory_size == 1 + assert scheduler.deterministic + for state in mdp.states: + choice = scheduler.get_choice(state) + assert choice.defined + assert choice.deterministic + action = choice.get_deterministic_choice() + if state.id == 0: + assert action == 1 + else: + assert action == 0