From fcc27ae46327bfa95f39f5850e768ed8b2c63314 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2026 15:04:24 +0200 Subject: [PATCH 1/3] Adaption to ExtendedNumber --- src/core/result.cpp | 14 ++++++++++---- src/dft/analysis.cpp | 6 ++++-- src/pars/pla.cpp | 10 ++++++---- 3 files changed, 20 insertions(+), 10 deletions(-) diff --git a/src/core/result.cpp b/src/core/result.cpp index e69eb153a..55368c39b 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -8,6 +8,7 @@ #include #include #include +#include template std::shared_ptr createFilterInitialStatesSparse(std::shared_ptr> model) { @@ -94,8 +95,13 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { py::classh, storm::modelchecker::CheckResult> quantitativeCheckResult( m, ("_" + vtSuffix + "QuantitativeCheckResult").c_str(), "Abstract class for quantitative model checking results"); - quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult::getMin, "Minimal value") - .def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult::getMax, "Maximal value"); + quantitativeCheckResult + .def_property_readonly( + "min", [](storm::modelchecker::QuantitativeCheckResult const& res) { return storm::utility::narrow(res.getMin()); }, + "Minimal value") + .def_property_readonly( + "max", [](storm::modelchecker::QuantitativeCheckResult const& res) { return storm::utility::narrow(res.getMax()); }, + "Maximal value"); py::classh>(m, ("Explicit" + vtSuffix + "QuantitativeCheckResult").c_str(), "Explicit quantitative model checking result", quantitativeCheckResult) @@ -103,11 +109,11 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { .def( "at", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& result, storm::storage::sparse::state_type state) { - return result[state]; + return storm::utility::narrow(result[state]); }, py::arg("state"), "Get result for given state") .def( - "get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) { return res.getValueVector(); }, + "get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) { return res.getFiniteValueVector(); }, "Get model checking result values for all states") .def_property_readonly( "scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult const& res) { return res.getScheduler(); }, "get scheduler"); diff --git a/src/dft/analysis.cpp b/src/dft/analysis.cpp index 498e563ba..820b6e875 100644 --- a/src/dft/analysis.cpp +++ b/src/dft/analysis.cpp @@ -6,6 +6,7 @@ #include #include #include +#include template using ExplicitDFTModelBuilder = storm::dft::builder::ExplicitDFTModelBuilder; @@ -18,8 +19,9 @@ std::vector analyzeDFT(storm::dft::storage::DFT const& dft dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::dft::builder::ApproximationHeuristic::DEPTH, false); std::vector results; - for (auto result : dftResults) { - results.push_back(boost::get(result)); + for (auto const& result : dftResults) { + results.push_back( + storm::utility::narrow(boost::get::ExtendedValueType>(result))); } return results; } diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index b8742032d..b5aee3164 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -5,6 +5,7 @@ #include #include #include +#include #include "src/helpers.h" @@ -65,8 +66,8 @@ storm::modelchecker::RegionResult checkRegion(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { - return checker->getBoundAtInitState(env, region, - maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); + return storm::utility::narrow( + checker->getBoundAtInitState(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)); } storm::modelchecker::ExplicitQuantitativeCheckResult getBound_dtmc(std::shared_ptr& checker, @@ -158,8 +159,9 @@ void define_pla(py::module& m) { "compute_extremum", [](RegionRefinementChecker& r, storm::Environment const& env, Region const& region, storm::solver::OptimizationDirection const& dirForParameters, storm::RationalFunctionCoefficient const& precision, bool absolutePrecision) { - return r.computeExtremalValue(env, region, dirForParameters, storm::utility::one() * precision, absolutePrecision, - std::nullopt); + auto [value, point] = r.computeExtremalValue(env, region, dirForParameters, storm::utility::one() * precision, + absolutePrecision, std::nullopt); + return std::make_pair(storm::utility::narrow(value), std::move(point)); }, "Compute extremum value and point with precision", py::arg("environment"), py::arg("region"), py::arg("extremum_direction"), py::arg("precision"), py::arg("precision_absolute") = false); From 0eec41528fcb1909ce8da383300f7902db8620d8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2026 15:34:02 +0200 Subject: [PATCH 2/3] Adaption to environment in InstatiationChecker --- src/pars/model_instantiator.cpp | 3 ++- tests/pars/test_model_instantiator.py | 12 ++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp index 39e3ae138..ec3c74581 100644 --- a/src/pars/model_instantiator.cpp +++ b/src/pars/model_instantiator.cpp @@ -5,6 +5,7 @@ #include #include #include +#include #include #include #include @@ -84,7 +85,7 @@ void define_typed_checker(py::module& m, const char* baseName, const char* baseD base.def("specify_formula", &BaseChecker::specifyFormula, "check_task"_a); py::classh(m, derivedName, derivedDesc, base) - .def(py::init(), "parametric model"_a) + .def(py::init(), "environment"_a, "parametric model"_a) .def( "check", [](CheckerType& c, storm::Environment const& env, diff --git a/tests/pars/test_model_instantiator.py b/tests/pars/test_model_instantiator.py index 5174367ac..d4a29d932 100644 --- a/tests/pars/test_model_instantiator.py +++ b/tests/pars/test_model_instantiator.py @@ -69,10 +69,10 @@ def test_pdtmc_instantiation_checker(self): model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_all_parameters() - inst_checker = stormpy.pars.PDtmcInstantiationChecker(model) + env = stormpy.Environment() + inst_checker = stormpy.pars.PDtmcInstantiationChecker(env, model) inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) - env = stormpy.Environment() point = {p: stormpy.RationalRF(1 / 2) for p in parameters} result = inst_checker.check(env, point) @@ -87,10 +87,10 @@ def test_pdtmc_exact_instantiation_checker(self): model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_all_parameters() - inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(model) + env = stormpy.Environment() + inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(env, model) inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) - env = stormpy.Environment() point = {p: stormpy.RationalRF("1/2") for p in parameters} result = inst_checker.check(env, point) @@ -105,10 +105,10 @@ def test_pdtmc_exact_instantiation_checker_die(self): model = stormpy.build_parametric_model(program, formulas) parameters = model.collect_all_parameters() - inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(model) + env = stormpy.Environment() + inst_checker = stormpy.pars.PDtmcExactInstantiationChecker(env, model) inst_checker.specify_formula(stormpy.ParametricCheckTask(formulas[0].raw_formula, True)) inst_checker.set_graph_preserving(True) - env = stormpy.Environment() point = {p: stormpy.RationalRF("2/5") for p in parameters} result = inst_checker.check(env, point) From ac0a07997527f5dfb36a40f2f906daf9e71f3b11 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2026 15:35:42 +0200 Subject: [PATCH 3/3] Removed Environment as default argument --- src/core/core.cpp | 4 ++-- src/core/modelchecking.cpp | 23 +++++++++++------------ 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/src/core/core.cpp b/src/core/core.cpp index 1583302cd..bab1e5352 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -157,7 +157,7 @@ void define_build_sparse_model_defs(py::module& m) { if constexpr (std::is_same_v) { m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, "Build the model in symbolic representation", py::arg("model_description"), - py::arg("formulas") = std::vector>(), py::arg("environment") = storm::Environment()); + py::arg("formulas") = std::vector>(), py::arg("environment")); 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") = "", py::arg("options") = storm::parser::ExplicitModelParserOptions()); @@ -170,7 +170,7 @@ void define_build_sparse_model_defs(py::module& m) { } else if constexpr (std::is_same_v) { m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, "Build the parametric model in symbolic representation", py::arg("model_description"), - py::arg("formulas") = std::vector>(), py::arg("environment") = storm::Environment()); + py::arg("formulas") = std::vector>(), py::arg("environment")); m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr, py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder::Options()); diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 46760db09..072781877 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -161,14 +161,13 @@ void define_modelchecking_mdefs(py::module& m) { py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); m.def("_compute_expected_number_of_visits_double", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); m.def("_compute_steady_state_distribution_double", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); - m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), - py::arg("environment") = storm::Environment()); + m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), - py::arg("task"), py::arg("environment") = storm::Environment()); + py::arg("task"), py::arg("environment")); m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", - py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine, "Perform model checking using the hybrid engine", - py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_min_double", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"), @@ -176,27 +175,27 @@ void define_modelchecking_mdefs(py::module& m) { m.def("_compute_prob01states_max_double", &computeProb01max, "Compute prob-0-1 states (max)", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_multi_objective_model_checking_double", &multiObjectiveModelChecking, "Run multi-objective model checking", py::arg("model"), - py::arg("formula"), py::arg("environment") = storm::Environment()); + py::arg("formula"), py::arg("environment")); } else if constexpr (std::is_same_v) { m.def("_get_reachable_states_exact", &getReachableStates, py::arg("model"), py::arg("initial_states"), py::arg("constraint_states"), py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); m.def("_compute_expected_number_of_visits_exact", &getExpectedNumberOfVisits, py::arg("env"), py::arg("model")); m.def("_compute_steady_state_distribution_exact", &getSteadyStateDistribution, py::arg("env"), py::arg("model")); m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), - py::arg("environment") = storm::Environment()); + py::arg("environment")); m.def("_exact_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", - py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_multi_objective_model_checking_exact", &multiObjectiveModelChecking, "Run multi-objective model checking", - py::arg("model"), py::arg("formula"), py::arg("environment") = storm::Environment()); + py::arg("model"), py::arg("formula"), py::arg("environment")); } else if constexpr (std::is_same_v) { m.def("_get_reachable_states_rf", &getReachableStates, py::arg("model"), py::arg("initial_states"), py::arg("constraint_states"), py::arg("target_states"), py::arg("maximal_steps") = boost::none, py::arg("choice_filter") = boost::none); m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, - "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, - "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine, - "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment")); m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_min_rationalfunc", &computeProb01min, "Compute prob-0-1 states (min)", py::arg("model"),