@ -315,11 +317,13 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) {
// Models with double numbers
// Models with double numbers
py::class_<SymbolicModel<DdType,double>,std::shared_ptr<SymbolicModel<DdType,double>>,ModelBase>model(m,("_"+prefixClassName+"Model").c_str(),"A probabilistic model where transitions are represented by doubles and saved in a symbolic representation");
py::class_<SymbolicModel<DdType,double>,std::shared_ptr<SymbolicModel<DdType,double>>,ModelBase>model(m,("_"+prefixClassName+"Model").c_str(),"A probabilistic model where transitions are represented by doubles and saved in a symbolic representation");
.def_property_readonly("reachable_states",&SymbolicModel<DdType,double>::getReachableStates,"reachable states as DD")
.def_property_readonly("reachable_states",&SymbolicModel<DdType,double>::getReachableStates,"reachable states as DD")
.def_property_readonly("initial_states",&SymbolicModel<DdType,double>::getInitialStates,"initial states as DD")
.def_property_readonly("initial_states",&SymbolicModel<DdType,double>::getInitialStates,"initial states as DD")
.def("get_states",[](SymbolicModel<DdType,double>const&model,storm::expressions::Expressionconst&expr){returnmodel.getStates(expr);},py::arg("expression"),"Get states that are described by the expression")
.def("get_states",[](SymbolicModel<DdType,double>const&model,storm::expressions::Expressionconst&expr){returnmodel.getStates(expr);},py::arg("expression"),"Get states that are described by the expression")
.def("compute_depth",[](SymbolicModel<DdType,double>const&model){returnstorm::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("compute_depth",[](SymbolicModel<DdType,double>const&model){returnstorm::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")
py::class_<SymbolicDtmc<DdType,double>,std::shared_ptr<SymbolicDtmc<DdType,double>>>(m,(prefixClassName+"Dtmc").c_str(),"DTMC in symbolic representation",model)
py::class_<SymbolicDtmc<DdType,double>,std::shared_ptr<SymbolicDtmc<DdType,double>>>(m,(prefixClassName+"Dtmc").c_str(),"DTMC in symbolic representation",model)