diff --git a/src/core/core.cpp b/src/core/core.cpp index fa6fedc..d5f03be 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -47,14 +47,21 @@ void define_parse(py::module& m) { // Thin wrapper for model building using one formula as argument template -std::shared_ptr buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool buildChoiceLabels = false, bool buildChoiceOrigins = false) { - return storm::api::buildSparseModel(modelDescription, formulas, buildChoiceLabels, buildChoiceOrigins); +std::shared_ptr buildSparseModel(storm::storage::SymbolicModelDescription const& modelDescription, std::vector> const& formulas, bool jit = false, bool doctor = false) { + if (formulas.empty()) { + // Build all labels and rewards + storm::builder::BuilderOptions options(true, true); + return storm::api::buildSparseModel(modelDescription, options, jit, doctor); + } else { + // Only build labels necessary for formulas + return storm::api::buildSparseModel(modelDescription, formulas, jit, doctor); + } } void define_build(py::module& m) { // Build model - m.def("_build_sparse_model_from_prism_program", &buildSparseModel, "Build the model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("build_choice_labels") = false, py::arg("build_choice_origins") = false); - m.def("_build_sparse_parametric_model_from_prism_program", &buildSparseModel, "Build the parametric model", py::arg("model_description"), py::arg("formulas"), py::arg("build_choice_labels") = false, py::arg("build_choice_origins") = false); + m.def("_build_sparse_model_from_prism_program", &buildSparseModel, "Build the model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_parametric_model_from_prism_program", &buildSparseModel, "Build the parametric model", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file")); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file")); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 3a246c0..a17ea85 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -43,6 +43,21 @@ class TestModelChecking: result = stormpy.model_checking(model, formula) assert result is None + def test_model_checking_dtmc_all_labels(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 0.16666666666666663) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 0.16666666666666663) + def test_model_checking_all_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)