More tests for formulas

Former-commit-id: ef9308a100

stormpy/src/core/core.cpp

@@ -40,12 +40,13 @@ std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models
 void define_core(py::module& m) {
     m.def("set_up", &setupStormLib, "Initialize Storm");
 
-    m.def("parse_program", &storm::parseProgram, "Parse program");
-    m.def("parse_formulas", &storm::parseFormulasForProgram, "Parse formula for program");
+    m.def("parse_program", &storm::parseProgram, "Parse program", py::arg("path"));
+    m.def("parse_formulas", &storm::parseFormulasForExplicit, "Parse explicit formulas", py::arg("formula_string"));
+    m.def("parse_formulas_for_program", &storm::parseFormulasForProgram, "Parse formulas for program", py::arg("formula_string"), py::arg("program"));
 
-    m.def("build_model", &buildModel, "Build the model");
-    m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model");
-    m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model");
+    m.def("build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula"));
+    m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
+    m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
 
     //m.def("perform_state_elimination", &performStateElimination, "Perform state elimination");
     

stormpy/src/logic/formulae.cpp

@@ -46,9 +46,9 @@ void define_formulae(py::module& m) {
     py::class_<storm::logic::UnaryStateFormula, std::shared_ptr<storm::logic::UnaryStateFormula const>>(m, "UnaryStateFormula", "State formula with one operand", py::base<storm::logic::StateFormula>());
     py::class_<storm::logic::UnaryBooleanStateFormula, std::shared_ptr<storm::logic::UnaryBooleanStateFormula const>>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base<storm::logic::UnaryStateFormula>());
     py::class_<storm::logic::OperatorFormula, std::shared_ptr<storm::logic::OperatorFormula const>>(m, "OperatorFormula", "Operator formula", py::base<storm::logic::UnaryStateFormula>())
-        .def("has_bound", &storm::logic::OperatorFormula::hasBound)
-        .def_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound)
-        .def_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType)
+        .def("has_bound", &storm::logic::OperatorFormula::hasBound, "Check if formula is bounded")
+        .def_property("threshold", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold of bound")
+        .def_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType, "Comparison type of bound")
     ;
     py::class_<storm::logic::TimeOperatorFormula, std::shared_ptr<storm::logic::TimeOperatorFormula const>>(m, "TimeOperator", "The time operator", py::base<storm::logic::OperatorFormula>());
     py::class_<storm::logic::LongRunAverageOperatorFormula, std::shared_ptr<storm::logic::LongRunAverageOperatorFormula const>>(m, "LongRunAvarageOperator", "Long run average operator", py::base<storm::logic::OperatorFormula>());

stormpy/tests/core/test_parse.py

@@ -8,16 +8,15 @@ class TestParse:
         assert program.has_undefined_constants() == False
     
     def test_parse_formula(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
         prop = "P=? [F \"one\"]"
-        formulas = stormpy.parse_formulas(prop, program)
+        formulas = stormpy.parse_formulas(prop)
         assert len(formulas) == 1
         assert str(formulas[0]) == prop
     
     def test_build_model_from_prism_program(self):
         program = stormpy.parse_program("../examples/dtmc/die/die.pm")
         prop = "P=? [F \"one\"]"
-        formulas = stormpy.parse_formulas(prop, program)
+        formulas = stormpy.parse_formulas_for_program(prop, program)
         pair = stormpy.build_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 13
@@ -27,7 +26,7 @@ class TestParse:
     
     def test_build_model(self):
         program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas("P=? [ F \"one\" ]", program)
+        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_model(program, formulas[0])
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20

stormpy/tests/logic/test_formulas.py

@@ -2,5 +2,49 @@ import stormpy
 from stormpy.logic import logic
 
 class TestFormulas:
-    def test_formula(self):
-        formula = logic.Formula
+
+    def test_probability_formula(self):
+        prop = "P=? [F \"one\"]"
+        formulas = stormpy.parse_formulas(prop)
+        formula = formulas[0]
+        assert type(formula) == logic.ProbabilityOperator
+        assert len(formulas) == 1
+        assert str(formula) == prop
+
+    def test_reward_formula(self):
+        prop = "R=? [F \"one\"]"
+        formulas = stormpy.parse_formulas(prop)
+        formula = formulas[0]
+        assert type(formula) == logic.RewardOperator
+        assert len(formulas) == 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])
+        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]
+        assert not formula.has_bound()
+        prop = "P<0.4 [F \"one\"]"
+        formula = stormpy.parse_formulas(prop)[0]
+        assert formula.has_bound()
+        assert formula.threshold == 0.4
+        assert formula.comparison_type == logic.ComparisonType.LESS
+
+    def test_set_bounds(self):
+        prop = "P<0.4 [F \"one\"]"
+        formula = stormpy.parse_formulas(prop)[0]
+        formula.threshold = 0.2
+        formula.comparison_type = logic.ComparisonType.GEQ
+        assert formula.threshold == 0.2
+        assert formula.comparison_type == logic.ComparisonType.GEQ
+        assert str(formula) == "P>=0.2 [F \"one\"]"