diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index ebcff7e99..b959014b9 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/stormpy/lib/stormpy/__init__.py @@ -28,3 +28,9 @@ def perform_bisimulation(model, formula, bisimulation_type): return core._perform_parametric_bisimulation(model, formula, bisimulation_type) else: return core._perform_bisimulation(model, formula, bisimulation_type) + +def model_checking(model, formula): + if model.supports_parameters(): + return core._parametric_model_checking(model, formula) + else: + return core._model_checking(model, formula) diff --git a/stormpy/src/core/modelchecking.cpp b/stormpy/src/core/modelchecking.cpp index d1fde5973..3e9b7756b 100644 --- a/stormpy/src/core/modelchecking.cpp +++ b/stormpy/src/core/modelchecking.cpp @@ -22,8 +22,14 @@ class PmcResult { } }; -// Thin wrapper for parametric state elimination -std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) { +// Thin wrapper for model checking +double modelChecking(std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) { + std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<double>(model, formula); + return checkResult->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()]; +} + +// Thin wrapper for parametric model checking +std::shared_ptr<PmcResult> parametricModelChecking(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) { std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula); std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>(); result->resultFunction = checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]; @@ -37,7 +43,8 @@ std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models void define_modelchecking(py::module& m) { // Model checking - m.def("perform_state_elimination", &performStateElimination, "Perform state elimination", py::arg("model"), py::arg("formula")); + m.def("_model_checking", &modelChecking, "Perform model checking", py::arg("model"), py::arg("formula")); + m.def("_parametric_model_checking", ¶metricModelChecking, "Perform parametric model checking", py::arg("model"), py::arg("formula")); // PmcResult py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking") diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index 2c9b8caab..334d049cf 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/stormpy/tests/core/test_modelchecking.py @@ -3,6 +3,15 @@ import stormpy.logic class TestModelChecking: def test_state_elimination(self): + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + 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 + result = stormpy.model_checking(model, formulas[0]) + assert result == 0.16666666666666663 + + def test_parametric_state_elimination(self): import pycarl import pycarl.formula program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm") @@ -14,7 +23,7 @@ class TestModelChecking: assert model.nr_transitions() == 803 assert model.model_type() == stormpy.ModelType.DTMC assert model.has_parameters() - result = stormpy.perform_state_elimination(model, formulas[0]) + result = stormpy.model_checking(model, formulas[0]) func = result.result_function one = pycarl.FactorizedPolynomial(pycarl.Rational(1)) assert func.denominator == one