Model checking binding

Former-commit-id: 10a7ebcf81

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)

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", &parametricModelChecking, "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")

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