diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 031fb5e87..fd4aae161 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -24,3 +24,116 @@ void define_core(py::module& m) { } + +/*// Holds the rational function and constraints after parametric model checking +class PmcResult { +public: + storm::RationalFunction resultFunction; + std::unordered_set> constraintsWellFormed; + std::unordered_set> constraintsGraphPreserving; +}; + +// 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 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; +} + +// Thin wrapper for initializing +void setupStormLib(std::string const& args) { + storm::utility::setUp(); + storm::settings::SettingsManager::manager().setFromString(args); +} + +BOOST_PYTHON_MODULE(_core) +{ + using namespace boost::python; + def("set_up", setupStormLib); + + + //////////////////////////////////////////// + // Program + //////////////////////////////////////////// + + defineClass("Program", "") + .add_property("nr_modules", &storm::prism::Program::getNumberOfModules) + ; + + + //////////////////////////////////////////// + // PmcResult + //////////////////////////////////////////// + class_, boost::noncopyable>("PmcResult", "Holds the results after parametric model checking") + .add_property("result_function", &PmcResult::resultFunction) + .add_property("constraints_well_formed", &PmcResult::constraintsWellFormed) + .add_property("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving) + ; + register_ptr_to_python>(); + + + //////////////////////////////////////////// + // Models + //////////////////////////////////////////// + + enum_("ModelType") + .value("DTMC", storm::models::ModelType::Dtmc) + .value("MDP", storm::models::ModelType::Mdp) + .value("CTMC", storm::models::ModelType::Ctmc) + .value("MA", storm::models::ModelType::MarkovAutomaton) + ; + + defineClass("ModelBase", "") + .add_property("nr_states", &storm::models::ModelBase::getNumberOfStates) + .add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions) + .add_property("model_type", &storm::models::ModelBase::getType) + .add_property("parametric", &storm::models::ModelBase::isParametric) + .def("as_dtmc", &storm::models::ModelBase::as>) + .def("as_pdtmc", &storm::models::ModelBase::as>) + .def("as_mdp", &storm::models::ModelBase::as>) + .def("as_pmdp", &storm::models::ModelBase::as>) + ; + + + defineClass, storm::models::ModelBase, boost::noncopyable>("SparseModel", + "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); + defineClass, storm::models::sparse::Model, boost::noncopyable>("SparseDtmc", ""); + defineClass, storm::models::sparse::Model>("SparseMdp", ""); + + defineClass, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "") + .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters) + ; + defineClass, storm::models::sparse::Model>("SparseParametricDtmc", ""); + defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); + + + //////////////////////////////////////////// + // Bisimulation + //////////////////////////////////////////// + enum_("BisimulationType") + .value("STRONG", storm::storage::BisimulationType::Strong) + .value("WEAK", storm::storage::BisimulationType::Weak) + ; + def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>)); + + + + ////////////////////////////////////////////// + // Model Checking + ////////////////////////////////////////////// + class_("ModelProgramPair", no_init) + .add_property("model", &storm::storage::ModelFormulasPair::model) + .add_property("program", &storm::storage::ModelFormulasPair::formulas) + ; + + def("perform_state_elimination", performStateElimination); +}*/