Refactoring

Former-commit-id: 0ff9eff43a

stormpy/lib/stormpy/__init__.py

@@ -1,2 +1,28 @@
 from . import core
 from .core import *
+
+def build_model(program, formulae):
+    intermediate = core._build_model(program, formulae)
+    
+    if intermediate.parametric():
+         raise RuntimeError("Model should be non-parametric")
+    else:
+         if intermediate.model_type() == ModelType.DTMC:
+             return intermediate.as_dtmc()
+         elif intermediate.model_type() == ModelType.MDP:
+             return intermediate.as_mdp()
+         else:
+             raise RuntimeError("Not supported non-parametric model constructed")
+
+def build_parametric_model(program, formulae):
+    intermediate = core._build_parametric_model(program, formulae)
+    
+    if intermediate.parametric():
+         if intermediate.model_type() == ModelType.DTMC:
+             return intermediate.as_pdtmc()
+         elif intermediate.model_type() == ModelType.MDP:
+             return intermediate.as_pmdp()
+         else:
+             raise RuntimeError("Not supported parametric model constructed")
+    else:
+        raise RuntimeError("Model should be parametric")

stormpy/src/core/bisimulation.cpp

@@ -0,0 +1,22 @@
+#include "bisimulation.h"
+
+// 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<storm::logic::Formula const> const& formula, storm::storage::BisimulationType bisimulationType) {
+    return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formula, bisimulationType);
+}
+
+// Define python bindings
+void define_bisimulation(py::module& m) {
+
+    // Bisimulation
+    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"));
+
+    // BisimulationType 
+    py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
+        .value("STRONG", storm::storage::BisimulationType::Strong)
+        .value("WEAK", storm::storage::BisimulationType::Weak)
+    ;
+
+}

stormpy/src/core/bisimulation.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_BISIMULATION_H_
+#define PYTHON_CORE_BISIMULATION_H_
+
+#include "common.h"
+
+void define_bisimulation(py::module& m);
+
+#endif /* PYTHON_CORE_BISIMULATION_H_ */

stormpy/src/core/common.h

@@ -0,0 +1,4 @@
+#include "src/common.h"
+#include <pybind11/stl.h>
+
+#include <src/utility/storm.h>

stormpy/src/core/core.cpp

@@ -1,146 +1,20 @@
 #include "core.h"
 
