Browse Source

Added tests for MAs: scheduler extraction and transformation to MDPs

refactoring
Matthias Volk 6 years ago
parent
commit
341bd544e3
  1. 28
      tests/core/test_transformation.py
  2. 37
      tests/storage/test_scheduler.py

28
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)

37
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
Loading…
Cancel
Save