diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index 3776f54..ae69462 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -8,13 +8,13 @@ class TestBisimulation: assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC prop = "P=? [F \"observe0Greater1\"]" - formulas = stormpy.parse_formulas_for_prism_program(prop, program) - model = stormpy.build_model_from_prism_program(program, formulas) + properties = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_model(program, properties) assert model.nr_states == 7403 assert model.nr_transitions == 13041 assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters - model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) + model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 64 assert model_bisim.nr_transitions == 104 assert model_bisim.model_type == stormpy.ModelType.DTMC @@ -26,13 +26,13 @@ class TestBisimulation: assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants prop = "P=? [F \"observe0Greater1\"]" - formulas = stormpy.parse_formulas_for_prism_program(prop, program) - model = stormpy.build_parametric_model_from_prism_program(program, formulas) + properties = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, properties) assert model.nr_states == 1367 assert model.nr_transitions == 2027 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters - model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) + model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 80 assert model_bisim.nr_transitions == 120 assert model_bisim.model_type == stormpy.ModelType.DTMC diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 68c6347..814d985 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -7,8 +7,8 @@ import math class TestModelChecking: def test_model_checking_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 assert len(model.initial_states) == 1 @@ -19,8 +19,8 @@ class TestModelChecking: def test_model_checking_all_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 result = stormpy.model_checking(model, formulas[0]) @@ -33,8 +33,8 @@ class TestModelChecking: import pycarl.formula program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) prop = "P=? [F s=5]" - formulas = stormpy.parse_formulas_for_prism_program(prop, program) - model = stormpy.build_parametric_model_from_prism_program(program, formulas) + 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 @@ -52,9 +52,9 @@ class TestModelChecking: def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulaPhi = stormpy.parse_formulas("true")[0] - formulaPsi = stormpy.parse_formulas("\"six\"")[0] - model = stormpy.build_model(program, formulaPsi) + formulaPhi = stormpy.parse_properties("true")[0] + formulaPsi = stormpy.parse_properties("\"six\"")[0] + model = stormpy.build_model(program, [formulaPsi]) phiResult = stormpy.model_checking(model, formulaPhi) phiStates = phiResult.get_truth_values() assert phiStates.number_of_set_bits() == model.nr_states diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 83aff42..56e6bc6 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -10,10 +10,10 @@ class TestParse: assert not program.has_undefined_constants def test_parse_formula(self): - prop = "P=? [F \"one\"]" - formulas = stormpy.parse_formulas(prop) - assert len(formulas) == 1 - assert str(formulas[0]) == prop + formula = "P=? [F \"one\"]" + properties = stormpy.parse_properties(formula) + assert len(properties) == 1 + assert str(properties[0].raw_formula) == formula def test_parse_explicit_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 1bb697c..ab074d2 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -5,45 +5,45 @@ import stormpy.logic class TestFormulas: def test_probability_formula(self): - prop = "P=? [F \"one\"]" - formulas = stormpy.parse_formulas(prop) - formula = formulas[0] + formula_str = "P=? [F \"one\"]" + properties = stormpy.parse_properties(formula_str) + formula = properties[0].raw_formula assert type(formula) == stormpy.logic.ProbabilityOperator - assert len(formulas) == 1 - assert str(formula) == prop + assert len(properties) == 1 + assert str(formula) == formula_str def test_reward_formula(self): - prop = "R=? [F \"one\"]" - formulas = stormpy.parse_formulas(prop) - formula = formulas[0] + formula_str = "R=? [F \"one\"]" + properties = stormpy.parse_properties(formula_str) + formula = properties[0].raw_formula assert type(formula) == stormpy.logic.RewardOperator - assert len(formulas) == 1 + assert len(properties) == 1 assert str(formula) == "R[exp]=? [F \"one\"]" def test_formula_list(self): formulas = [] prop = "=? [F \"one\"]" - forms = stormpy.parse_formulas("P" + prop) - formulas.append(forms[0]) - forms = stormpy.parse_formulas("R" + prop) - formulas.append(forms[0]) + forms = stormpy.parse_properties("P" + prop) + formulas.append(forms[0].raw_formula) + forms = stormpy.parse_properties("R" + prop) + formulas.append(forms[0].raw_formula) assert len(formulas) == 2 assert str(formulas[0]) == "P" + prop assert str(formulas[1]) == "R[exp]" + prop def test_bounds(self): prop = "P=? [F \"one\"]" - formula = stormpy.parse_formulas(prop)[0] + formula = stormpy.parse_properties(prop)[0].raw_formula assert not formula.has_bound prop = "P<0.4 [F \"one\"]" - formula = stormpy.parse_formulas(prop)[0] + formula = stormpy.parse_properties(prop)[0].raw_formula assert formula.has_bound assert formula.threshold == pycarl.Rational("0.4") assert formula.comparison_type == stormpy.logic.ComparisonType.LESS def test_set_bounds(self): prop = "P<0.4 [F \"one\"]" - formula = stormpy.parse_formulas(prop)[0] + formula = stormpy.parse_properties(prop)[0].raw_formula formula.threshold = pycarl.Rational("0.2") formula.comparison_type = stormpy.logic.ComparisonType.GEQ assert formula.threshold == pycarl.Rational("0.2") diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 97d7863..4ca2faf 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -36,7 +36,7 @@ class TestMatrix: for e in matrix: assert e.value() == 0.5 or e.value() == 0 or e.value() == 1 # First model checking - formulas = stormpy.parse_formulas("P=? [ F \"one\" ]") + formulas = stormpy.parse_properties("P=? [ F \"one\" ]") result = stormpy.model_checking(model, formulas[0]) resValue = result.at(model.initial_states[0]) assert math.isclose(resValue, 0.16666666666666663) @@ -74,8 +74,8 @@ class TestMatrix: import stormpy.logic import pycarl program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(program, formulas) matrix = model.transition_matrix # Check matrix one_pol = pycarl.Rational(1) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 5c32826..8ca25f4 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -5,7 +5,7 @@ from helpers.helper import get_example_path class TestModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - model = stormpy.build_model_from_prism_program(program) + model = stormpy.build_model(program) assert model.nr_states == 13 assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC @@ -15,8 +15,8 @@ class TestModel: def test_build_dtmc_from_prism_program_formulas(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) prop = "P=? [F \"one\"]" - formulas = stormpy.parse_formulas_for_prism_program(prop, program) - model = stormpy.build_model_from_prism_program(program, formulas) + properties = stormpy.parse_properties_for_prism_program(prop, program, None) + model = stormpy.build_model(program, properties) assert model.nr_states == 13 assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC @@ -29,8 +29,8 @@ class TestModel: assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants prop = "P=? [F s=5]" - formulas = stormpy.parse_formulas_for_prism_program(prop, program) - model = stormpy.build_parametric_model_from_prism_program(program, formulas) + 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 @@ -40,8 +40,8 @@ class TestModel: def test_build_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC @@ -50,8 +50,8 @@ class TestModel: def test_build_parametric_dtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", 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 @@ -61,8 +61,8 @@ class TestModel: def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_parametric_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_parametric_model(program, formulas) assert model.nr_states == 13 assert model.nr_transitions == 20 assert model.model_type == stormpy.ModelType.DTMC @@ -72,8 +72,8 @@ class TestModel: def test_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) labels = model.labels assert len(labels) == 3 assert "init" in labels @@ -83,16 +83,16 @@ class TestModel: def test_initial_states(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) - model = stormpy.build_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas) initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states def test_label_parametric(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(program, formulas) labels = model.labels assert len(labels) == 3 assert "init" in labels diff --git a/tests/storage/test_model_instantiator.py b/tests/storage/test_model_instantiator.py index 867b3c8..5e7a489 100644 --- a/tests/storage/test_model_instantiator.py +++ b/tests/storage/test_model_instantiator.py @@ -6,8 +6,8 @@ from helpers.helper import get_example_path class TestModel: def test_instantiate_dtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(program, formulas[0]) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_probability_parameters() instantiator = stormpy.storage.PdtmcInstantiator(model) point = dict() @@ -18,4 +18,4 @@ class TestModel: assert not instantiated_model.has_parameters for p in parameters: point[p] = 0.5 - instatiated_model2 = instantiator.instantiate(point) \ No newline at end of file + instatiated_model2 = instantiator.instantiate(point) diff --git a/tests/utility/test_shortestpaths.py b/tests/utility/test_shortestpaths.py index 45f4d96..c0c5411 100644 --- a/tests/utility/test_shortestpaths.py +++ b/tests/utility/test_shortestpaths.py @@ -19,9 +19,9 @@ class ModelWithKnownShortestPaths: program_path = get_example_path("dtmc", "die.pm") raw_formula = "P=? [ F \"" + self.target_label + "\" ]" program = stormpy.parse_prism_program(program_path) - formulas = stormpy.parse_formulas_for_prism_program(raw_formula, program) + formulas = stormpy.parse_properties_for_prism_program(raw_formula, program) - self.model = stormpy.build_model(program, formulas[0]) + self.model = stormpy.build_model(program, formulas) def probability(self, k): return (1/2)**((2 * k) + 1)