Skip to content

Adaption to Environment and ExtendedNumber #453

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
volkm merged 3 commits into from
Sep 9, 2026
Merged

Adaption to Environment and ExtendedNumber #453

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
fcc27ae
Adaption to ExtendedNumber
volkm Sep 7, 2026
0eec415
Adaption to environment in InstatiationChecker
volkm Sep 7, 2026
ac0a079
Removed Environment as default argument
volkm Sep 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/core/core.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ void define_build_sparse_model_defs(py::module& m) {
if constexpr (std::is_same_v<ValueType, double>) {
m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>,
"Build the model in symbolic representation", py::arg("model_description"),
py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("environment") = storm::Environment());
py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("environment"));
m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "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());
Expand All @@ -170,7 +170,7 @@ void define_build_sparse_model_defs(py::module& m) {
} else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>,
"Build the parametric model in symbolic representation", py::arg("model_description"),
py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("environment") = storm::Environment());
py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("environment"));
m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<storm::RationalFunction>, "Construct a builder instance",
py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr,
py::arg("exploration_options") = typename storm::builder::ExplicitModelBuilder<ValueType>::Options());
Expand Down
23 changes: 11 additions & 12 deletions src/core/modelchecking.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,42 +161,41 @@ 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<double>, py::arg("env"), py::arg("model"));
m.def("_compute_steady_state_distribution_double", &getSteadyStateDistribution<double>, py::arg("env"), py::arg("model"));
m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<double>, py::arg("model"), py::arg("task"),
py::arg("environment") = storm::Environment());
m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<double>, py::arg("model"), py::arg("task"), py::arg("environment"));
m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "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<storm::dd::DdType::Sylvan, double>, "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<storm::dd::DdType::Sylvan, double>, "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<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"),
py::arg("psi_states"));
m.def("_compute_prob01states_min_double", &computeProb01min<double>, "Compute prob-0-1 states (min)", py::arg("model"), py::arg("phi_states"),
py::arg("psi_states"));
m.def("_compute_prob01states_max_double", &computeProb01max<double>, "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<double>, "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<ValueType, storm::RationalNumber>) {
m.def("_get_reachable_states_exact", &getReachableStates<storm::RationalNumber>, 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<storm::RationalNumber>, py::arg("env"), py::arg("model"));
m.def("_compute_steady_state_distribution_exact", &getSteadyStateDistribution<storm::RationalNumber>, py::arg("env"), py::arg("model"));
m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<storm::RationalNumber>, py::arg("model"), py::arg("task"),
py::arg("environment") = storm::Environment());
py::arg("environment"));
m.def("_exact_model_checking_sparse_engine", &modelCheckingSparseEngine<storm::RationalNumber>, "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<storm::RationalNumber>, "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<ValueType, storm::RationalFunction>) {
m.def("_get_reachable_states_rf", &getReachableStates<storm::RationalFunction>, 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<storm::RationalFunction>,
"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<storm::dd::DdType::Sylvan, storm::RationalFunction>,
"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<storm::dd::DdType::Sylvan, storm::RationalFunction>,
"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<storm::RationalFunction>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"),
py::arg("psi_states"));
m.def("_compute_prob01states_min_rationalfunc", &computeProb01min<storm::RationalFunction>, "Compute prob-0-1 states (min)", py::arg("model"),
Expand Down
14 changes: 10 additions & 4 deletions src/core/result.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include <storm/modelchecker/results/SymbolicQualitativeCheckResult.h>
#include <storm/modelchecker/results/SymbolicQuantitativeCheckResult.h>
#include <storm/models/symbolic/StandardRewardModel.h>
#include <storm/utility/ExtendedNumber.h>

template<typename ValueType>
std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterInitialStatesSparse(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) {
Expand Down Expand Up @@ -94,20 +95,25 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) {

py::classh<storm::modelchecker::QuantitativeCheckResult<ValueType>, storm::modelchecker::CheckResult> quantitativeCheckResult(
m, ("_" + vtSuffix + "QuantitativeCheckResult").c_str(), "Abstract class for quantitative model checking results");
quantitativeCheckResult.def_property_readonly("min", &storm::modelchecker::QuantitativeCheckResult<ValueType>::getMin, "Minimal value")
.def_property_readonly("max", &storm::modelchecker::QuantitativeCheckResult<ValueType>::getMax, "Maximal value");
quantitativeCheckResult
.def_property_readonly(
"min", [](storm::modelchecker::QuantitativeCheckResult<ValueType> const& res) { return storm::utility::narrow<ValueType>(res.getMin()); },
"Minimal value")
.def_property_readonly(
"max", [](storm::modelchecker::QuantitativeCheckResult<ValueType> const& res) { return storm::utility::narrow<ValueType>(res.getMax()); },
"Maximal value");

py::classh<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(m, ("Explicit" + vtSuffix + "QuantitativeCheckResult").c_str(),
"Explicit quantitative model checking result", quantitativeCheckResult)
.def(py::init<std::vector<ValueType>>(), py::arg("values"))
.def(
"at",
[](storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& result, storm::storage::sparse::state_type state) {
return result[state];
return storm::utility::narrow<ValueType>(result[state]);
},
py::arg("state"), "Get result for given state")
.def(
"get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& res) { return res.getValueVector(); },
"get_values", [](storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& res) { return res.getFiniteValueVector(); },
"Get model checking result values for all states")
.def_property_readonly(
"scheduler", [](storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType> const& res) { return res.getScheduler(); }, "get scheduler");
Expand Down
6 changes: 4 additions & 2 deletions src/dft/analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
#include <storm-dft/parser/DFTJsonParser.h>
#include <storm-dft/storage/DftSymmetries.h>
#include <storm/adapters/RationalFunctionAdapter.h>
#include <storm/utility/ExtendedNumber.h>

template<typename ValueType>
using ExplicitDFTModelBuilder = storm::dft::builder::ExplicitDFTModelBuilder<ValueType>;
Expand All @@ -18,8 +19,9 @@ std::vector<ValueType> analyzeDFT(storm::dft::storage::DFT<ValueType> const& dft
dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevant, 0.0, storm::dft::builder::ApproximationHeuristic::DEPTH, false);

std::vector<ValueType> results;
for (auto result : dftResults) {
results.push_back(boost::get<ValueType>(result));
for (auto const& result : dftResults) {
results.push_back(
storm::utility::narrow<ValueType>(boost::get<typename storm::dft::modelchecker::DFTModelChecker<ValueType>::ExtendedValueType>(result)));
}
return results;
}
Expand Down
3 changes: 2 additions & 1 deletion src/pars/model_instantiator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#include <storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h>
#include <storm-pars/transformer/SparseParametricDtmcSimplifier.h>
#include <storm/adapters/RationalFunctionAdapter.h>
#include <storm/environment/Environment.h>
#include <storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h>
#include <storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h>
#include <storm/modelchecker/propositional/SparsePropositionalModelChecker.h>
Expand Down Expand Up @@ -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<CheckerType>(m, derivedName, derivedDesc, base)
.def(py::init<ModelType>(), "parametric model"_a)
.def(py::init<storm::Environment, ModelType>(), "environment"_a, "parametric model"_a)
.def(
"check",
[](CheckerType& c, storm::Environment const& env,
Expand Down
10 changes: 6 additions & 4 deletions src/pars/pla.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
#include <storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h>
#include <storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h>
#include <storm/api/verification.h>
#include <storm/utility/ExtendedNumber.h>

#include "src/helpers.h"

Expand Down Expand Up @@ -65,8 +66,8 @@ storm::modelchecker::RegionResult checkRegion(std::shared_ptr<RegionModelChecker
}

Region::CoefficientType getBoundAtInit(std::shared_ptr<RegionModelChecker>& 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<Region::CoefficientType>(
checker->getBoundAtInitState(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize));
}

storm::modelchecker::ExplicitQuantitativeCheckResult<double> getBound_dtmc(std::shared_ptr<DtmcParameterLiftingModelChecker>& checker,
Expand Down Expand Up @@ -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<storm::RationalFunction>() * precision, absolutePrecision,
std::nullopt);
auto [value, point] = r.computeExtremalValue(env, region, dirForParameters, storm::utility::one<storm::RationalFunction>() * precision,
absolutePrecision, std::nullopt);
return std::make_pair(storm::utility::narrow<Region::CoefficientType>(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);
Expand Down
12 changes: 6 additions & 6 deletions tests/pars/test_model_instantiator.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down
Loading