-#include <pybind11/stl.h>
-
-#include "src/common.h"
-
-#include <src/utility/storm.h>
-
-// Thin wrapper for initializing
-void setupStormLib(std::string const& args) {
-    storm::utility::setUp();
-    storm::settings::SettingsManager::manager().setFromString(args);
-}
-
-// Thin wrapper for model building
-std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula) {
-    return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<storm::logic::Formula const>>(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<storm::logic::Formula const> 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 {
-    public:
-        storm::RationalFunction resultFunction;
-        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
-        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
-
-        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> 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()];
-    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) {
-    m.def("set_up", &setupStormLib, "Initialize Storm");
+    
+    // Init
+    m.def("set_up", [] (std::string const& args) {
+            storm::utility::setUp();
+            storm::settings::SettingsManager::manager().setFromString(args);
+        }, "Initialize Storm", py::arg("arguments"));
 
-    m.def("parse_program", &storm::parseProgram, "Parse program", py::arg("path"));
+    // Parse formulas
     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("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")
-        .value("DTMC", storm::prism::Program::ModelType::DTMC)
-        .value("CTMC", storm::prism::Program::ModelType::CTMC)
-        .value("MDP", storm::prism::Program::ModelType::MDP)
-        .value("CTMDP", storm::prism::Program::ModelType::CTMDP)
-        .value("MA", storm::prism::Program::ModelType::MA)
-        .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED)
-    ;
-    
-    py::class_<storm::prism::Program>(m, "Program", "Prism program")
-        .def("nr_modules", &storm::prism::Program::getNumberOfModules, "Get number of modules")
-        .def("model_type", &storm::prism::Program::getModelType, "Get model type")
-        .def("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Check if program has undefined constants")
-    ;
-    
-    py::class_<storm::storage::ModelFormulasPair>(m, "ModelProgramPair", "Pair of model and program")
+    // Pair <Model,Formulas>
+    py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
         .def_readwrite("model", &storm::storage::ModelFormulasPair::model, "The model")
         .def_readwrite("formulas", &storm::storage::ModelFormulasPair::formulas, "The formulas")
     ;
-
-    
-    // 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)
-        .value("CTMC", storm::models::ModelType::Ctmc)
-        .value("MA", storm::models::ModelType::MarkovAutomaton)
-    ;
-
-    py::class_<storm::models::ModelBase, std::shared_ptr<storm::models::ModelBase>>(m, "ModelBase", "Base class for all models")
-        .def("nr_states", &storm::models::ModelBase::getNumberOfStates, "Get number of states")
-        .def("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Get number of transitions")
-        .def("model_type", &storm::models::ModelBase::getType, "Get model type")
-        .def("parametric", &storm::models::ModelBase::isParametric, "Check if model is parametric")
-        .def("as_dtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<double>>, "Get model as DTMC")
-        .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
-        .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")
-        .def("as_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>, "Get model as pMDP")
-    ;
-
-    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>>())
-    ;
-    
-
-    // 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_readonly("result_function", &PmcResult::resultFunction, "Result as rational function")
-        .def_readonly("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
-        .def_readonly("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
-    ;
-
 }

stormpy/src/core/core.h

@@ -1,7 +1,7 @@
 #ifndef PYTHON_CORE_CORE_H_
 #define PYTHON_CORE_CORE_H_
 
-#include "src/common.h"
+#include "common.h"
 
 void define_core(py::module& m);
 

stormpy/src/core/model.cpp

@@ -0,0 +1,53 @@
+#include "model.h"
+
+// Thin wrapper for model building
+template<typename ValueType>
+std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula) {
+    return storm::buildSymbolicModel<ValueType>(program, std::vector<std::shared_ptr<storm::logic::Formula const>>(1,formula)).model;
+}
+
+// Define python bindings
+void define_model(py::module& m) {
+   
+    // Build model
+    m.def("_build_model", &buildModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
+    m.def("_build_parametric_model", &buildModel<storm::RationalFunction>, "Build the parametric 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"));
+
+    // ModelType
+    py::enum_<storm::models::ModelType>(m, "ModelType", "Type of the model")
+        .value("DTMC", storm::models::ModelType::Dtmc)
+        .value("MDP", storm::models::ModelType::Mdp)
+        .value("CTMC", storm::models::ModelType::Ctmc)
+        .value("MA", storm::models::ModelType::MarkovAutomaton)
+    ;
+
+    // ModelBase
+    py::class_<storm::models::ModelBase, std::shared_ptr<storm::models::ModelBase>>(m, "ModelBase", "Base class for all models")
+        .def("nr_states", &storm::models::ModelBase::getNumberOfStates, "Get number of states")
+        .def("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Get number of transitions")
+        .def("model_type", &storm::models::ModelBase::getType, "Get model type")
+        .def("parametric", &storm::models::ModelBase::isParametric, "Check if model is parametric")
+        .def("as_dtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<double>>, "Get model as DTMC")
+        .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
+        .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")
+        .def("as_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>, "Get model as pMDP")
+    ;
+
+    // Models
+    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>>())
+    ;
+
+}

stormpy/src/core/model.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_MODEL_H_
+#define PYTHON_CORE_MODEL_H_
+
+#include "common.h"
+
+void define_model(py::module& m);
+
+#endif /* PYTHON_CORE_MODEL_H_ */

stormpy/src/core/modelchecking.cpp

@@ -0,0 +1,50 @@
+#include "modelchecking.h"
+
+// Class holding the model checking result
+class PmcResult {
+    public:
+        storm::RationalFunction resultFunction;
+        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
+        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
+
+        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> 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()];
+    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_modelchecking(py::module& m) {
+
+    // Model checking
+    m.def("perform_state_elimination", &performStateElimination, "Perform state elimination", py::arg("model"), py::arg("formula"));
+
+    // PmcResult
+    py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
+        .def("__str__", &PmcResult::toString)
+        .def_readonly("result_function", &PmcResult::resultFunction, "Result as rational function")
+        .def_readonly("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
+        .def_readonly("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+    ;
+
+}

stormpy/src/core/modelchecking.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_MODELCHECKING_H_
+#define PYTHON_CORE_MODELCHECKING_H_
+
+#include "common.h"
+
+void define_modelchecking(py::module& m);
+
+#endif /* PYTHON_CORE_MODELCHECKING_H_ */

stormpy/src/core/prism.cpp

@@ -0,0 +1,26 @@
+#include "prism.h"
+
+// Define python bindings
+void define_prism(py::module& m) {
+
+    // Parse prism program
+    m.def("parse_program", &storm::parseProgram, "Parse program", py::arg("path"));
+
+    // PrismType
+    py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
+        .value("DTMC", storm::prism::Program::ModelType::DTMC)
+        .value("CTMC", storm::prism::Program::ModelType::CTMC)
+        .value("MDP", storm::prism::Program::ModelType::MDP)
+        .value("CTMDP", storm::prism::Program::ModelType::CTMDP)
+        .value("MA", storm::prism::Program::ModelType::MA)
+        .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED)
+    ;
+    
+    // PrismProgram
+    py::class_<storm::prism::Program>(m, "Program", "Prism program")
+        .def("nr_modules", &storm::prism::Program::getNumberOfModules, "Get number of modules")
+        .def("model_type", &storm::prism::Program::getModelType, "Get model type")
+        .def("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Check if program has undefined constants")
+    ;
+    
+}

stormpy/src/core/prism.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_CORE_PRISM_H_
+#define PYTHON_CORE_PRISM_H_
+
+#include "common.h"
+
+void define_prism(py::module& m);
+
+#endif /* PYTHON_CORE_PRISM_H_ */

stormpy/src/mod_core.cpp

@@ -1,9 +1,17 @@
 #include "common.h"
 
 #include "core/core.h"
+#include "core/model.h"
+#include "core/modelchecking.h"
+#include "core/bisimulation.h"
+#include "core/prism.h"
 
 PYBIND11_PLUGIN(core) {
     py::module m("core");
     define_core(m);
+    define_model(m);
+    define_modelchecking(m);
+    define_bisimulation(m);
+    define_prism(m);
     return m.ptr();
 }

stormpy/tests/core/test_parse.py

@@ -31,4 +31,4 @@ class TestParse:
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
-        assert model.parametric()
+        assert not model.parametric()