From 4e86667b46bb7dff645a345a77d0a66febe3602f Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 12 May 2016 17:53:55 +0200 Subject: [PATCH] Refactoring Former-commit-id: 0ff9eff43a38ce91160fefdd72065c3e19c2bfb0 --- stormpy/lib/stormpy/__init__.py | 26 ++++++ stormpy/src/core/bisimulation.cpp | 22 +++++ stormpy/src/core/bisimulation.h | 8 ++ stormpy/src/core/common.h | 4 + stormpy/src/core/core.cpp | 144 ++--------------------------- stormpy/src/core/core.h | 2 +- stormpy/src/core/model.cpp | 53 +++++++++++ stormpy/src/core/model.h | 8 ++ stormpy/src/core/modelchecking.cpp | 50 ++++++++++ stormpy/src/core/modelchecking.h | 8 ++ stormpy/src/core/prism.cpp | 26 ++++++ stormpy/src/core/prism.h | 8 ++ stormpy/src/mod_core.cpp | 8 ++ stormpy/tests/core/test_parse.py | 2 +- 14 files changed, 232 insertions(+), 137 deletions(-) create mode 100644 stormpy/src/core/bisimulation.cpp create mode 100644 stormpy/src/core/bisimulation.h create mode 100644 stormpy/src/core/common.h create mode 100644 stormpy/src/core/model.cpp create mode 100644 stormpy/src/core/model.h create mode 100644 stormpy/src/core/modelchecking.cpp create mode 100644 stormpy/src/core/modelchecking.h create mode 100644 stormpy/src/core/prism.cpp create mode 100644 stormpy/src/core/prism.h diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index ca45a2d36..9a126cbfe 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/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") diff --git a/stormpy/src/core/bisimulation.cpp b/stormpy/src/core/bisimulation.cpp new file mode 100644 index 000000000..240c8b1c8 --- /dev/null +++ b/stormpy/src/core/bisimulation.cpp @@ -0,0 +1,22 @@ +#include "bisimulation.h" + +// Thin wrapper for bisimulation +template +std::shared_ptr> performBisimulation(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType bisimulationType) { + return storm::performBisimulationMinimization>(model, formula, bisimulationType); +} + +// Define python bindings +void define_bisimulation(py::module& m) { + + // Bisimulation + m.def("perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); + m.def("perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); + + // BisimulationType + py::enum_(m, "BisimulationType", "Types of bisimulation") + .value("STRONG", storm::storage::BisimulationType::Strong) + .value("WEAK", storm::storage::BisimulationType::Weak) + ; + +} diff --git a/stormpy/src/core/bisimulation.h b/stormpy/src/core/bisimulation.h new file mode 100644 index 000000000..d444f40e9 --- /dev/null +++ b/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_ */ diff --git a/stormpy/src/core/common.h b/stormpy/src/core/common.h new file mode 100644 index 000000000..68aac6d6f --- /dev/null +++ b/stormpy/src/core/common.h @@ -0,0 +1,4 @@ +#include "src/common.h" +#include + +#include diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 98d9332c6..a3cf262d9 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -1,146 +1,20 @@ #include "core.h" -#include - -#include "src/common.h" - -#include - -// 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 buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { - return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; -} - -// Thin wrapper for bisimulation -template -std::shared_ptr> performBisimulation(std::shared_ptr> const& model, std::shared_ptr const& formula, storm::storage::BisimulationType bisimulationType) { - return storm::performBisimulationMinimization>(model, formula, bisimulationType); -} - -// Class holding the model checking result -class PmcResult { - public: - storm::RationalFunction resultFunction; - std::unordered_set> constraintsWellFormed; - std::unordered_set> 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 performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { - std::unique_ptr checkResult = storm::verifySparseModel(model, formula); - std::shared_ptr result = std::make_shared(); - result->resultFunction = checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; - storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); - 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_(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_(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_(m, "ModelProgramPair", "Pair of model and program") + // Pair + py::class_(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, "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")); - - py::enum_(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_>(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>, "Get model as DTMC") - .def("as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") - .def("as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") - .def("as_pmdp", &storm::models::ModelBase::as>, "Get model as pMDP") - ; - - py::class_, std::shared_ptr>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base()) - ; - py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", py::base>()) - ; - py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", py::base>()) - ; - py::class_, std::shared_ptr>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base()) - .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters") - ; - py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base>()) - ; - py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", py::base>()) - ; - - - // Bisimulation - py::enum_(m, "BisimulationType", "Types of bisimulation") - .value("STRONG", storm::storage::BisimulationType::Strong) - .value("WEAK", storm::storage::BisimulationType::Weak) - ; - - m.def("perform_bisimulation", &performBisimulation, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); - m.def("perform_parametric_bisimulation", &performBisimulation, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type")); - - // PmcResult - py::class_>(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") - ; - } diff --git a/stormpy/src/core/core.h b/stormpy/src/core/core.h index 0f53b21bd..f750d7c74 100644 --- a/stormpy/src/core/core.h +++ b/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); diff --git a/stormpy/src/core/model.cpp b/stormpy/src/core/model.cpp new file mode 100644 index 000000000..fe618618e --- /dev/null +++ b/stormpy/src/core/model.cpp @@ -0,0 +1,53 @@ +#include "model.h" + +// Thin wrapper for model building +template +std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { + return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; +} + +// Define python bindings +void define_model(py::module& m) { + + // Build model + m.def("_build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula")); + m.def("_build_parametric_model", &buildModel, "Build the parametric 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")); + + // ModelType + py::enum_(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_>(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>, "Get model as DTMC") + .def("as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") + .def("as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") + .def("as_pmdp", &storm::models::ModelBase::as>, "Get model as pMDP") + ; + + // Models + py::class_, std::shared_ptr>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base()) + ; + py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", py::base>()) + ; + py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", py::base>()) + ; + py::class_, std::shared_ptr>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base()) + .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters") + ; + py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base>()) + ; + py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", py::base>()) + ; + +} diff --git a/stormpy/src/core/model.h b/stormpy/src/core/model.h new file mode 100644 index 000000000..9f5c279e6 --- /dev/null +++ b/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_ */ diff --git a/stormpy/src/core/modelchecking.cpp b/stormpy/src/core/modelchecking.cpp new file mode 100644 index 000000000..d1fde5973 --- /dev/null +++ b/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> constraintsWellFormed; + std::unordered_set> 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 performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { + std::unique_ptr checkResult = storm::verifySparseModel(model, formula); + std::shared_ptr result = std::make_shared(); + result->resultFunction = checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; + storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); + 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_>(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") + ; + +} diff --git a/stormpy/src/core/modelchecking.h b/stormpy/src/core/modelchecking.h new file mode 100644 index 000000000..06b1aad3c --- /dev/null +++ b/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_ */ diff --git a/stormpy/src/core/prism.cpp b/stormpy/src/core/prism.cpp new file mode 100644 index 000000000..2cc88f370 --- /dev/null +++ b/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_(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_(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") + ; + +} diff --git a/stormpy/src/core/prism.h b/stormpy/src/core/prism.h new file mode 100644 index 000000000..6a4d43307 --- /dev/null +++ b/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_ */ diff --git a/stormpy/src/mod_core.cpp b/stormpy/src/mod_core.cpp index a4fd9a438..c86da7fba 100644 --- a/stormpy/src/mod_core.cpp +++ b/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(); } diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py index 909bef7a2..fe1c92ba0 100644 --- a/stormpy/tests/core/test_parse.py +++ b/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()