Browse Source

Formatted tests according to PEP

refactoring
Matthias Volk 8 years ago
parent
commit
e13df9b2ec
  1. 1
      tests/conftest.py
  2. 2
      tests/core/test_bisimulation.py
  3. 7
      tests/core/test_parse.py
  4. 2
      tests/dft/test_build.py
  5. 1
      tests/helpers/helper.py
  6. 2
      tests/pars/test_model_instantiator.py
  7. 16
      tests/pars/test_parametric.py
  8. 21
      tests/pars/test_pla.py
  9. 1
      tests/storage/test_labeling.py
  10. 12
      tests/storage/test_matrix.py
  11. 31
      tests/storage/test_state.py
  12. 1
      tests/utility/test_shortestpaths.py

1
tests/conftest.py

@ -1,3 +1,4 @@
import sys
import os
sys.path.append(os.path.join(os.path.dirname(__file__), 'helpers'))

2
tests/core/test_bisimulation.py

@ -1,10 +1,10 @@
import stormpy
import stormpy.logic
from helpers.helper import get_example_path
import math
import math
class TestBisimulation:
def test_bisimulation(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm"))

7
tests/core/test_parse.py

@ -23,7 +23,8 @@ class TestParse:
assert str(properties[0].raw_formula) == formula
def test_parse_explicit_dtmc(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
assert model.nr_states == 13
assert model.nr_transitions == 20
assert model.model_type == stormpy.ModelType.DTMC
@ -31,7 +32,8 @@ class TestParse:
assert type(model) is stormpy.SparseDtmc
def test_parse_explicit_mdp(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"),
get_example_path("mdp", "two_dice.lab"))
assert model.nr_states == 169
assert model.nr_transitions == 436
assert model.model_type == stormpy.ModelType.MDP
@ -45,4 +47,3 @@ class TestParse:
assert model.model_type == stormpy.ModelType.CTMC
assert not model.supports_parameters
assert type(model) is stormpy.SparseCtmc

2
tests/dft/test_build.py

@ -4,8 +4,8 @@ from helpers.helper import get_example_path
import math
class TestBuild:
class TestBuild:
def test_import(self):
import stormpy.dft

1
tests/helpers/helper.py

@ -2,6 +2,7 @@ import os
import stormpy
import stormpy.examples
import stormpy.examples.files
example_dir = stormpy.examples.files.testfile_dir

2
tests/pars/test_model_instantiator.py

@ -4,7 +4,7 @@ import stormpy.pars
from helpers.helper import get_example_path
class TestModel:
class TestModelInstantiator:
def test_instantiate_dtmc(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program)

16
tests/pars/test_parametric.py

@ -3,8 +3,8 @@ import stormpy.info
import stormpy.logic
from helpers.helper import get_example_path
class TestParametric:
class TestParametric:
def test_constraints_collector(self):
from pycarl.formula import FormulaType, Relation
if stormpy.info.storm_ratfunc_use_cln():
@ -26,3 +26,17 @@ class TestParametric:
assert formula.type == FormulaType.CONSTRAINT
constraint = formula.get_constraint()
assert constraint.relation == Relation.NEQ
def test_derivatives(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
prop = "P<=0.84 [F s=5 ]"
formulas = stormpy.parse_properties_for_prism_program(prop, program)
model = stormpy.build_parametric_model(program, formulas)
assert model.nr_states == 613
assert model.nr_transitions == 803
assert model.model_type == stormpy.ModelType.DTMC
assert model.has_parameters
parameters = model.collect_probability_parameters()
assert len(parameters) == 2
derivatives = stormpy.pars.gather_derivatives(model, list(parameters)[0])
assert len(derivatives) == 0

21
tests/pars/test_pla.py

@ -3,7 +3,8 @@ import stormpy.logic
import stormpy.pars
from helpers.helper import get_example_path
class TestModelChecking:
class TestPLA:
def test_pla(self):
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
prop = "P<=0.84 [F s=5 ]"
@ -20,23 +21,9 @@ class TestModelChecking:
result = checker.check_region(region)
assert result == stormpy.pars.RegionResult.ALLSAT
region = stormpy.pars.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters)
result = checker.check_region(region, stormpy.pars.RegionResultHypothesis.UNKNOWN, stormpy.pars.RegionResult.UNKNOWN, True)
result = checker.check_region(region, stormpy.pars.RegionResultHypothesis.UNKNOWN,
stormpy.pars.RegionResult.UNKNOWN, True)
assert result == stormpy.pars.RegionResult.EXISTSBOTH
region = stormpy.pars.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters)
result = checker.check_region(region)
assert result == stormpy.pars.RegionResult.ALLVIOLATED
def test_derivatives(self):
import pycarl
program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
prop = "P<=0.84 [F s=5 ]"
formulas = stormpy.parse_properties_for_prism_program(prop, program)
model = stormpy.build_parametric_model(program, formulas)
assert model.nr_states == 613
assert model.nr_transitions == 803
assert model.model_type == stormpy.ModelType.DTMC
assert model.has_parameters
parameters = model.collect_probability_parameters()
assert len(parameters) == 2
derivatives = stormpy.pars.gather_derivatives(model, list(parameters)[0])
assert len(derivatives) == 0

1
tests/storage/test_labeling.py

@ -2,6 +2,7 @@ import stormpy
import stormpy.logic
from helpers.helper import get_example_path
class TestLabeling:
def test_set_labeling(self):
program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))

