diff --git a/src/storage/dd.cpp b/src/storage/dd.cpp index 09b5a39..02e5f40 100644 --- a/src/storage/dd.cpp +++ b/src/storage/dd.cpp @@ -1,5 +1,6 @@ #include "dd.h" #include "storm/storage/dd/DdManager.h" +#include "storm/storage/dd/DdMetaVariable.h" #include "storm/storage/dd/Dd.h" #include "storm/storage/dd/Bdd.h" #include "src/helpers.h" @@ -9,9 +10,11 @@ void define_dd(py::module& m, std::string const& libstring) { py::class_> ddMetaVariable(m, (std::string("DdMetaVariable_") + libstring).c_str()); ddMetaVariable.def("compute_indices", &storm::dd::DdMetaVariable::getIndices, py::arg("sorted")=true); ddMetaVariable.def_property_readonly("name", &storm::dd::DdMetaVariable::getName); + ddMetaVariable.def_property_readonly("lowest_value", &storm::dd::DdMetaVariable::getLow); + ddMetaVariable.def("__str__", &storm::dd::DdMetaVariable::getName); py::class_, std::shared_ptr>> ddManager(m, (std::string("DdManager_") + libstring).c_str()); - //ddManager.def("get_meta_variable", &storm::dd::DdManager::getMetaVariable, py::arg("expression_variable")); + ddManager.def("get_meta_variable", [](storm::dd::DdManager const& manager, storm::expressions::Variable const& var) {return manager.getMetaVariable(var);}, py::arg("expression_variable")); py::class_> dd(m, (std::string("Dd_") + libstring).c_str(), "Dd"); dd.def_property_readonly("node_count", &storm::dd::Dd::getNodeCount, "get node count"); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 4fd4d0d..19f1fc5 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -17,6 +17,8 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/utility/dd.h" +#include "storm/storage/dd/DdManager.h" + #include "storm/storage/Scheduler.h" #include @@ -315,11 +317,13 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { // 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_property_readonly("reachable_states", &SymbolicModel::getReachableStates, "reachable states as DD") + .def_property_readonly("dd_manager", &SymbolicModel::getManager, "dd manager") + .def_property_readonly("reachable_states", &SymbolicModel::getReachableStates, "reachable states as DD") .def_property_readonly("initial_states", &SymbolicModel::getInitialStates, "initial states as DD") .def("get_states", [](SymbolicModel const& model, storm::expressions::Expression const& expr) {return model.getStates(expr);}, py::arg("expression"), "Get states that are described by the expression") .def("compute_depth", [](SymbolicModel const& model) {return storm::utility::dd::computeReachableStates(model.getInitialStates(), model.getQualitativeTransitionMatrix(false), model.getRowVariables(), model.getColumnVariables()).second;}, "Computes the depth of the model, i.e., the distance to the node with the largest minimal distance from the initial states") .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)