tests updated

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

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

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"))

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")

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)

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

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()

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)