Pybind for bisimulation and state elimination

Former-commit-id: 5d3d6e0bb2

stormpy/src/core/core.cpp

@@ -17,24 +17,48 @@ std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const
     return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<const storm::logic::Formula>>(1,formula)).model;
 }
 
+// Thin wrapper for bisimulation
+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<const storm::logic::Formula> const& formula, storm::storage::BisimulationType bisimulationType) {
+    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formula, bisimulationType);
+}
+
 // Class holding the model checking result
-/*class PmcResult {
+class PmcResult {
     public:
         storm::RationalFunction resultFunction;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
+
+        /*storm::RationalFunction getFunc() {
+            return resultFunction;
+        }*/
+
+        std::string toString() {
+            std::stringstream stream;
+            stream << resultFunction << std::endl;
+            stream << "Well formed constraints:" << std::endl;
+            for (auto constraint : constraintsWellFormed) {
+                stream << constraint << std::endl;
+            }
+            stream << "Graph preserving constraints:" << std::endl;
+            for (auto constraint : constraintsGraphPreserving) {
+                stream << constraint << std::endl;
+            }
+            return stream.str();
+        }
 };
 
 // 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& 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()]);
+    result->resultFunction = checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()];
     storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector constraintCollector(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>()));
     result->constraintsWellFormed = constraintCollector.getWellformedConstraints();
     result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints();
     return result;
-}*/
+}
 
 // Define python bindings
 void define_core(py::module& m) {
@@ -44,14 +68,7 @@ void define_core(py::module& m) {
     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", 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");
-    
-    //m.def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<const storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>), "Perform bisimulation");
-    
+    m.def("perform_state_elimination", &performStateElimination, "Perform state elimination", py::arg("model"), py::arg("formula"));
 
     // Program
     py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
@@ -76,6 +93,10 @@ void define_core(py::module& m) {
 
     
     // Models
+    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"));
+
     py::enum_<storm::models::ModelType>(m, "ModelType", "Type of the model")
         .value("DTMC", storm::models::ModelType::Dtmc)
         .value("MDP", storm::models::ModelType::Mdp)
@@ -96,36 +117,35 @@ void define_core(py::module& m) {
 
     py::class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base<storm::models::ModelBase>())
     ;    
-
     py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", py::base<storm::models::sparse::Model<double>>())
     ;
-
     py::class_<storm::models::sparse::Mdp<double>, std::shared_ptr<storm::models::sparse::Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", py::base<storm::models::sparse::Model<double>>())
     ;
-
     py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base<storm::models::ModelBase>())
         .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters")
     ;
-
     py::class_<storm::models::sparse::Dtmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
     ;
-
     py::class_<storm::models::sparse::Mdp<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>>>(m, "SparseParametricMdp", "pMDP in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
     ;
-
     
-    // PmcResult
-    /*py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
-        .def_readwrite("result_function", &PmcResult::resultFunction, "Result as rational function")
-        //.def_readwrite("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
-        //.def_readwrite("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
-    ;*/
-
 
     // Bisimulation
-    /*py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
+    py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
         .value("STRONG", storm::storage::BisimulationType::Strong)
         .value("WEAK", storm::storage::BisimulationType::Weak)
-    ;*/
+    ;
     
+    m.def("perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
+    m.def("perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
+
+    // PmcResult
+    py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
+        .def("__str__", &PmcResult::toString)
+        //.def("result_function", &PmcResult::getFunc, "Result as rational function")
+        //.def_readwrite("result_function", &PmcResult::resultFunction, "Result as rational function")
+        //.def_readwrite("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
+        //.def_readwrite("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+    ;
+
 }

stormpy/tests/core/test_core.py

@@ -3,3 +3,67 @@ import stormpy
 class TestCore:
     def test_init(self):
         stormpy.set_up("")
+    
+    def test_build_parametric_model_from_prism_program(self):
+        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
+        assert program.nr_modules() == 5
+        assert program.model_type() == stormpy.PrismModelType.DTMC
+        assert program.has_undefined_constants()
+        prop = "P=? [F \"target\"]"
+        formulas = stormpy.parse_formulas_for_program(prop, program)
+        pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+        model = pair.model
+        assert model.nr_states() == 613
+        assert model.nr_transitions() == 803
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert model.parametric()
+    
+    def test_bisimulation(self):
+        program = stormpy.parse_program("../examples/dtmc/crowds/crowds5_5.pm")
+        assert program.nr_modules() == 1
+        assert program.model_type() == stormpy.PrismModelType.DTMC
+        prop = "P=? [F \"observe0Greater1\"]"
+        formulas = stormpy.parse_formulas_for_program(prop, program)
+        pair = stormpy.build_model_from_prism_program(program, formulas)
+        model = pair.model
+        assert model.nr_states() == 7403
+        assert model.nr_transitions() == 13041
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert not model.parametric()
+        model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
+        assert model_bisim.nr_states() == 64
+        assert model_bisim.nr_transitions() == 104
+        assert model_bisim.model_type() == stormpy.ModelType.DTMC
+        assert not model_bisim.parametric()
+    
+    def test_parametric_bisimulation(self):
+        program = stormpy.parse_program("../examples/pdtmc/crowds/crowds_3-5.pm")
+        assert program.nr_modules() == 1
+        assert program.model_type() == stormpy.PrismModelType.DTMC
+        assert program.has_undefined_constants()
+        prop = "P=? [F \"observe0Greater1\"]"
+        formulas = stormpy.parse_formulas_for_program(prop, program)
+        pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+        model = pair.model
+        assert model.nr_states() == 1367
+        assert model.nr_transitions() == 2027
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert model.parametric()
+        model_bisim = stormpy.perform_parametric_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
+        assert model_bisim.nr_states() == 80
+        assert model_bisim.nr_transitions() == 120
+        assert model_bisim.model_type() == stormpy.ModelType.DTMC
+        assert model_bisim.parametric()
+    
+    def test_state_elimination(self):
+        import pycarl
+        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
+        prop = "P=? [F \"target\"]"
+        formulas = stormpy.parse_formulas_for_program(prop, program)
+        pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+        model = pair.model
+        assert model.nr_states() == 613
+        assert model.nr_transitions() == 803
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert model.parametric()
+        result = stormpy.perform_state_elimination(model, formulas[0])

stormpy/tests/core/test_parse.py

@@ -5,7 +5,7 @@ class TestParse:
         program = stormpy.parse_program("../examples/dtmc/die/die.pm")
         assert program.nr_modules() == 1
         assert program.model_type() == stormpy.PrismModelType.DTMC
-        assert program.has_undefined_constants() == False
+        assert not program.has_undefined_constants()
     
     def test_parse_formula(self):
         prop = "P=? [F \"one\"]"
@@ -22,7 +22,7 @@ class TestParse:
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric() == False
+        assert not model.parametric()
     
     def test_build_model(self):
         program = stormpy.parse_program("../examples/dtmc/die/die.pm")
@@ -31,5 +31,4 @@ class TestParse:
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric() == True
-        
+        assert model.parametric()