Matthias Volk 8 years ago
parent
commit
ba028a8e44
  1. 8
      tests/core/test_modelchecking.py
  2. 8
      tests/storage/test_matrix.py

8
tests/core/test_modelchecking.py

@ -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

8
tests/storage/test_matrix.py

@ -1,6 +1,8 @@
import stormpy import stormpy
from helpers.helper import get_example_path from helpers.helper import get_example_path
import math
class TestMatrix: class TestMatrix:
def test_sparse_matrix(self): def test_sparse_matrix(self):
model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
@ -36,7 +38,7 @@ class TestMatrix:
# First model checking # First model checking
formulas = stormpy.parse_formulas("P=? [ F \"one\" ]") formulas = stormpy.parse_formulas("P=? [ F \"one\" ]")
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result == 0.16666666666666663
assert math.isclose(result, 0.16666666666666663)
# Change probabilities # Change probabilities
i = 0 i = 0
@ -51,7 +53,7 @@ class TestMatrix:
assert e.value() == 0.3 or e.value() == 0.7 or e.value() == 1 or e.value() == 0 assert e.value() == 0.3 or e.value() == 0.7 or e.value() == 1 or e.value() == 0
# Second model checking # Second model checking
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result == 0.06923076923076932
assert math.isclose(result, 0.06923076923076932)
# Change probabilities again # Change probabilities again
for state in stormpy.state.State(0, model): for state in stormpy.state.State(0, model):
@ -63,7 +65,7 @@ class TestMatrix:
transition.set_value(0.2) transition.set_value(0.2)
# Third model checking # Third model checking
result = stormpy.model_checking(model, formulas[0]) result = stormpy.model_checking(model, formulas[0])
assert result == 0.3555555555555556 or result == 0.3555555555555557
assert math.isclose(result, 0.3555555555555556)
def test_change_parametric_sparse_matrix_modelchecking(self): def test_change_parametric_sparse_matrix_modelchecking(self):
import stormpy.logic import stormpy.logic

Loading…
Cancel
Save