From 21ecfacc3b69e2f3a6ec5c7c30fe5a6626561d2c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 17 May 2018 17:49:44 +0200 Subject: [PATCH] Bindings for symbolic models using Sylvan --- src/mod_storage.cpp | 3 ++ src/storage/model.cpp | 105 +++++++++++++++++++++++++++++++++++++++++- src/storage/model.h | 3 ++ 3 files changed, 110 insertions(+), 1 deletion(-) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 9907378..a8d3089 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -10,6 +10,8 @@ #include "storage/labeling.h" #include "storage/expressions.h" +#include "storm/storage/dd/DdType.h" + PYBIND11_MODULE(storage, m) { m.doc() = "Data structures in Storm"; @@ -22,6 +24,7 @@ PYBIND11_MODULE(storage, m) { define_model(m); define_sparse_model(m); define_sparse_matrix(m); + define_symbolic_model(m, "Sylvan"); define_state(m); define_prism(m); define_labeling(m); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index c185ae6..f2f49a1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -8,6 +8,12 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/symbolic/Model.h" +#include "storm/models/symbolic/Dtmc.h" +#include "storm/models/symbolic/Mdp.h" +#include "storm/models/symbolic/Ctmc.h" +#include "storm/models/symbolic/MarkovAutomaton.h" +#include "storm/models/symbolic/StandardRewardModel.h" #include #include @@ -24,6 +30,13 @@ template using SparseCtmc = storm::models::sparse::Ctmc using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; template using SparseRewardModel = storm::models::sparse::StandardRewardModel; +template using SymbolicModel = storm::models::symbolic::Model; +template using SymbolicDtmc = storm::models::symbolic::Dtmc; +template using SymbolicMdp = storm::models::symbolic::Mdp; +template using SymbolicCtmc = storm::models::symbolic::Ctmc; +template using SymbolicMarkovAutomaton = storm::models::symbolic::MarkovAutomaton; +template using SymbolicRewardModel = storm::models::symbolic::StandardRewardModel; + // Thin wrappers @@ -117,7 +130,30 @@ void define_model(py::module& m) { .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") + .def("_as_symbolic_pdtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pDTMC") + .def("_as_symbolic_mdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic MDP") + .def("_as_symbolic_pmdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pMDP") + .def("_as_symbolic_ctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic CTMC") + .def("_as_symbolic_pctmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pCTMC") + .def("_as_symbolic_ma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic MA") + .def("_as_symbolic_pma", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as symbolic pMA") ; } @@ -210,3 +246,70 @@ void define_sparse_model(py::module& m) { } + +// Bindings for symbolic models +template +void define_symbolic_model(py::module& m, std::string vt_suffix) { + + // Set class names + std::string prefixClassName = "Symbolic" + vt_suffix; + std::string prefixParametricClassName = "Symbolic" + vt_suffix + "Parametric"; + + + // Models with double numbers + py::class_, std::shared_ptr>, ModelBase> model(m, ("_"+prefixClassName+"Model").c_str(), "A probabilistic model where transitions are represented by doubles and saved in a symbolic representation"); + model.def_property_readonly("reward_models", [](SymbolicModel& model) {return model.getRewardModels(); }, "Reward models") + .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) + .def("__str__", getModelInfoPrinter()) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Dtmc").c_str(), "DTMC in symbolic representation", model) + .def("__str__", getModelInfoPrinter("DTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Mdp").c_str(), "MDP in symbolic representation", model) + .def("__str__", getModelInfoPrinter("MDP")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"Ctmc").c_str(), "CTMC in symbolic representation", model) + .def("__str__", getModelInfoPrinter("CTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixClassName+"MA").c_str(), "MA in symbolic representation", model) + .def("__str__", getModelInfoPrinter("MA")) + ; + + py::class_>(m, (prefixClassName+"RewardModel").c_str(), "Reward structure for symbolic models") + .def_property_readonly("has_state_rewards", &SymbolicRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SymbolicRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SymbolicRewardModel::hasTransitionRewards) + ; + + + // Parametric models + py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, ("_"+prefixParametricClassName+"Model").c_str(), "A probabilistic model where transitions are represented by rational functions and saved in a symbolic representation"); + modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") + .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters") + .def_property_readonly("reward_models", [](SymbolicModel const& model) {return model.getRewardModels(); }, "Reward models") + .def("reduce_to_state_based_rewards", &SymbolicModel::reduceToStateBasedRewards) + .def("__str__", getModelInfoPrinter("ParametricModel")) + ; + + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Dtmc").c_str(), "pDTMC in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricDTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Mdp").c_str(), "pMDP in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricMDP")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"Ctmc").c_str(), "pCTMC in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricCTMC")) + ; + py::class_, std::shared_ptr>>(m, (prefixParametricClassName+"MA").c_str(), "pMA in symbolic representation", modelRatFunc) + .def("__str__", getModelInfoPrinter("ParametricMA")) + ; + + py::class_>(m, (prefixParametricClassName+"RewardModel").c_str(), "Reward structure for parametric symbolic models") + .def_property_readonly("has_state_rewards", &SymbolicRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SymbolicRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SymbolicRewardModel::hasTransitionRewards) + ; + +} + +template void define_symbolic_model(py::module& m, std::string vt_suffix); diff --git a/src/storage/model.h b/src/storage/model.h index 50f4c31..7643d39 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -1,7 +1,10 @@ #pragma once #include "common.h" +#include "storm/storage/dd/DdType.h" void define_model(py::module& m); void define_sparse_model(py::module& m); +template +void define_symbolic_model(py::module& m, std::string vt_suffix);