Browse Source

Test (currently) unsupported jani property

refactoring
Matthias Volk 7 years ago
parent
commit
ddae1c8c80
  1. 13
      tests/core/test_modelchecking.py

13
tests/core/test_modelchecking.py

@ -30,6 +30,19 @@ class TestModelChecking:
result = stormpy.model_checking(model, formula) result = stormpy.model_checking(model, formula)
assert math.isclose(result.at(initial_state), 0.16666666666666663) assert math.isclose(result.at(initial_state), 0.16666666666666663)
def test_model_checking_jani_dtmc(self):
jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani"))
formula = properties["Expected number of coin flips"]
model = stormpy.build_model(jani_model, [formula])
assert model.nr_states == 13
assert model.nr_transitions == 20
assert len(model.initial_states) == 1
initial_state = model.initial_states[0]
assert initial_state == 0
# Unsupported formula yields None result
result = stormpy.model_checking(model, formula)
assert result is None
def test_model_checking_all_dtmc(self): def test_model_checking_all_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)

Loading…
Cancel
Save