From e13df9b2ec273ed3fbf9b0867f8ab4e2cf4973c1 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 2 Aug 2017 18:04:00 +0200 Subject: [PATCH] Formatted tests according to PEP --- tests/conftest.py | 1 + tests/core/test_bisimulation.py | 2 +- tests/core/test_modelchecking.py | 4 +-- tests/core/test_parse.py | 13 +++++----- tests/dft/test_build.py | 2 +- tests/helpers/helper.py | 1 + tests/pars/test_model_instantiator.py | 2 +- tests/pars/test_parametric.py | 16 +++++++++++- tests/pars/test_pla.py | 21 +++------------- tests/storage/test_bitvector.py | 8 +++--- tests/storage/test_labeling.py | 5 ++-- tests/storage/test_matrix.py | 12 ++++++--- tests/storage/test_model.py | 12 ++++----- tests/storage/test_state.py | 35 ++++++++++++++++++--------- tests/utility/test_shortestpaths.py | 3 ++- 15 files changed, 79 insertions(+), 58 deletions(-) diff --git a/tests/conftest.py b/tests/conftest.py index 5e85fe6..9661c49 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -1,3 +1,4 @@ import sys import os + sys.path.append(os.path.join(os.path.dirname(__file__), 'helpers')) diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index a1c0178..f160fa9 100644 --- a/tests/core/test_bisimulation.py +++ b/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")) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 6195cf8..648b4eb 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -44,7 +44,7 @@ class TestModelChecking: func = result.at(initial_state) one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) assert func.denominator == one - #constraints_well_formed = result.constraints_well_formed + # constraints_well_formed = result.constraints_well_formed # for constraint in constraints_well_formed: # assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ # constraints_graph_preserving = result.constraints_graph_preserving @@ -74,7 +74,7 @@ class TestModelChecking: labelprop = stormpy.core.Property("cora", formulaPsi.raw_formula) result = stormpy.model_checking(model, labelprop) assert result.get_truth_values().number_of_set_bits() == 1 - + def test_model_checking_ctmc(self): model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) formulas = stormpy.parse_properties("T=? [ F \"failed\" ]") diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 0610c25..910311d 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -21,23 +21,25 @@ class TestParse: properties = stormpy.parse_properties(formula) assert len(properties) == 1 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 assert not model.supports_parameters 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 assert not model.supports_parameters assert type(model) is stormpy.SparseMdp - + def test_parse_drn_dtmc(self): model = stormpy.build_model_from_drn(get_example_path("ctmc", "dft.drn")) assert model.nr_states == 16 @@ -45,4 +47,3 @@ class TestParse: assert model.model_type == stormpy.ModelType.CTMC assert not model.supports_parameters assert type(model) is stormpy.SparseCtmc - diff --git a/tests/dft/test_build.py b/tests/dft/test_build.py index 93b6cf2..338f0be 100644 --- a/tests/dft/test_build.py +++ b/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 diff --git a/tests/helpers/helper.py b/tests/helpers/helper.py index 37a49f5..cde009a 100644 --- a/tests/helpers/helper.py +++ b/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 diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index 98d5dad..494a3df 100644 --- a/tests/pars/test_model_instantiator.py +++ b/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) diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 24bf5b9..dd221ef 100644 --- a/tests/pars/test_parametric.py +++ b/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 diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 9f0e5f1..7f1a86e 100644 --- a/tests/pars/test_pla.py +++ b/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 diff --git a/tests/storage/test_bitvector.py b/tests/storage/test_bitvector.py index adcfdac..2fb8d0d 100644 --- a/tests/storage/test_bitvector.py +++ b/tests/storage/test_bitvector.py @@ -6,7 +6,7 @@ class TestBitvector: bit = stormpy.BitVector() assert bit.size() == 0 assert bit.number_of_set_bits() == 0 - + def test_init_length(self): bit = stormpy.BitVector(10) assert bit.size() == 10 @@ -14,7 +14,7 @@ class TestBitvector: bit = stormpy.BitVector(5, True) assert bit.size() == 5 assert bit.number_of_set_bits() == 5 - + def test_init_vector(self): bit = stormpy.BitVector(5, [2, 3]) assert bit.size() == 5 @@ -24,14 +24,14 @@ class TestBitvector: assert bit.get(2) is True assert bit.get(3) is True assert bit.get(4) is False - + def test_init_bitvector(self): bit = stormpy.BitVector(7, [0, 6]) bit2 = stormpy.BitVector(bit) assert bit == bit2 assert bit2.get(0) is True assert bit2.get(6) is True - + def test_negate(self): bit = stormpy.BitVector(7, [0, 6]) bit2 = stormpy.BitVector(bit) diff --git a/tests/storage/test_labeling.py b/tests/storage/test_labeling.py index 190a53e..509cff1 100644 --- a/tests/storage/test_labeling.py +++ b/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")) @@ -18,7 +19,7 @@ class TestLabeling: states.set(3) labeling.set_states("tmp", states) assert labeling.has_state_label("tmp", 3) - + def test_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -32,7 +33,7 @@ class TestLabeling: assert "init" in labeling.get_labels_of_state(0) assert "one" in model.labels_state(7) assert "one" in labeling.get_labels_of_state(7) - + def test_label_parametric(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) diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 07d222a..3a29e8a 100644 --- a/tests/storage/test_matrix.py +++ b/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: diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 3d6b838..a70fa37 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -12,7 +12,7 @@ class TestModel: assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - + def test_build_dtmc_from_prism_program_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) prop = "P=? [F \"one\"]" @@ -23,7 +23,7 @@ class TestModel: assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - + def test_build_parametric_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) prop = "P=? [F s=5]" @@ -35,7 +35,7 @@ class TestModel: assert model.supports_parameters assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc - + def test_build_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -45,7 +45,7 @@ class TestModel: assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc - + def test_build_parametric_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) @@ -56,7 +56,7 @@ class TestModel: assert model.supports_parameters assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc - + def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -72,6 +72,6 @@ class TestModel: program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas) - initial_states = model.initial_states + initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states diff --git a/tests/storage/test_state.py b/tests/storage/test_state.py index 9b64ef4..b0d4571 100644 --- a/tests/storage/test_state.py +++ b/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: @@ -60,12 +67,14 @@ class TestState: (4, 8, 0.5), (4, 9, 0.5), (5, 10, 0.5), (5, 11, 0.5), (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 @@ -90,8 +100,9 @@ class TestState: (4, 8, 0.5), (4, 9, 0.5), (5, 10, 0.5), (5, 11, 0.5), (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): diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index c0c5411..e1751ec 100644 --- a/tests/utility/test_shortestpaths.py +++ b/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" @@ -24,7 +25,7 @@ class ModelWithKnownShortestPaths: self.model = stormpy.build_model(program, formulas) def probability(self, k): - return (1/2)**((2 * k) + 1) + return (1 / 2) ** ((2 * k) + 1) def state_set(self, k): return BitVector(self.model.nr_states, [0, 1, 3, 7])