diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 8a47e13..883cc2c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -22,15 +22,46 @@ except ImportError: core._set_up("") +def _convert_sparse_model(model, parametric=False): + """ + Convert (parametric) model in sparse representation into model corresponding to exact model type. + :param model: Sparse model. + :param parametric: Flag indicating if the model is parametric. + :return: Model corresponding to exact model type. + """ + if parametric: + assert model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_sparse_pdtmc() + elif model.model_type == ModelType.MDP: + return model._as_sparse_pmdp() + elif model.model_type == ModelType.CTMC: + return model._as_sparse_pctmc() + elif model.model_type == ModelType.MA: + return model._as_sparse_pma() + else: + raise StormError("Not supported parametric model constructed") + else: + assert not model.supports_parameters + if model.model_type == ModelType.DTMC: + return model._as_sparse_dtmc() + elif model.model_type == ModelType.MDP: + return model._as_sparse_mdp() + elif model.model_type == ModelType.CTMC: + return model._as_sparse_ctmc() + elif model.model_type == ModelType.MA: + return model._as_sparse_ma() + else: + raise StormError("Not supported non-parametric model constructed") + def build_model(symbolic_description, properties=None): """ - Build a model from a symbolic description. + Build a model in sparse representation from a symbolic description. :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Model in sparse representation. - :rtype: SparseDtmc or SparseMdp """ if not symbolic_description.undefined_constants_are_graph_preserving: raise StormError("Program still contains undefined constants") @@ -40,91 +71,49 @@ def build_model(symbolic_description, properties=None): intermediate = core._build_sparse_model_from_prism_program(symbolic_description, formulae) else: intermediate = core._build_sparse_model_from_prism_program(symbolic_description) - assert not intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_dtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_mdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_ctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_ma() - else: - raise StormError("Not supported non-parametric model constructed") + return _convert_sparse_model(intermediate, parametric=False) def build_parametric_model(symbolic_description, properties=None): """ - Build a parametric model from a symbolic description. + Build a parametric model in sparse representation from a symbolic description. :param symbolic_description: Symbolic model description to translate into a model. :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. :return: Parametric model in sparse representation. - :rtype: SparseParametricDtmc or SparseParametricMdp """ if not symbolic_description.undefined_constants_are_graph_preserving: raise StormError("Program still contains undefined constants") if properties: formulae = [prop.raw_formula for prop in properties] + intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) else: - formulae = [] - intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description, formulae) - assert intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_pmdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_pctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_pma() - else: - raise StormError("Not supported parametric model constructed") + intermediate = core._build_sparse_parametric_model_from_prism_program(symbolic_description) + return _convert_sparse_model(intermediate, parametric=True) def build_model_from_drn(file): """ - Build a model from the explicit DRN representation. + Build a model in sparse representation from the explicit DRN representation. :param String file: DRN file containing the model. :return: Model in sparse representation. - :rtype: SparseDtmc or SparseMdp or SparseCTMC or SparseMA """ intermediate = core._build_sparse_model_from_drn(file) - assert not intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_dtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_mdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_ctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_ma() - else: - raise StormError("Not supported non-parametric model constructed") + return _convert_sparse_model(intermediate, parametric=False) def build_parametric_model_from_drn(file): """ - Build a parametric model from the explicit DRN representation. + Build a parametric model in sparse representation from the explicit DRN representation. :param String file: DRN file containing the model. :return: Parametric model in sparse representation. - :rtype: SparseParametricDtmc or SparseParametricMdp or SparseParametricCTMC or SparseParametricMA """ intermediate = core._build_sparse_parametric_model_from_drn(file) - assert intermediate.supports_parameters - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_pmdp() - elif intermediate.model_type == ModelType.CTMC: - return intermediate._as_pctmc() - elif intermediate.model_type == ModelType.MA: - return intermediate._as_pma() - else: - raise StormError("Not supported parametric model constructed") + return _convert_sparse_model(intermediate, parametric=True) + def perform_bisimulation(model, properties, bisimulation_type): diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 4fd3cbd..9907378 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -20,6 +20,7 @@ PYBIND11_MODULE(storage, m) { define_bitvector(m); define_model(m); + define_sparse_model(m); define_sparse_matrix(m); define_state(m); define_prism(m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index ec3d43f..9d0993b 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -13,22 +13,22 @@ #include #include +// Typedefs +using RationalFunction = storm::RationalFunction; +using state_type = storm::storage::sparse::state_type; +template using SparseRewardModel = storm::models::sparse::StandardRewardModel; using ModelBase = storm::models::ModelBase; -using state_type = storm::storage::sparse::state_type; -using RationalFunction = storm::RationalFunction; -using RationalFunctionVariable = storm::RationalFunctionVariable; -template using Model = storm::models::sparse::Model; -template using Dtmc = storm::models::sparse::Dtmc; -template using Mdp = storm::models::sparse::Mdp; -template using Ctmc = storm::models::sparse::Ctmc; -template using MarkovAutomaton = storm::models::sparse::MarkovAutomaton; -template using SparseMatrix = storm::storage::SparseMatrix; -template using RewardModel = storm::models::sparse::StandardRewardModel; +template using SparseModel = storm::models::sparse::Model; +template using SparseDtmc = storm::models::sparse::Dtmc; +template using SparseMdp = storm::models::sparse::Mdp; +template using SparseCtmc = storm::models::sparse::Ctmc; +template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; + // Thin wrapper for getting initial states template -std::vector getInitialStates(Model const& model) { +std::vector getInitialStates(SparseModel const& model) { std::vector initialStates; for (auto entry : model.getInitialStates()) { initialStates.push_back(entry); @@ -38,28 +38,28 @@ std::vector getInitialStates(Model const& model) { // Thin wrapper for getting transition matrix template -SparseMatrix& getTransitionMatrix(Model& model) { +storm::storage::SparseMatrix& getTransitionMatrix(SparseModel& model) { return model.getTransitionMatrix(); } template -storm::storage::SparseMatrix getBackwardTransitionMatrix(storm::models::sparse::Model& model) { - return model.getBackwardTransitions(); +storm::storage::SparseMatrix getBackwardTransitionMatrix(SparseModel const& model) { + return std::move(model.getBackwardTransitions()); } // requires pycarl.Variable -std::set probabilityVariables(Model const& model) { +std::set probabilityVariables(SparseModel const& model) { return storm::models::sparse::getProbabilityParameters(model); } -std::set rewardVariables(Model const& model) { +std::set rewardVariables(SparseModel const& model) { return storm::models::sparse::getRewardParameters(model); } template -std::function const&)> getModelInfoPrinter(std::string name = "Model") { +std::function const&)> getModelInfoPrinter(std::string name = "Model") { // look, C++ has lambdas and stuff! - return [name](Model const& model) { + return [name](storm::models::Model const& model) { std::stringstream ss; model.printModelInformationToStream(ss); @@ -75,11 +75,12 @@ std::function const&)> getModelInfoPrinter(std::st } template -storm::models::sparse::StateLabeling& getLabeling(storm::models::sparse::Model& model) { +storm::models::sparse::StateLabeling& getLabeling(SparseModel& model) { return model.getStateLabeling(); } -// Define python bindings + +// Bindings for general models void define_model(py::module& m) { // ModelType @@ -98,116 +99,121 @@ void define_model(py::module& m) { .def_property_readonly("supports_parameters", &ModelBase::supportsParameters, "Flag whether model supports parameters") .def_property_readonly("has_parameters", &ModelBase::hasParameters, "Flag whether model has parameters") .def_property_readonly("is_exact", &ModelBase::isExact, "Flag whether model is exact") - .def("_as_dtmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as DTMC") - .def("_as_pdtmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pDTMC") - .def("_as_mdp", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as MDP") - .def("_as_pmdp", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pMDP") - .def("_as_ctmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as CTMC") - .def("_as_pctmc", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pCTMC") - .def("_as_ma", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as MA") - .def("_as_pma", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as pMA") + .def("_as_sparse_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse DTMC") + .def("_as_sparse_pdtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pDTMC") + .def("_as_sparse_mdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse MDP") + .def("_as_sparse_pmdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pMDP") + .def("_as_sparse_ctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse CTMC") + .def("_as_sparse_pctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pCTMC") + .def("_as_sparse_ma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse MA") + .def("_as_sparse_pma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pMA") + .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic DTMC") ; +} + + +// Bindings for sparse models +void define_sparse_model(py::module& m) { + // Models - py::class_, std::shared_ptr>> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", modelBase); + py::class_, std::shared_ptr>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); model.def_property_readonly("labeling", &getLabeling, "Labels") - .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") - .def_property_readonly("states", [](Model& model) { + .def_property_readonly("states", [](SparseModel& model) { return SparseModelStates(model); }, "Get states") - .def_property_readonly("reward_models", [](Model& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") - .def("reduce_to_state_based_rewards", &Model::reduceToStateBasedRewards) + .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter()) ; - py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) .def("__str__", getModelInfoPrinter("DTMC")) ; - py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", model) .def("__str__", getModelInfoPrinter("MDP")) ; - py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) .def("__str__", getModelInfoPrinter("CTMC")) ; - py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) + py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) .def("__str__", getModelInfoPrinter("MA")) ; - py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") - .def_property_readonly("has_state_rewards", &RewardModel::hasStateRewards) - .def_property_readonly("has_state_action_rewards", &RewardModel::hasStateActionRewards) - .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) - .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) - .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) - .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") - ; - + py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") + .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) + .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) + .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") + ; - 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); + py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix"); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") - .def_property_readonly("labeling", &getLabeling, "Labels") - .def("labels_state", &Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("labeling", &getLabeling, "Labels") + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getInitialStates, "Initial states") - .def_property_readonly("states", [](Model& model) { - return SparseModelStates(model); + .def_property_readonly("states", [](SparseModel& model) { + return SparseModelStates(model); }, "Get states") - .def_property_readonly("reward_models", [](Model const& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("reward_models", [](SparseModel const& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") - .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") - .def("reduce_to_state_based_rewards", &Model::reduceToStateBasedRewards) + .def_property_readonly("backward_transition_matrix", &getBackwardTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) .def("__str__", getModelInfoPrinter("ParametricModel")) ; - py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricDTMC")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricMDP")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricCTMC")) ; - - py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) + py::class_, std::shared_ptr>>(m, "SparseParametricMA", "pMA in sparse representation", modelRatFunc) .def("__str__", getModelInfoPrinter("ParametricMA")) ; - py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") - .def_property_readonly("has_state_rewards", &RewardModel::hasStateRewards) - .def_property_readonly("has_state_action_rewards", &RewardModel::hasStateActionRewards) - .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) - .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) - .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) - .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") + py::class_>(m, "SparseParametricRewardModel", "Reward structure for parametric sparse models") + .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) + .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) + .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; } diff --git a/src/storage/model.h b/src/storage/model.h index c779f26..ac91a56 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -4,5 +4,6 @@ #include "common.h" void define_model(py::module& m); +void define_sparse_model(py::module& m); #endif /* PYTHON_STORAGE_MODEL_H_ */