From d9e0a9ac923ac919a3b1f8cdf99ce0b39aecbc17 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 13 Jun 2020 18:13:58 -0700 Subject: [PATCH] compute the depth of the model, i.e., the longest shortest path from an initial state --- src/storage/model.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 74d8516..b978c51 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -15,6 +15,7 @@ #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/MarkovAutomaton.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/utility/dd.h" #include "storm/storage/Scheduler.h" @@ -305,6 +306,7 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { .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) ;