|
@ -2,6 +2,8 @@ import stormpy |
|
|
import stormpy.logic |
|
|
import stormpy.logic |
|
|
from helpers.helper import get_example_path |
|
|
from helpers.helper import get_example_path |
|
|
|
|
|
|
|
|
|
|
|
import math |
|
|
|
|
|
|
|
|
class TestModelChecking: |
|
|
class TestModelChecking: |
|
|
def test_model_checking_dtmc(self): |
|
|
def test_model_checking_dtmc(self): |
|
|
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) |
|
|
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) |
|
@ -10,7 +12,7 @@ class TestModelChecking: |
|
|
assert model.nr_states == 13 |
|
|
assert model.nr_states == 13 |
|
|
assert model.nr_transitions == 20 |
|
|
assert model.nr_transitions == 20 |
|
|
result = stormpy.model_checking(model, formulas[0]) |
|
|
result = stormpy.model_checking(model, formulas[0]) |
|
|
assert result == 0.16666666666666663 |
|
|
|
|
|
|
|
|
assert math.isclose(result, 0.16666666666666663) |
|
|
|
|
|
|
|
|
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")) |
|
@ -19,8 +21,8 @@ class TestModelChecking: |
|
|
assert model.nr_states == 13 |
|
|
assert model.nr_states == 13 |
|
|
assert model.nr_transitions == 20 |
|
|
assert model.nr_transitions == 20 |
|
|
results = stormpy.model_checking_all(model, formulas[0]) |
|
|
results = stormpy.model_checking_all(model, formulas[0]) |
|
|
results_orig = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] |
|
|
|
|
|
assert results == results_orig |
|
|
|
|
|
|
|
|
reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] |
|
|
|
|
|
assert all(map(math.isclose, results, reference)) |
|
|
|
|
|
|
|
|
def test_parametric_state_elimination(self): |
|
|
def test_parametric_state_elimination(self): |
|
|
import pycarl |
|
|
import pycarl |
|
|