diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index d3e9b6af2..0883f133f 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -40,12 +40,13 @@ std::shared_ptr performStateElimination(std::shared_ptr, "Build the model"); - m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "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, "Build the model", py::arg("program"), py::arg("formulas")); + m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); //m.def("perform_state_elimination", &performStateElimination, "Perform state elimination"); diff --git a/stormpy/src/logic/formulae.cpp b/stormpy/src/logic/formulae.cpp index 926a69f14..ad4bb52b1 100644 --- a/stormpy/src/logic/formulae.cpp +++ b/stormpy/src/logic/formulae.cpp @@ -46,9 +46,9 @@ void define_formulae(py::module& m) { py::class_>(m, "UnaryStateFormula", "State formula with one operand", py::base()); py::class_>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base()); py::class_>(m, "OperatorFormula", "Operator formula", py::base()) - .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_>(m, "TimeOperator", "The time operator", py::base()); py::class_>(m, "LongRunAvarageOperator", "Long run average operator", py::base()); diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py index b064dc238..ee55f4150 100644 --- a/stormpy/tests/core/test_parse.py +++ b/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 diff --git a/stormpy/tests/logic/test_formulas.py b/stormpy/tests/logic/test_formulas.py index 3d43775b1..7600f5a6f 100644 --- a/stormpy/tests/logic/test_formulas.py +++ b/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\"]"