#include "model.h" #include "storm/models/ModelBase.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/ModelInstantiator.h" // Thin wrapper for getting initial states template std::vector getInitialStates(storm::models::sparse::Model const& model) { std::vector initialStates; for (auto entry : model.getInitialStates()) { initialStates.push_back(entry); } return initialStates; } // Thin wrapper for getting transition matrix template storm::storage::SparseMatrix& getTransitionMatrix(storm::models::sparse::Model& model) { return model.getTransitionMatrix(); } std::set probabilityVariables(storm::models::sparse::Model const& model) { return storm::models::sparse::getProbabilityParameters(model); } std::set rewardVariables(storm::models::sparse::Model const& model) { return storm::models::sparse::getRewardParameters(model); } // Define python bindings void define_model(py::module& m) { // 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_> modelBase(m, "_ModelBase", "Base class for all models"); modelBase.def_property_readonly("nr_states", &storm::models::ModelBase::getNumberOfStates, "Number of states") .def_property_readonly("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Number of transitions") .def_property_readonly("model_type", &storm::models::ModelBase::getType, "Model type") .def_property_readonly("supports_parameters", &storm::models::ModelBase::supportsParameters, "Flag whether model supports parameters") .def_property_readonly("has_parameters", &storm::models::ModelBase::hasParameters, "Flag whether model has parameters") .def_property_readonly("is_exact", &storm::models::ModelBase::isExact, "Flag whether model is exact") .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") .def("_as_ctmc", &storm::models::ModelBase::as>, "Get model as CTMC") .def("_as_pctmc", &storm::models::ModelBase::as>, "Get model as pCTMC") .def("_as_ma", &storm::models::ModelBase::as>, "Get model as MA") .def("_as_pma", &storm::models::ModelBase::as>, "Get model as pMA") ; // Models //storm::models::sparse::Model > py::class_, std::shared_ptr>> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", modelBase); model.def_property_readonly("labels", [](storm::models::sparse::Model& model) { return model.getStateLabeling().getLabels(); }, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) ; py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) ; py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) ; py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) ; py::class_, std::shared_ptr>> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") .def_property_readonly("labels", [](storm::models::sparse::Model& model) { return model.getStateLabeling().getLabels(); }, "Labels") .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) ; py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) ; py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) ; py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) ; } // Model instantiator void define_model_instantiator(py::module& m) { py::class_,storm::models::sparse::Dtmc>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to DTMCs") .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values"); py::class_,storm::models::sparse::Mdp>>(m, "PmdpInstantiator", "Instantiate PMDPs to MDPs") .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values"); py::class_,storm::models::sparse::Ctmc>>(m, "PctmcInstantiator", "Instantiate PCTMCs to CTMCs") .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Ctmc>::instantiate, "Instantiate model with given parameter values"); py::class_,storm::models::sparse::MarkovAutomaton>>(m, "PmaInstantiator", "Instantiate PMAs to MAs") .def(py::init>(), "parametric model"_a) .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::MarkovAutomaton>::instantiate, "Instantiate model with given parameter values"); }