12
tests/storage/test_matrix.py

@ -6,7 +6,8 @@ import math
class TestMatrix:
def test_sparse_matrix(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
assert type(matrix) is stormpy.storage.SparseMatrix
assert matrix.nr_rows == model.nr_states
@ -17,7 +18,8 @@ class TestMatrix:
assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6)
def test_backward_matrix(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
matrix = model.backward_transition_matrix
assert type(matrix) is stormpy.storage.SparseMatrix
assert matrix.nr_rows == model.nr_states
@ -28,7 +30,8 @@ class TestMatrix:
assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6)
def test_change_sparse_matrix(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
for e in matrix:
assert e.value() == 0.5 or e.value() == 0 or e.value() == 1
@ -43,7 +46,8 @@ class TestMatrix:
def test_change_sparse_matrix_modelchecking(self):
import stormpy.logic
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
matrix = model.transition_matrix
# Check matrix
for e in matrix:

31
tests/storage/test_state.py

@ -1,9 +1,11 @@
import stormpy
from helpers.helper import get_example_path
class TestState:
def test_states_dtmc(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
i = 0
states = model.states
assert len(states) == 13
@ -17,7 +19,8 @@ class TestState:
assert state.id == 5
def test_states_mdp(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"),
get_example_path("mdp", "two_dice.lab"))
i = 0
assert len(model.states) == 169
for state in model.states:
@ -31,8 +34,10 @@ class TestState:
assert state.id == 1
def test_labels_dtmc(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"], ["four", "done"], ["five", "done"], ["six", "done"]]
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
labelsOrig = [["init"], [], [], [], [], [], [], ["one", "done"], ["two", "done"], ["three", "done"],
["four", "done"], ["five", "done"], ["six", "done"]]
i = 0
for state in model.states:
labels = state.labels
@ -41,14 +46,16 @@ class TestState:
i += 1
def test_actions_dtmc(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
for state in model.states:
assert len(state.actions) == 1
for action in state.actions:
assert action.id == 0
def test_actions_mdp(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"),
get_example_path("mdp", "two_dice.lab"))
for state in model.states:
assert len(state.actions) == 1 or len(state.actions) == 2
for action in state.actions:
@ -61,11 +68,13 @@ class TestState:
(6, 2, 0.5), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
i = 0
for state in model.states:
for action in state.actions:
assert (state.id < 7 and len(action.transitions) == 2) or (state.id >= 7 and len(action.transitions) == 1)
assert (state.id < 7 and len(action.transitions) == 2) or (
state.id >= 7 and len(action.transitions) == 1)
for transition in action.transitions:
transition_orig = transitions_orig[i]
i += 1
@ -74,7 +83,8 @@ class TestState:
assert transition.value() == transition_orig[2]
def test_transitions_mdp(self):
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"), get_example_path("mdp", "two_dice.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("mdp", "two_dice.tra"),
get_example_path("mdp", "two_dice.lab"))
assert model.states[1].id == 1
for state in model.states:
i = 0
@ -91,7 +101,8 @@ class TestState:
(6, 2, 0.5), (6, 12, 0.5), (7, 7, 1), (8, 8, 1),
(9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1)
]
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab"))
model = stormpy.build_sparse_model_from_explicit(get_example_path("dtmc", "die.tra"),
get_example_path("dtmc", "die.lab"))
i = 0
for state in model.states:
for transition in model.transition_matrix.row_iter(state.id, state.id):

1
tests/utility/test_shortestpaths.py

@ -13,6 +13,7 @@ import math
class ModelWithKnownShortestPaths:
"""Knuth's die model with reference kSP methods"""
def __init__(self):
self.target_label = "one"

Loading…
Cancel
Save