diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index b8f696890..50b77c3f4 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -28,17 +28,23 @@ void define_parse(py::module& m) { m.def("parse_explicit_model", &storm::parser::AutoParser<>::parseModel, "Parse explicit model", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); } -// Thin wrapper for model building +// Thin wrapper for model building using one formula as argument template std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { return storm::buildSymbolicModel(program, std::vector>(1,formula)); } +template +std::shared_ptr buildSparseModel(storm::prism::Program const& program, std::shared_ptr const& formula, + bool onlyInitialStatesRelevant = false) { + return storm::buildSparseModel(program, std::vector>(1,formula), onlyInitialStatesRelevant); +} + void define_build(py::module& m) { // Build model m.def("_build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula")); - m.def("_build_parametric_model", &buildModel, "Build the parametric model", py::arg("program"), py::arg("formula")); + m.def("_build_parametric_model", &buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false); m.def("build_model_from_prism_program", &storm::buildSymbolicModel, "Build the model", py::arg("program"), py::arg("formulas")); - m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "Build the parametric model", py::arg("program"), py::arg("formulas")); + m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false); }