From a571d14491642a7a9926b2fcc09a30ebd903fcc0 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Tue, 21 Apr 2026 13:40:59 +0200 Subject: [PATCH 01/14] Add exact interval (RationalInterval) support Binds storm::RationalInterval throughout: sparse models, matrices, schedulers, model components, model checking, DRN build/export, and the Kwek-Mehlhorn sharpening utility. --- lib/stormpy/__init__.py | 22 ++++++++++++++++++++++ lib/stormpy/storage/__init__.py | 2 ++ src/core/core.cpp | 2 ++ src/core/modelchecking.cpp | 6 ++++++ src/mod_storage.cpp | 24 +++++++++++++++--------- src/mod_utility.cpp | 24 +++++++++++++----------- src/storage/decomposition.cpp | 1 + src/storage/distribution.cpp | 1 + src/storage/matrix.cpp | 1 + src/storage/model.cpp | 19 ++++++++++++++++--- src/storage/model_components.cpp | 2 ++ src/storage/state.cpp | 1 + src/storage/valuation.cpp | 2 +- src/utility/kwekMehlhorn.cpp | 22 ++++++++++++++++++++++ src/utility/kwekMehlhorn.h | 6 ++++++ 15 files changed, 111 insertions(+), 24 deletions(-) create mode 100644 src/utility/kwekMehlhorn.cpp create mode 100644 src/utility/kwekMehlhorn.h diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 02be704ce9..d132abebf8 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -312,6 +312,26 @@ def build_interval_model_from_drn(file, options=DirectEncodingParserOptions()): return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL) +def build_exact_interval_model_from_drn(file, options=DirectEncodingParserOptions()): + """ + Build an exact interval model in sparse representation from the explicit DRN representation. + + :param String file: DRN file containing the model. + :param DirectEncodingParserOptions: Options for the parser. + :return: Exact Interval model in sparse representation. + """ + intermediate = _core._build_sparse_exact_interval_model_from_drn(file, options) + assert intermediate.supports_uncertainty and intermediate.is_exact + if intermediate.model_type == ModelType.DTMC: + return intermediate._as_sparse_exact_idtmc() + elif intermediate.model_type == ModelType.MDP: + return intermediate._as_sparse_exact_imdp() + elif intermediate.model_type == ModelType.POMDP: + return intermediate._as_sparse_exact_ipomdp() + else: + raise StormError("Not supported exact interval model constructed") + + def perform_bisimulation(model, properties, bisimulation_type, graph_preserving=True): """ Perform bisimulation on model. @@ -741,6 +761,8 @@ def export_to_drn(model, file, options=DirectEncodingExporterOptions()): """ if model.supports_parameters: return _core._export_parametric_to_drn(model, file, options) + if model.supports_uncertainty and model.is_exact: + return _core._export_exact_to_drn_interval(model, file, options) if model.supports_uncertainty: return _core._export_to_drn_interval(model, file, options) if model.is_exact: diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index eea332c77f..cf2ad4a227 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -69,6 +69,8 @@ def get_maximal_end_components(model): """ if model.supports_parameters: return stormpy.MaximalEndComponentDecomposition_ratfunc(model) + elif model.supports_uncertainty and model.is_exact: + return stormpy.MaximalEndComponentDecomposition_ratinterval(model) elif model.is_exact: return stormpy.MaximalEndComponentDecomposition_exact(model) elif model.supports_uncertainty: diff --git a/src/core/core.cpp b/src/core/core.cpp index b93e53f1b2..173d9f559c 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -134,6 +134,7 @@ void define_build(py::module& m) { m.def("_build_sparse_exact_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); m.def("_build_sparse_interval_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the interval model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); + m.def("_build_sparse_exact_interval_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the exact interval model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); 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") = ""); m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr); @@ -207,6 +208,7 @@ void define_export(py::module& m) { // Export m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); m.def("_export_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); + m.def("_export_exact_to_drn_interval", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); m.def("_export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); m.def("_export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions()); } diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 5ebf428f76..804b5c2283 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -59,6 +59,11 @@ std::shared_ptr checkIntervalMdp(std::shared_p return checker.check(env, task); } +std::shared_ptr checkRationalIntervalMdp(std::shared_ptr> mdp, CheckTask const& task, storm::Environment& env) { + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); + return checker.check(env, task); +} + std::vector computeAllUntilProbabilities(storm::Environment const& env, CheckTask const& task, std::shared_ptr> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::solver::SolveGoal goal(*ctmc, task); return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllUntilProbabilities(env, std::move(goal), ctmc->getTransitionMatrix(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates); @@ -147,6 +152,7 @@ void define_modelchecking(py::module& m) { 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()); m.def("check_interval_dtmc", &checkIntervalDtmc, "Check interval DTMC"); m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP"); + m.def("check_exact_interval_mdp", &checkRationalIntervalMdp, "Check exact interval MDP"); m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities"); m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities"); m.def("_compute_prob01states_double", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index f88d6bf9ed..c4291e5374 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -1,22 +1,22 @@ #include "common.h" #include "storage/bitvector.h" +#include "storage/choiceorigins.h" #include "storage/dd.h" -#include "storage/model.h" #include "storage/decomposition.h" +#include "storage/distribution.h" +#include "storage/expressions.h" +#include "storage/geometry.h" +#include "storage/jani.h" +#include "storage/labeling.h" #include "storage/matrix.h" #include "storage/memorystructure.h" +#include "storage/model.h" #include "storage/model_components.h" -#include "storage/distribution.h" -#include "storage/scheduler.h" #include "storage/prism.h" -#include "storage/jani.h" +#include "storage/scheduler.h" #include "storage/state.h" #include "storage/valuation.h" -#include "storage/choiceorigins.h" -#include "storage/labeling.h" -#include "storage/expressions.h" -#include "storage/geometry.h" #include "storm/adapters/IntervalAdapter.h" #include "storm/storage/dd/DdType.h" @@ -37,12 +37,14 @@ PYBIND11_MODULE(_storage, m) { define_sparse_model(m, "Exact"); define_sparse_model(m, "Interval"); define_sparse_model(m, "Parametric"); + define_sparse_model(m, "RationalInterval"); define_statevaluation(m); define_statevaluation_transformer(m); define_simplevaluation(m); define_sparse_matrix(m, ""); define_sparse_matrix(m, "Exact"); define_sparse_matrix(m, "Interval"); + define_sparse_matrix(m, "RationalInterval"); define_sparse_matrix(m, "Parametric"); define_sparse_matrix_nt(m); define_symbolic_model(m, "Sylvan"); @@ -51,6 +53,7 @@ PYBIND11_MODULE(_storage, m) { define_state(m, ""); define_state(m, "Exact"); define_state(m, "Interval"); + define_state(m, "RationalInterval"); define_state(m, "Parametric"); define_memorystructure_typed(m, ""); define_memorystructure_typed(m, "Exact"); @@ -66,13 +69,16 @@ PYBIND11_MODULE(_storage, m) { define_scheduler(m, ""); define_scheduler(m, "Exact"); define_scheduler(m, "Interval"); + define_scheduler(m, "RationalInterval"); define_scheduler(m, "Parametric"); define_distribution(m, ""); define_distribution(m, "Exact"); define_distribution(m, "Interval"); + define_distribution(m, "RationalInterval"); define_sparse_model_components(m, ""); define_sparse_model_components(m, "Exact"); define_sparse_model_components(m, "Interval"); + define_sparse_model_components(m, "RationalInterval"); define_sparse_model_components(m, "Parametric"); define_geometry(m, "Double"); define_geometry(m, "Exact"); @@ -81,6 +87,6 @@ PYBIND11_MODULE(_storage, m) { define_maximal_end_component_decomposition(m, "_double"); define_maximal_end_component_decomposition(m, "_exact"); define_maximal_end_component_decomposition(m, "_interval"); + define_maximal_end_component_decomposition(m, "_ratinterval"); define_maximal_end_component_decomposition(m, "_ratfunc"); - } diff --git a/src/mod_utility.cpp b/src/mod_utility.cpp index dd53606bed..d2510cb400 100644 --- a/src/mod_utility.cpp +++ b/src/mod_utility.cpp @@ -1,22 +1,24 @@ #include "common.h" -#include "utility/shortestPaths.h" -#include "utility/smtsolver.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "utility/chrono.h" #include "utility/json.h" -#include "storm/adapters/RationalNumberAdapter.h" +#include "utility/kwekMehlhorn.h" +#include "utility/shortestPaths.h" +#include "utility/smtsolver.h" PYBIND11_MODULE(_utility, m) { - m.doc() = "Utilities for Storm"; + m.doc() = "Utilities for Storm"; #ifdef STORMPY_DISABLE_SIGNATURE_DOC - py::options options; - options.disable_function_signatures(); + py::options options; + options.disable_function_signatures(); #endif - define_ksp(m); - define_smt(m); - define_chrono(m); - define_json(m, "Double"); - define_json(m, "Rational"); + define_ksp(m); + define_smt(m); + define_chrono(m); + define_json(m, "Double"); + define_json(m, "Rational"); + define_kwek_mehlhorn(m, ""); } diff --git a/src/storage/decomposition.cpp b/src/storage/decomposition.cpp index 08db02b9fb..c1a060ea12 100644 --- a/src/storage/decomposition.cpp +++ b/src/storage/decomposition.cpp @@ -38,4 +38,5 @@ void define_maximal_end_component_decomposition(py::module& m, std::string const template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); +template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp index f970e73d75..122e9ba42c 100644 --- a/src/storage/distribution.cpp +++ b/src/storage/distribution.cpp @@ -19,3 +19,4 @@ void define_distribution(py::module& m, std::string vt_suffix) { template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); +template void define_distribution(py::module&, std::string vt_suffix); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 15c01ecc41..b52356650a 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -134,5 +134,6 @@ void define_sparse_matrix(py::module& m, std::string const& vtSuffix) { template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); +template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 16f17ee1a1..03b5ae5e5c 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -116,6 +116,12 @@ void define_model(py::module& m) { .def("_as_sparse_pdtmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric DTMC") + .def("_as_sparse_idtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse interval DTMC") + .def("_as_sparse_exact_idtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact interval DTMC") .def("_as_sparse_mdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse MDP") @@ -125,18 +131,24 @@ void define_model(py::module& m) { .def("_as_sparse_imdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse interval MDP") + .def("_as_sparse_exact_imdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact interval MDP") .def("_as_sparse_pmdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric MDP") .def("_as_sparse_pomdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse POMDP") + .def("_as_sparse_ipomdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse interval POMDP") + .def("_as_sparse_exact_ipomdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse interval exact POMDP") .def("_as_sparse_exact_pomdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse exact POMDP") - .def("_as_sparse_ipomdp", [](ModelBase &modelbase) { - return modelbase.as>(); - }, "Get model as sparse interval POMDP") .def("_as_sparse_ppomdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric POMDP") @@ -393,6 +405,7 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { template void define_sparse_model(py::module& m, std::string const& vt_suffix); template void define_sparse_model(py::module& m, std::string const& vt_suffix); template void define_sparse_model(py::module& m, std::string const& vt_suffix); +template void define_sparse_model(py::module& m, std::string const& vt_suffix); template void define_sparse_model(py::module& m, std::string const& vt_suffix); template void define_symbolic_model(py::module& m, std::string vt_suffix); diff --git a/src/storage/model_components.cpp b/src/storage/model_components.cpp index 9f46bbe874..57252740f8 100644 --- a/src/storage/model_components.cpp +++ b/src/storage/model_components.cpp @@ -40,6 +40,7 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix) // POMDP specific components .def_readwrite("observability_classes", &SparseModelComponents::observabilityClasses, "The POMDP observations") + .def_readwrite("observation_valuations", &SparseModelComponents::observationValuations, "The POMDP observation valuations") // Continuous time specific components (CTMCs, Markov Automata): .def_readwrite("rate_transitions", &SparseModelComponents::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates") @@ -59,4 +60,5 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix) template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); +template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/state.cpp b/src/storage/state.cpp index e73323cfb1..8125541e48 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -40,5 +40,6 @@ void define_state(py::module& m, std::string const& vtSuffix) { template void define_state(py::module& m, std::string const& vtSuffix); template void define_state(py::module& m, std::string const& vtSuffix); template void define_state(py::module& m, std::string const& vtSuffix); +template void define_state(py::module& m, std::string const& vtSuffix); template void define_state(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp index a73aeabe85..5a71aab0cc 100644 --- a/src/storage/valuation.cpp +++ b/src/storage/valuation.cpp @@ -32,7 +32,7 @@ void define_statevaluation(py::module& m) { .def("get_string", &storm::storage::sparse::StateValuations::toString, py::arg("state"), py::arg("pretty")=true, py::arg("selected_variables")=boost::none) .def("get_json", &toJson, py::arg("state"), py::arg("selected_variables")=boost::none) .def("get_nr_of_states", &storm::storage::sparse::StateValuations::getNumberOfStates) - .def_property_readonly("manager", &storm::storage::sparse::StateValuations::getManager); + .def_property_readonly("manager", &storm::storage::sparse::StateValuations::getManager) ; diff --git a/src/utility/kwekMehlhorn.cpp b/src/utility/kwekMehlhorn.cpp new file mode 100644 index 0000000000..50bcb5438a --- /dev/null +++ b/src/utility/kwekMehlhorn.cpp @@ -0,0 +1,22 @@ +#include "kwekMehlhorn.h" +#include "src/common.h" +#include +#include +#include + +template +void define_kwek_mehlhorn(py::module &m, std::string const &vtSuffix) { + m.def( + "sharpen", + [](uint64_t precision, double value) { + return storm::utility::kwek_mehlhorn::sharpen(precision, value); + }, + "Convert a float to the nearest rational within precision using Kwek " + "Mehlhorn", + py::arg("precision"), py::arg("value")); +} + +template void +define_kwek_mehlhorn(py::module &m, + std::string const &vtSuffix); \ No newline at end of file diff --git a/src/utility/kwekMehlhorn.h b/src/utility/kwekMehlhorn.h new file mode 100644 index 0000000000..42292ca4f7 --- /dev/null +++ b/src/utility/kwekMehlhorn.h @@ -0,0 +1,6 @@ +#pragma once + +#include "src/common.h" + +template +void define_kwek_mehlhorn(py::module &m, std::string const &vtSuffix); \ No newline at end of file From a91489a7e9848fb215d9e9f7b1a44a7acc364627 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Tue, 21 Apr 2026 13:41:36 +0200 Subject: [PATCH 02/14] Add conditional model checking, POMDP generator, environment bindings Exposes conditional/multi-objective model checker environment settings, scheduler class restrictions, qualitative result schedulers, AddUncertainty transformer, POMDP observation trace unfolder options, verimon generator, and removes the dense belief tracker. --- .gitignore | 5 +- CMakeLists.txt | 2 +- lib/stormpy/__init__.py | 2 +- lib/stormpy/pomdp/__init__.py | 12 +++- src/core/environment.cpp | 102 +++++++++++++++++++++++++++++++++- src/core/result.cpp | 11 ++-- src/core/transformation.cpp | 11 ++++ src/core/transformation.h | 2 + src/logic/formulae.cpp | 8 ++- src/mod_core.cpp | 15 ++--- src/mod_pomdp.cpp | 24 ++++++-- src/pomdp/generator.cpp | 48 ++++++++++++++++ src/pomdp/generator.h | 5 ++ src/pomdp/tracker.cpp | 12 ---- src/pomdp/transformations.cpp | 79 +++++++++++++++++--------- src/pomdp/transformations.h | 8 ++- src/storage/scheduler.cpp | 11 +++- 17 files changed, 287 insertions(+), 70 deletions(-) create mode 100644 src/pomdp/generator.cpp create mode 100644 src/pomdp/generator.h diff --git a/.gitignore b/.gitignore index 28f42c3176..356a7aa716 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,9 @@ dist/ __pycache__/ _build/ .pytest_cache/ +.idea/ +.vscode/ cmake-build-debug/ - +.cache/ .DS_Store +.venv/ diff --git a/CMakeLists.txt b/CMakeLists.txt index d2606bc448..d12008f65f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -411,4 +411,4 @@ if (PYCARL_HAS_PARSE) endif() else() MESSAGE(WARNING "Stormpy - No support for carl-parser") -endif() +endif() \ No newline at end of file diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index d132abebf8..a1059487e4 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -394,7 +394,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment, - ) + ) else: assert model.is_symbolic_model if extract_scheduler: diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index c43ceb50ec..a518cf7a26 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -16,6 +16,8 @@ def make_canonic(model): if model.supports_parameters: return _pomdp._make_canonic_Rf(model) + elif model.is_exact: + return _pomdp._make_canonic_Exact(model) else: return _pomdp._make_canonic_Double(model) @@ -73,15 +75,19 @@ def create_nondeterminstic_belief_tracker(model, reduction_timeout, track_timeou return _pomdp.NondeterministicBeliefTrackerDoubleSparse(model, opts) -def create_observation_trace_unfolder(model, risk_assessment, expr_manager): +def create_observation_trace_unfolder(model, risk_assessment, expr_manager, options=None): """ :param model: :param risk_assessment: :param expr_manager: + :param options: :return: """ + if options is None: + options = ObservationTraceUnfolderOptions() + if model.is_exact: - return _pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager) + return _pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager, options) else: - return _pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager) + return _pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager, options) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index e89007057c..d0abcc3f68 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -3,6 +3,9 @@ #include "storm/environment/Environment.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/AllSolverEnvironments.h" +#include "storm/environment/modelchecker/ModelCheckerEnvironment.h" +#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" +#include "storm/storage/SchedulerClass.h" // added for SchedulerClass binding void define_environment(py::module& m) { py::enum_(m, "EquationSolverType", "Solver type for equation systems") @@ -36,9 +39,107 @@ void define_environment(py::module& m) { .value("optimistic_value_iteration", storm::solver::MinMaxMethod::OptimisticValueIteration) ; + // Multi-objective related enums + py::enum_(m, "MultiObjectiveMethod", "Multi-objective model checking method") + .value("pcaa", storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa) + .value("constraint_based", storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased) + ; + + // Added enums for model checker environment + py::enum_(m, "SteadyStateDistributionAlgorithm", "Algorithm for steady state distribution computation") + .value("automatic", storm::SteadyStateDistributionAlgorithm::Automatic) + .value("equation_system", storm::SteadyStateDistributionAlgorithm::EquationSystem) + .value("expected_visiting_times", storm::SteadyStateDistributionAlgorithm::ExpectedVisitingTimes) + .value("classic", storm::SteadyStateDistributionAlgorithm::Classic) + ; + + py::enum_(m, "ConditionalAlgorithmSetting", "Algorithm used for conditional model checking") + .value("default", storm::ConditionalAlgorithmSetting::Default) + .value("restart", storm::ConditionalAlgorithmSetting::Restart) + .value("bisection", storm::ConditionalAlgorithmSetting::Bisection) + .value("bisection_advanced", storm::ConditionalAlgorithmSetting::BisectionAdvanced) + .value("bisection_pt", storm::ConditionalAlgorithmSetting::BisectionPolicyTracking) + .value("bisection_advanced_pt", storm::ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking) + .value("policy_iteration", storm::ConditionalAlgorithmSetting::PolicyIteration) + ; + + py::enum_(m, "MultiObjectivePrecisionType", "Type of precision for multi-objective model checking") + .value("absolute", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute) + .value("relative_to_diff", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::RelativeToDiff) + ; + + py::enum_(m, "MultiObjectiveEncodingType", "Encoding type for multi-objective model checking") + .value("auto", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto) + .value("classic", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic) + .value("flow", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow) + ; + + // Scheduler class bindings (needed for scheduler restriction) + py::enum_(m, "SchedulerMemoryPattern", "Memory pattern of a scheduler") + .value("arbitrary", storm::storage::SchedulerClass::MemoryPattern::Arbitrary) + .value("goal_memory", storm::storage::SchedulerClass::MemoryPattern::GoalMemory) + .value("counter", storm::storage::SchedulerClass::MemoryPattern::Counter) + ; + + py::class_(m, "SchedulerClass", "Scheduler class restriction") + .def(py::init<>()) + .def_property("deterministic", &storm::storage::SchedulerClass::isDeterministic, [](storm::storage::SchedulerClass& sc, bool v){ sc.setIsDeterministic(v); }) + .def_property("memory_states", + [](storm::storage::SchedulerClass const& sc)->py::object { if (sc.isMemoryBounded()) return py::cast(sc.getMemoryStates()); return py::none(); }, + [](storm::storage::SchedulerClass& sc, py::object obj){ if (obj.is_none()) sc.unsetMemoryStates(); else sc.setMemoryStates(obj.cast()); }) + .def_property_readonly("is_memory_bounded", &storm::storage::SchedulerClass::isMemoryBounded) + .def_property_readonly("memory_pattern", &storm::storage::SchedulerClass::getMemoryPattern) + .def("set_memory_pattern", [](storm::storage::SchedulerClass& sc, storm::storage::SchedulerClass::MemoryPattern p){ sc.setMemoryPattern(p); }) + .def("set_positional", &storm::storage::SchedulerClass::setPositional) + ; + py::class_(m, "Environment", "Environment") .def(py::init<>(), "Construct default environment") .def_property_readonly("solver_environment", [](storm::Environment& env) -> auto& {return env.solver();}, "solver part of environment") + .def_property_readonly("model_checker_environment", [](storm::Environment& env) -> auto& {return env.modelchecker();}, "model checker part of environment") + ; + + py::class_(m, "ModelCheckerEnvironment", "Environment for the solver") + .def_property("conditional_algorithm", &storm::ModelCheckerEnvironment::getConditionalAlgorithmSetting, &storm::ModelCheckerEnvironment::setConditionalAlgorithmSetting, "conditional algorithm used") + .def_property("conditional_tolerance", &storm::ModelCheckerEnvironment::getConditionalTolerance, &storm::ModelCheckerEnvironment::setConditionalTolerance, "conditional tolerance used") + .def_property("steady_state_distribution_algorithm", &storm::ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm, &storm::ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm, "steady state distribution algorithm used") + .def_property("optimization_for_bounded_properties", &storm::ModelCheckerEnvironment::isAllowOptimizationForBoundedPropertiesSet, &storm::ModelCheckerEnvironment::setAllowOptimizationForBoundedProperties, "enable optimization for bounded properties") + .def_property("ltl2da_tool", + [](storm::ModelCheckerEnvironment const& env)->py::object { if (env.isLtl2daToolSet()) return py::cast(env.getLtl2daTool()); return py::none(); }, + [](storm::ModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetLtl2daTool(); else env.setLtl2daTool(obj.cast()); }, + "Path to external ltl2da tool (None to unset)") + .def_property_readonly("multi", [](storm::ModelCheckerEnvironment& env)->storm::MultiObjectiveModelCheckerEnvironment& { return env.multi(); }, py::return_value_policy::reference, "Access multi-objective sub-environment") + ; + + py::class_(m, "MultiObjectiveModelCheckerEnvironment", "Environment for multi-objective model checking") + .def_property("method", + [](storm::MultiObjectiveModelCheckerEnvironment const& env){ return env.getMethod(); }, + &storm::MultiObjectiveModelCheckerEnvironment::setMethod, + "multi-objective model checking method") + .def_property("precision", &storm::MultiObjectiveModelCheckerEnvironment::getPrecision, &storm::MultiObjectiveModelCheckerEnvironment::setPrecision) + .def_property("precision_type", &storm::MultiObjectiveModelCheckerEnvironment::getPrecisionType, &storm::MultiObjectiveModelCheckerEnvironment::setPrecisionType) + .def_property("encoding_type", &storm::MultiObjectiveModelCheckerEnvironment::getEncodingType, &storm::MultiObjectiveModelCheckerEnvironment::setEncodingType) + .def_property("use_indicator_constraints", &storm::MultiObjectiveModelCheckerEnvironment::getUseIndicatorConstraints, &storm::MultiObjectiveModelCheckerEnvironment::setUseIndicatorConstraints) + .def_property("use_bscc_order_encoding", &storm::MultiObjectiveModelCheckerEnvironment::getUseBsccOrderEncoding, &storm::MultiObjectiveModelCheckerEnvironment::setUseBsccOrderEncoding) + .def_property("use_redundant_bscc_constraints", &storm::MultiObjectiveModelCheckerEnvironment::getUseRedundantBsccConstraints, &storm::MultiObjectiveModelCheckerEnvironment::setUseRedundantBsccConstraints) + .def_property_readonly("export_plot_set", &storm::MultiObjectiveModelCheckerEnvironment::isExportPlotSet) + .def_property("plot_path_under_approximation", + [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathUnderApproximation(); if (p) return py::cast(*p); return py::none(); }, + [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathUnderApproximation(); else env.setPlotPathUnderApproximation(obj.cast()); }) + .def_property("plot_path_over_approximation", + [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathOverApproximation(); if (p) return py::cast(*p); return py::none(); }, + [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathOverApproximation(); else env.setPlotPathOverApproximation(obj.cast()); }) + .def_property("plot_path_pareto_points", + [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathParetoPoints(); if (p) return py::cast(*p); return py::none(); }, + [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathParetoPoints(); else env.setPlotPathParetoPoints(obj.cast()); }) + .def_property("max_steps", + [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { if (env.isMaxStepsSet()) return py::cast(env.getMaxSteps()); return py::none(); }, + [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetMaxSteps(); else env.setMaxSteps(obj.cast()); }) + .def_property("scheduler_restriction", + [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { if (env.isSchedulerRestrictionSet()) return py::cast(env.getSchedulerRestriction()); return py::none(); }, + [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetSchedulerRestriction(); else env.setSchedulerRestriction(obj.cast()); }) + .def_property("print_results", &storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet, &storm::MultiObjectiveModelCheckerEnvironment::setPrintResults) + .def_property("lexicographic_model_checking", &storm::MultiObjectiveModelCheckerEnvironment::isLexicographicModelCheckingSet, &storm::MultiObjectiveModelCheckerEnvironment::setLexicographicModelChecking) ; py::class_(m, "SolverEnvironment", "Environment for solvers") @@ -62,4 +163,3 @@ void define_environment(py::module& m) { } - diff --git a/src/core/result.cpp b/src/core/result.cpp index c4618e9250..4f111786fd 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -28,7 +28,7 @@ std::shared_ptr createFilterSymboli void define_result(py::module& m) { // CheckResult - py::class_>(m, "_CheckResult", "Base class for all modelchecking results") + auto checkResult = py::class_>(m, "_CheckResult", "Base class for all modelchecking results") .def_property_readonly("_symbolic", &storm::modelchecker::CheckResult::isSymbolic, "Flag if result is symbolic") .def_property_readonly("_hybrid", &storm::modelchecker::CheckResult::isHybrid, "Flag if result is hybrid") .def_property_readonly("_quantitative", &storm::modelchecker::CheckResult::isQuantitative, "Flag if result is quantitative") @@ -69,10 +69,10 @@ void define_result(py::module& m) { ; // QualitativeCheckResult - py::class_, storm::modelchecker::CheckResult>(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results"); + py::class_> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult); - py::class_, std::shared_ptr>, storm::modelchecker::QualitativeCheckResult>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result") - .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult::getTruthValuesVector, "Get Dd representing the truth values") + py::class_, std::shared_ptr>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult) + .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult::getTruthValuesVector, "Get Dd representing the truth values") ; } @@ -84,6 +84,7 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { return result[state]; }, py::arg("state"), "Get result for given state") .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") + .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQualitativeCheckResult const& res) {return res.getScheduler();}, "get scheduler") ; py::class_, std::shared_ptr>, storm::modelchecker::CheckResult> quantitativeCheckResult(m, ("_" + vtSuffix + "QuantitativeCheckResult").c_str(), "Abstract class for quantitative model checking results"); @@ -126,4 +127,4 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) { template void define_typed_result(py::module& m, std::string const& vtSuffix); template void define_typed_result(py::module& m, std::string const& vtSuffix); -template void define_typed_result(py::module& m, std::string const& vtSuffix); \ No newline at end of file +template void define_typed_result(py::module& m, std::string const& vtSuffix); diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index c7d99ac6ed..cf43d7a627 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -5,6 +5,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/transformer/SubsystemBuilder.h" #include "storm/transformer/EndComponentEliminator.h" +#include "storm/transformer/AddUncertainty.h" // Thin wrappers. template @@ -84,6 +85,16 @@ void define_transformation_typed(py::module& m, std::string const& vtSuffix) { m.def(("_construct_subsystem_" + vtSuffix).c_str(), &constructSubsystem, "build a subsystem of a sparse model"); } +template +void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix) { + py::class_>(m, ("AddUncertainty" + vtSuffix).c_str(), "Transform model into interval model with specified uncertainty") + .def(py::init> const&>(), py::arg("model")) + .def("transform", &storm::transformer::AddUncertainty::transform, "transform the model", py::arg("additiveUncertainty"), py::arg("minimalValue") = storm::utility::convertNumber(0.0001), py::arg("maxSuccessors") = std::optional{}); +} + template void define_transformation_typed(py::module& m, std::string const& vtSuffix); template void define_transformation_typed(py::module& m, std::string const& vtSuffix); template void define_transformation_typed(py::module& m, std::string const& vtSuffix); + +template void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); +template void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); diff --git a/src/core/transformation.h b/src/core/transformation.h index 7bd010bb8d..b9691d82cc 100644 --- a/src/core/transformation.h +++ b/src/core/transformation.h @@ -5,3 +5,5 @@ void define_transformation(py::module& m); template void define_transformation_typed(py::module& m, std::string const& suffix); +template +void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix); diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 46ccaed610..c5364bddc2 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -32,13 +32,15 @@ void define_formulae(py::module& m) { .def_property_readonly("is_bounded_until_formula", &storm::logic::Formula::isBoundedUntilFormula) .def_property_readonly("is_until_formula", &storm::logic::Formula::isUntilFormula) .def_property_readonly("is_multi_objective_formula", &storm::logic::Formula::isMultiObjectiveFormula) + .def("_as_eventually_formula", [](storm::logic::Formula const& f) { return f.asEventuallyFormula(); }, "Get as eventually formula") ; // Path Formulae py::class_> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula); py::class_> unaryPathFormula(m, "UnaryPathFormula", "Path formula with one operand", pathFormula); unaryPathFormula.def_property_readonly("subformula", &storm::logic::UnaryPathFormula::getSubformula, "the subformula"); - py::class_>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula); + py::class_>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula) + .def_property_readonly("subformula", &storm::logic::EventuallyFormula::getSubformula, "the subformula"); py::class_>(m, "GloballyFormula", "Formula for globally", unaryPathFormula); py::class_> binaryPathFormula(m, "BinaryPathFormula", "Path formula with two operands", pathFormula); binaryPathFormula.def_property_readonly("left_subformula", &storm::logic::BinaryPathFormula::getLeftSubformula); @@ -49,7 +51,9 @@ void define_formulae(py::module& m) { .def_property_readonly("upper_bound_expression", [](storm::logic::BoundedUntilFormula const& form) { return form.getUpperBound(); } ) .def_property_readonly("left_subformula", [](storm::logic::BoundedUntilFormula const& form) -> storm::logic::Formula const& { return form.getLeftSubformula(); }, py::return_value_policy::reference_internal) .def_property_readonly("right_subformula", [](storm::logic::BoundedUntilFormula const& form)-> storm::logic::Formula const& { return form.getRightSubformula(); }, py::return_value_policy::reference_internal); - py::class_>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula); + py::class_>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula) + .def_property_readonly("main_subformula", &storm::logic::ConditionalFormula::getSubformula, "the subformula") + .def_property_readonly("conditional_subformula", &storm::logic::ConditionalFormula::getConditionFormula, "the conditional subformula"); py::class_>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula); // Reward Path Formulae diff --git a/src/mod_core.cpp b/src/mod_core.cpp index a246a5bf32..76a7fee234 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -1,15 +1,15 @@ #include "common.h" -#include "core/core.h" -#include "core/result.h" -#include "core/modelchecking.h" -#include "core/bisimulation.h" -#include "core/input.h" #include "core/analysis.h" +#include "core/bisimulation.h" +#include "core/core.h" #include "core/counterexample.h" #include "core/environment.h" -#include "core/transformation.h" +#include "core/input.h" +#include "core/modelchecking.h" +#include "core/result.h" #include "core/simulator.h" +#include "core/transformation.h" PYBIND11_MODULE(_core, m) { m.doc() = "core"; @@ -43,8 +43,9 @@ PYBIND11_MODULE(_core, m) { define_transformation_typed(m, "Double"); define_transformation_typed(m, "Exact"); define_transformation_typed(m, "RatFunc"); + define_transformation_typed_only_numbers(m, "Double"); + define_transformation_typed_only_numbers(m, "Exact"); define_sparse_model_simulator(m, "Double"); define_sparse_model_simulator(m, "Exact"); define_prism_program_simulator(m, "Double"); - } diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp index a26a9e50f0..6cdd333046 100644 --- a/src/mod_pomdp.cpp +++ b/src/mod_pomdp.cpp @@ -1,12 +1,15 @@ #include "common.h" -#include "pomdp/tracker.h" -#include "pomdp/qualitative_analysis.h" -#include "pomdp/transformations.h" +#include +#include +#include +#include "pomdp/generator.h" #include "pomdp/memory.h" +#include "pomdp/qualitative_analysis.h" #include "pomdp/quantitative_analysis.h" -#include +#include "pomdp/tracker.h" +#include "pomdp/transformations.h" PYBIND11_MODULE(_pomdp, m) { m.doc() = "Functionality for POMDP analysis"; @@ -21,9 +24,18 @@ PYBIND11_MODULE(_pomdp, m) { define_qualitative_policy_search_nt(m); define_memory(m); define_transformations_nt(m); + define_transformations(m, "Double"); define_transformations(m, "Exact"); - define_belief_exploration(m, "Double"); - define_transformations(m, "Rf"); + + define_transformations_int(m, "Double"); + define_transformations_int(m, "Exact"); + define_transformations_int(m, "Rf"); + define_transformations_int(m, "Interval"); + define_transformations_int(m, "RationalInterval"); + + define_belief_exploration(m, "Double"); + define_verimon_generator(m, "Double"); + define_verimon_generator(m, "Exact"); } diff --git a/src/pomdp/generator.cpp b/src/pomdp/generator.cpp new file mode 100644 index 0000000000..8093d9d443 --- /dev/null +++ b/src/pomdp/generator.cpp @@ -0,0 +1,48 @@ +#include "generator.h" +#include +#include +#include "storm-pomdp/generator/GenerateMonitorVerifier.h" +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/storage/expressions/ExpressionManager.h" + +template +using GenerateMonitorVerifier = storm::generator::GenerateMonitorVerifier; +template +using SparseDtmc = storm::models::sparse::Dtmc; +template +using SparseMdp = storm::models::sparse::Mdp; +template +using SparsePomdp = storm::models::sparse::Pomdp; +template +using GenerateMonitorVerifierOptions = typename storm::generator::GenerateMonitorVerifier::Options; + +template +void define_verimon_generator(py::module &m, std::string const &vtSuffix) { + py::class_, std::shared_ptr>> mv( + m, ("MonitorVerifier" + vtSuffix).c_str(), "Container for monitor verifier POMDP with associated objects"); + mv.def(py::init &, const std::map, uint32_t> &, const std::map &>(), + py::arg("product"), py::arg("observation_map"), py::arg("default_action_map")); + mv.def("get_product", &storm::generator::MonitorVerifier::getProduct, py::return_value_policy::copy); + mv.def_property_readonly("observation_map", &storm::generator::MonitorVerifier::getObservationMap, py::return_value_policy::copy); + mv.def_property_readonly("default_action_map", &storm::generator::MonitorVerifier::getObservationDefaultAction, py::return_value_policy::copy); + + py::class_> gmv(m, ("GenerateMonitorVerifier" + vtSuffix).c_str(), + "Generator of POMDP used in verifying monitors against markov chains"); + gmv.def(py::init const &, SparseMdp const &, std::shared_ptr &, + GenerateMonitorVerifierOptions const &>(), + py::arg("mc"), py::arg("monitor"), py::arg("expr_manager"), py::arg("options")); + gmv.def("create_product", &storm::generator::GenerateMonitorVerifier::createProduct, py::return_value_policy::copy, + "Created the verification POMDP"); + gmv.def("set_risk", &storm::generator::GenerateMonitorVerifier::setRisk, py::arg("risk")); + + py::class_> gmvopts(m, ("GenerateMonitorVerifier" + vtSuffix + "Options").c_str(), + "Options for corresponding generator"); + gmvopts.def(py::init<>()); + gmvopts.def_readwrite("accepting_label", &GenerateMonitorVerifierOptions::acceptingLabel); + gmvopts.def_readwrite("step_prefix", &GenerateMonitorVerifierOptions::stepPrefix); + gmvopts.def_readwrite("horizon_label", &GenerateMonitorVerifierOptions::horizonLabel); + gmvopts.def_readwrite("use_restart_semantics", &GenerateMonitorVerifierOptions::useRestartSemantics); +} + +template void define_verimon_generator(py::module &m, std::string const &vtSuffix); +template void define_verimon_generator(py::module &m, std::string const &vtSuffix); diff --git a/src/pomdp/generator.h b/src/pomdp/generator.h new file mode 100644 index 0000000000..bd28415441 --- /dev/null +++ b/src/pomdp/generator.h @@ -0,0 +1,5 @@ +#pragma once +#include "common.h" + +template +void define_verimon_generator(py::module& m, std::string const& vtSuffix); diff --git a/src/pomdp/tracker.cpp b/src/pomdp/tracker.cpp index 11740e2b98..8c7a20a55c 100644 --- a/src/pomdp/tracker.cpp +++ b/src/pomdp/tracker.cpp @@ -10,7 +10,6 @@ template using SparsePomdp = storm::models::sparse::Pomdp using SparsePomdpTracker = storm::generator::BeliefSupportTracker; template using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker>; -template using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker>; template @@ -49,17 +48,6 @@ void define_tracker(py::module& m, std::string const& vtSuffix) { ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse::getCurrentObservation); ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse::reduce); ndetbelieftracker.def("reduction_timed_out", &NDPomdpTrackerSparse::hasTimedOut); - -// py::class_> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions"); -// ndetbelieftrackerd.def(py::init const&>(), py::arg("pomdp")); -// ndetbelieftrackerd.def("reset", &NDPomdpTrackerDense::reset); -// ndetbelieftrackerd.def("set_risk", &NDPomdpTrackerDense::setRisk, py::arg("risk")); -// ndetbelieftrackerd.def("obtain_current_risk",&NDPomdpTrackerDense::getCurrentRisk, py::arg("max")=true); -// ndetbelieftrackerd.def("track", &NDPomdpTrackerDense::track, py::arg("observation")); -// ndetbelieftrackerd.def("obtain_beliefs", &NDPomdpTrackerDense::getCurrentBeliefs); -// ndetbelieftrackerd.def("obtain_last_observation", &NDPomdpTrackerDense::getCurrentObservation); -// ndetbelieftrackerd.def("reduce",&NDPomdpTrackerDense::reduce); - } template void define_tracker(py::module& m, std::string const& vtSuffix); diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index dea2cb7437..3b27c5569f 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -1,70 +1,95 @@ #include "transformations.h" -#include "storm-pomdp/transformer/PomdpMemoryUnfolder.h" -#include "storm-pomdp/transformer/BinaryPomdpTransformer.h" #include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h" +#include "storm-pomdp/transformer/BinaryPomdpTransformer.h" #include "storm-pomdp/transformer/ObservationTraceUnfolder.h" +#include "storm-pomdp/transformer/PomdpMemoryUnfolder.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/transformer/MakePOMDPCanonic.h" template -std::shared_ptr> make_canonic(storm::models::sparse::Pomdp const& pomdp) { +std::shared_ptr> make_canonic(storm::models::sparse::Pomdp const &pomdp) { storm::transformer::MakePOMDPCanonic makeCanonic(pomdp); return makeCanonic.transform(); } template -std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels, bool keepStateValuations) { +std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const &pomdp, + storm::storage::PomdpMemory const &memory, bool addMemoryLabels, + bool keepStateValuations) { storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory, addMemoryLabels, keepStateValuations); return unfolder.transform(); } template -std::shared_ptr> make_simple(storm::models::sparse::Pomdp const& pomdp, bool keepStateValuations) { +std::shared_ptr> make_simple(storm::models::sparse::Pomdp const &pomdp, bool keepStateValuations) { storm::transformer::BinaryPomdpTransformer transformer; - return transformer.transform(pomdp,true, keepStateValuations).transformedPomdp; + return transformer.transform(pomdp, true, keepStateValuations).transformedPomdp; } template -std::shared_ptr> apply_unknown_fsc(storm::models::sparse::Pomdp const& pomdp, storm::transformer::PomdpFscApplicationMode const& applicationMode) { +std::shared_ptr> apply_unknown_fsc(storm::models::sparse::Pomdp const &pomdp, + storm::transformer::PomdpFscApplicationMode const &applicationMode) { storm::transformer::ApplyFiniteSchedulerToPomdp transformer(pomdp); return transformer.transform(applicationMode); } template -std::shared_ptr> unfold_trace(storm::models::sparse::Pomdp const& pomdp, std::shared_ptr& exprManager, std::vector const& observationTrace, std::vector const& riskDef ) { - storm::pomdp::ObservationTraceUnfolder transformer(pomdp, exprManager); - return transformer.transform(observationTrace, riskDef); +std::shared_ptr> unfold_trace(storm::models::sparse::Pomdp const &pomdp, + std::shared_ptr &exprManager, + std::vector const &observationTrace, std::vector const &riskDef, + bool restartSemantics = true) { + storm::pomdp::ObservationTraceUnfolderOptions options = storm::pomdp::ObservationTraceUnfolderOptions(); + options.useRestartSemantics = restartSemantics; + storm::pomdp::ObservationTraceUnfolder transformer(pomdp, riskDef, exprManager, options); + return transformer.transform(observationTrace); } // STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL void define_transformations_nt(py::module &m) { py::enum_(m, "PomdpFscApplicationMode") - .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) - .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) - .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) - .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) - .value("full", storm::transformer::PomdpFscApplicationMode::FULL) - ; + .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) + .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) + .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) + .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) + .value("full", storm::transformer::PomdpFscApplicationMode::FULL); + py::class_ options(m, "ObservationTraceUnfolderOptions", "Options for unfolding observation traces"); + options.def(py::init<>()); + options.def_readwrite("restart_semantics", &storm::pomdp::ObservationTraceUnfolderOptions::useRestartSemantics, + "Use restart semantics instead of a sink state"); } template -void define_transformations(py::module& m, std::string const& vtSuffix) { +void define_transformations(py::module &m, std::string const &vtSuffix) { m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic, "Return a canonicly-ordered POMDP", py::arg("pomdp")); - m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false); - m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false); - m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); - //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition")); + m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), + py::arg("memorylabels") = false, py::arg("keep_state_valuations") = false); + m.def(("_make_simple_" + vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations") = false); + m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC", py::arg("pomdp"), + py::arg("application_mode") = storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); +} - py::class_> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models"); - unfolder.def(py::init const&, std::vector const&, std::shared_ptr&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager")); +template +void define_transformations_int(py::module &m, std::string const &vtSuffix) { + py::class_> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), + "Unfolds observation traces in models"); + unfolder.def(py::init, std::vector const &, std::shared_ptr &, + storm::pomdp::ObservationTraceUnfolderOptions const &>(), + py::arg("model"), py::arg("risk"), py::arg("expression_manager"), py::arg("options"), py::keep_alive<2, 1>()); + unfolder.def("is_restart_semantics_set", &storm::pomdp::ObservationTraceUnfolder::isRestartSemanticsSet); unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder::transform, py::arg("trace")); - unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder::reset, py::arg("new_observation")); + unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); } -template void define_transformations(py::module& m, std::string const& vtSuffix); -template void define_transformations(py::module& m, std::string const& vtSuffix); -template void define_transformations(py::module& m, std::string const& vtSuffix); +template void define_transformations(py::module &m, std::string const &vtSuffix); +template void define_transformations(py::module &m, std::string const &vtSuffix); +template void define_transformations(py::module &m, std::string const &vtSuffix); + +template void define_transformations_int(py::module &m, std::string const &vtSuffix); +template void define_transformations_int(py::module &m, std::string const &vtSuffix); +template void define_transformations_int(py::module &m, std::string const &vtSuffix); +template void define_transformations_int(py::module &m, std::string const &vtSuffix); +template void define_transformations_int(py::module &m, std::string const &vtSuffix); diff --git a/src/pomdp/transformations.h b/src/pomdp/transformations.h index 4410946f9c..fca131f8ae 100644 --- a/src/pomdp/transformations.h +++ b/src/pomdp/transformations.h @@ -2,6 +2,8 @@ #include "common.h" -void define_transformations_nt(py::module& m); -template -void define_transformations(py::module& m, std::string const& vtSuffix); +void define_transformations_nt(py::module &m); +template +void define_transformations(py::module &m, std::string const &vtSuffix); +template +void define_transformations_int(py::module &m, std::string const &vtSuffix); diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index 263ec7bd55..7020afc505 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -31,9 +31,16 @@ void define_scheduler(py::module& m, std::string vt_suffix) { s.printJsonToStream(str, model, skipUniqueChoices, skipDontCareStates); return str.str(); }, py::arg("model"), py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false) + .def("to_str", [](Scheduler const& s, std::shared_ptr> model, bool skipUniqueChoices, + bool skipDontCareStates) { + std::stringstream str; + s.printToStream(str, model, skipUniqueChoices, skipDontCareStates); + return str.str(); + }, py::arg("model") = nullptr, py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false) + .def("get_memoryless_scheduler_for_memory_state", &Scheduler::getMemorylessSchedulerForMemoryState, py::arg("memory_state") = 0, "Get the memoryless scheduler corresponding to the given memory state") ; - if constexpr (!std::is_same_v) { + if constexpr (!std::is_same_v && !std::is_same_v) { // Conversion from Interval not implemented scheduler .def("cast_to_double_datatype", &Scheduler::template toValueType, "Construct the scheduler with `double` value type") @@ -43,6 +50,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) { if constexpr (!std::is_same_v) { // Conversion from RationalFunction to Interval not implemented scheduler.def("cast_to_interval_datatype", &Scheduler::template toValueType, "Construct the scheduler with `interval` value type"); + scheduler.def("cast_to_exact_interval_datatype", &Scheduler::template toValueType, "Construct the scheduler with `interval` value type"); } } @@ -62,4 +70,5 @@ void define_scheduler(py::module& m, std::string vt_suffix) { template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); +template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); From f28ce03f5ef33ab4642acc1a198250b1d59b468c Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Tue, 21 Apr 2026 13:59:47 +0200 Subject: [PATCH 03/14] Adapt to the new storm conditional env --- src/core/environment.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index d0abcc3f68..552c12ae4e 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -3,9 +3,10 @@ #include "storm/environment/Environment.h" #include "storm/environment/solver/SolverEnvironment.h" #include "storm/environment/solver/AllSolverEnvironments.h" +#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h" #include "storm/environment/modelchecker/ModelCheckerEnvironment.h" #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h" -#include "storm/storage/SchedulerClass.h" // added for SchedulerClass binding +#include "storm/storage/SchedulerClass.h" void define_environment(py::module& m) { py::enum_(m, "EquationSolverType", "Solver type for equation systems") @@ -99,15 +100,17 @@ void define_environment(py::module& m) { .def_property_readonly("model_checker_environment", [](storm::Environment& env) -> auto& {return env.modelchecker();}, "model checker part of environment") ; - py::class_(m, "ModelCheckerEnvironment", "Environment for the solver") - .def_property("conditional_algorithm", &storm::ModelCheckerEnvironment::getConditionalAlgorithmSetting, &storm::ModelCheckerEnvironment::setConditionalAlgorithmSetting, "conditional algorithm used") - .def_property("conditional_tolerance", &storm::ModelCheckerEnvironment::getConditionalTolerance, &storm::ModelCheckerEnvironment::setConditionalTolerance, "conditional tolerance used") + py::class_(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking") + .def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm, "algorithm for conditional model checking") + ; + + py::class_(m, "ModelCheckerEnvironment", "Environment for the model checker") .def_property("steady_state_distribution_algorithm", &storm::ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm, &storm::ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm, "steady state distribution algorithm used") - .def_property("optimization_for_bounded_properties", &storm::ModelCheckerEnvironment::isAllowOptimizationForBoundedPropertiesSet, &storm::ModelCheckerEnvironment::setAllowOptimizationForBoundedProperties, "enable optimization for bounded properties") .def_property("ltl2da_tool", [](storm::ModelCheckerEnvironment const& env)->py::object { if (env.isLtl2daToolSet()) return py::cast(env.getLtl2daTool()); return py::none(); }, [](storm::ModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetLtl2daTool(); else env.setLtl2daTool(obj.cast()); }, "Path to external ltl2da tool (None to unset)") + .def_property_readonly("conditional", [](storm::ModelCheckerEnvironment& env)->storm::ConditionalModelCheckerEnvironment& { return env.conditional(); }, py::return_value_policy::reference, "Access conditional model checking sub-environment") .def_property_readonly("multi", [](storm::ModelCheckerEnvironment& env)->storm::MultiObjectiveModelCheckerEnvironment& { return env.multi(); }, py::return_value_policy::reference, "Access multi-objective sub-environment") ; From a730319a559c2240b3fe955f95f43c1489706236 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Tue, 21 Apr 2026 14:46:11 +0200 Subject: [PATCH 04/14] Add tolerance to conditional env --- src/core/environment.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index 552c12ae4e..b772ae5a82 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -102,6 +102,7 @@ void define_environment(py::module& m) { py::class_(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking") .def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm, "algorithm for conditional model checking") + .def_property("tolerance", &storm::ConditionalModelCheckerEnvironment::getTolerance, &storm::ConditionalModelCheckerEnvironment::setTolerance, "tolerance for conditional model checking") ; py::class_(m, "ModelCheckerEnvironment", "Environment for the model checker") From 73be99070970e88da173c6fb0812ea070cf9735e Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Wed, 22 Apr 2026 14:32:44 +0200 Subject: [PATCH 05/14] Update to match storm env --- src/core/environment.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index b772ae5a82..6c4e348d90 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -1,4 +1,7 @@ #include "environment.h" +#include +#include +#include #include "src/helpers.h" #include "storm/environment/Environment.h" #include "storm/environment/solver/SolverEnvironment.h" @@ -102,7 +105,8 @@ void define_environment(py::module& m) { py::class_(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking") .def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm, "algorithm for conditional model checking") - .def_property("tolerance", &storm::ConditionalModelCheckerEnvironment::getTolerance, &storm::ConditionalModelCheckerEnvironment::setTolerance, "tolerance for conditional model checking") + .def_property("precision", &storm::ConditionalModelCheckerEnvironment::getPrecision, [](storm::ConditionalModelCheckerEnvironment& env, storm::RationalNumber value){ env.setPrecision(value, false); }, "precision for conditional model checking") + .def_property("relative", &storm::ConditionalModelCheckerEnvironment::isRelativePrecision, &storm::ConditionalModelCheckerEnvironment::setRelativePrecision, "whether the precision is relative") ; py::class_(m, "ModelCheckerEnvironment", "Environment for the model checker") From 53489834813e8498f589b80acedb2d548d7fa594 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 21 Apr 2026 18:04:50 +0200 Subject: [PATCH 06/14] Adaption to changes in POMDP (#387) --- src/pomdp/tracker.cpp | 5 ----- src/pomdp/transformations.cpp | 21 ++++++++++----------- 2 files changed, 10 insertions(+), 16 deletions(-) diff --git a/src/pomdp/tracker.cpp b/src/pomdp/tracker.cpp index 8c7a20a55c..3635773a0b 100644 --- a/src/pomdp/tracker.cpp +++ b/src/pomdp/tracker.cpp @@ -24,11 +24,6 @@ void define_tracker(py::module& m, std::string const& vtSuffix) { sbel.def_property_readonly("risk", &storm::generator::SparseBeliefState::getRisk); sbel.def("__str__", &storm::generator::SparseBeliefState::toString); sbel.def_property_readonly("is_valid", &storm::generator::SparseBeliefState::isValid); -// -// py::class_> dbel(m, "DenseBeliefStateDouble", "Belief state in dense format"); -// dbel.def("get", &storm::generator::ObservationDenseBeliefState::get, py::arg("state")); -// dbel.def_property_readonly("risk", &storm::generator::ObservationDenseBeliefState::getRisk); -// dbel.def("__str__", &storm::generator::ObservationDenseBeliefState::toString); py::class_::Options> opts(m, ("NondeterministicBeliefTracker" + vtSuffix + "SparseOptions").c_str(), "Options for the corresponding tracker"); opts.def(py::init<>()); diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 3b27c5569f..0979e1687a 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -49,12 +49,12 @@ std::shared_ptr> unfold_trace(storm::model // STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL void define_transformations_nt(py::module &m) { py::enum_(m, "PomdpFscApplicationMode") - .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) - .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) - .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) - .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) - .value("full", storm::transformer::PomdpFscApplicationMode::FULL); - + .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) + .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) + .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) + .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) + .value("full", storm::transformer::PomdpFscApplicationMode::FULL) + ; py::class_ options(m, "ObservationTraceUnfolderOptions", "Options for unfolding observation traces"); options.def(py::init<>()); options.def_readwrite("restart_semantics", &storm::pomdp::ObservationTraceUnfolderOptions::useRestartSemantics, @@ -64,11 +64,10 @@ void define_transformations_nt(py::module &m) { template void define_transformations(py::module &m, std::string const &vtSuffix) { m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic, "Return a canonicly-ordered POMDP", py::arg("pomdp")); - m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), - py::arg("memorylabels") = false, py::arg("keep_state_valuations") = false); - m.def(("_make_simple_" + vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations") = false); - m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC", py::arg("pomdp"), - py::arg("application_mode") = storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); + m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false); + m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false); + m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); + } template From 68ad81a916bc985654fb5739d05aa9f992de11e4 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Tue, 21 Apr 2026 14:57:55 +0200 Subject: [PATCH 07/14] format --- src/helpers.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/helpers.h b/src/helpers.h index 9aec2ad854..052737ca33 100644 --- a/src/helpers.h +++ b/src/helpers.h @@ -28,4 +28,3 @@ std::string containerToString(T& t) { // Be warned: Enabling something like this will break everything about Monomial, // as to Python the shared_ptr (Arg) IS the Monomial // //PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr); - From 9c74aa31a6892beae7f6d19b2e14d634b793e448 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 21 Apr 2026 18:04:50 +0200 Subject: [PATCH 08/14] Adaption to changes in POMDP (#387) --- src/pomdp/transformations.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 0979e1687a..01cff7858c 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -67,7 +67,6 @@ void define_transformations(py::module &m, std::string const &vtSuffix) { m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false); m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false); m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); - } template From 3b4ab01dda380638d2ce0f20e328e687cd43e661 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Thu, 23 Apr 2026 14:37:36 +0200 Subject: [PATCH 09/14] Use _convert_model in exact interval model building --- lib/stormpy/__init__.py | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index a1059487e4..866631c185 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -27,6 +27,7 @@ class _ValueType(Enum): EXACT = 2 PARAMETRIC = 3 INTERVAL = 4 + EXACT_INTERVAL = 5 def _convert_sparse_model(model, value_type=_ValueType.DOUBLE): @@ -103,6 +104,22 @@ def _convert_sparse_model(model, value_type=_ValueType.DOUBLE): return model._as_sparse_ismg() else: raise stormpy.exceptions.StormError("Not supported interval model constructed") + case _ValueType.EXACT_INTERVAL: + assert model.supports_uncertainty and model.is_exact + if model.model_type == ModelType.DTMC: + return model._as_sparse_exact_idtmc() + elif model.model_type == ModelType.MDP: + return model._as_sparse_exact_imdp() + elif model.model_type == ModelType.POMDP: + return model._as_sparse_exact_ipomdp() + elif model.model_type == ModelType.CTMC: + return model._as_sparse_exact_ictmc() + elif model.model_type == ModelType.MA: + return model._as_sparse_exact_ima() + elif model.model_type == ModelType.SMG: + return model._as_sparse_exact_ismg() + else: + raise stormpy.exceptions.StormError("Not supported exact interval model constructed") case _: raise stormpy.exceptions.StormError("Not supported model type constructed") @@ -321,15 +338,7 @@ def build_exact_interval_model_from_drn(file, options=DirectEncodingParserOption :return: Exact Interval model in sparse representation. """ intermediate = _core._build_sparse_exact_interval_model_from_drn(file, options) - assert intermediate.supports_uncertainty and intermediate.is_exact - if intermediate.model_type == ModelType.DTMC: - return intermediate._as_sparse_exact_idtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate._as_sparse_exact_imdp() - elif intermediate.model_type == ModelType.POMDP: - return intermediate._as_sparse_exact_ipomdp() - else: - raise StormError("Not supported exact interval model constructed") + return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL) def perform_bisimulation(model, properties, bisimulation_type, graph_preserving=True): From 7cbab1f029c0b6ea4c46a62e746e0c283b4200c4 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Thu, 23 Apr 2026 14:46:19 +0200 Subject: [PATCH 10/14] Added missing bulid exact interval model bindings --- lib/stormpy/__init__.py | 18 ++++++++++++++++++ src/core/core.cpp | 2 ++ src/storage/model.cpp | 9 +++++++++ 3 files changed, 29 insertions(+) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 866631c185..3cd47531df 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -254,6 +254,24 @@ def build_sparse_interval_model(symbolic_description, properties=None): intermediate = _core._build_sparse_interval_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL) +def build_sparse_exact_interval_model(symbolic_description, properties=None): + """ + Build an exact interval model in sparse representation from a symbolic description. + + :param symbolic_description: Symbolic model description to translate into a model. + :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved. + :return: Exact interval model in sparse representation. + """ + if not symbolic_description.undefined_constants_are_graph_preserving: + raise stormpy.exceptions.StormError("Program still contains undefined constants") + + if properties: + formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties] + intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description, formulae) + else: + intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description) + return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL) + def build_symbolic_model(symbolic_description, properties=None): """ diff --git a/src/core/core.cpp b/src/core/core.cpp index 173d9f559c..29335f90b1 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -124,10 +124,12 @@ void define_build(py::module& m) { m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_sparse_interval_model_from_symbolic_description", &buildSparseModel, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); + m.def("_build_sparse_exact_interval_model_from_symbolic_description", &buildSparseModel, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("build_sparse_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options")); m.def("build_sparse_exact_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("options")); m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options")); m.def("build_sparse_interval_model_with_options", &buildSparseModelWithOptions, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("options")); + m.def("build_sparse_exact_interval_model_with_options", &buildSparseModelWithOptions, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("options")); m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); 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>()); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 03b5ae5e5c..bf7eb852c7 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -161,6 +161,9 @@ void define_model(py::module& m) { .def("_as_sparse_ictmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse interval CTMC") + .def("_as_sparse_exact_ictmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact interval CTMC") .def("_as_sparse_pctmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric CTMC") @@ -173,6 +176,9 @@ void define_model(py::module& m) { .def("_as_sparse_ima", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse interval MA") + .def("_as_sparse_exact_ima", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact interval MA") .def("_as_sparse_pma", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric MA") @@ -185,6 +191,9 @@ void define_model(py::module& m) { .def("_as_sparse_ismg", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse interval SMG") + .def("_as_sparse_exact_ismg", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact interval SMG") .def("_as_sparse_psmg", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse parametric SMG") From e92fcd2173886067940df8f573fbae22fb4a8970 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Thu, 23 Apr 2026 15:22:23 +0200 Subject: [PATCH 11/14] Add test and fix bugs --- src/core/modelchecking.cpp | 6 ++++ src/storage/scheduler.cpp | 2 +- tests/core/test_modelchecking.py | 52 ++++++++++++++++++++++++++++++++ tests/storage/test_model.py | 21 +++++++++++++ 4 files changed, 80 insertions(+), 1 deletion(-) diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index 804b5c2283..a4b26e74d6 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -54,6 +54,11 @@ std::shared_ptr checkIntervalDtmc(std::shared_ return checker.check(env, task); } +std::shared_ptr checkRationalIntervalDtmc(std::shared_ptr> dtmc, CheckTask const& task, storm::Environment& env) { + auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker>(*dtmc); + return checker.check(env, task); +} + std::shared_ptr checkIntervalMdp(std::shared_ptr> mdp, CheckTask const& task, storm::Environment& env) { auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); return checker.check(env, task); @@ -151,6 +156,7 @@ void define_modelchecking(py::module& m) { 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()); 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()); m.def("check_interval_dtmc", &checkIntervalDtmc, "Check interval DTMC"); + m.def("check_exact_interval_dtmc", &checkRationalIntervalDtmc, "Check exact interval DTMC"); m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP"); m.def("check_exact_interval_mdp", &checkRationalIntervalMdp, "Check exact interval MDP"); m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities"); diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index 7020afc505..b2cade6195 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -40,7 +40,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) { .def("get_memoryless_scheduler_for_memory_state", &Scheduler::getMemorylessSchedulerForMemoryState, py::arg("memory_state") = 0, "Get the memoryless scheduler corresponding to the given memory state") ; - if constexpr (!std::is_same_v && !std::is_same_v) { + if constexpr (!storm::IsIntervalType) { // Conversion from Interval not implemented scheduler .def("cast_to_double_datatype", &Scheduler::template toValueType, "Construct the scheduler with `double` value type") diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 21b8a6e1ea..6975f1c94e 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -96,6 +96,58 @@ def test_model_checking_interval_mdp(self): result = stormpy.check_interval_mdp(model, task, env) assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) + def test_model_checking_exact_interval_dtmc(self): + program = stormpy.parse_prism_program(get_example_path("idtmc", "die-intervals.pm")) + formulas = stormpy.parse_properties('P=? [ F "one"]') + model = stormpy.build_sparse_exact_interval_model(program, formulas) + initial_state = model.initial_states[0] + assert initial_state == 0 + + env = stormpy.Environment() + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + + task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) + task.set_produce_schedulers() + # Compute maximal + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.MAXIMIZE) + result = stormpy.check_exact_interval_dtmc(model, task, env) + assert math.isclose(result.at(initial_state), 72.0 / 189.0, rel_tol=1e-4) + # Compute minimal + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.MINIMIZE) + result = stormpy.check_exact_interval_dtmc(model, task, env) + assert math.isclose(result.at(initial_state), 9.0 / 189.0, rel_tol=1e-4) + + def test_model_checking_exact_interval_mdp(self): + model = stormpy.build_exact_interval_model_from_drn(get_example_path("imdp", "tiny-01.drn")) + formulas = stormpy.parse_properties('Pmax=? [ F "target"];Pmin=? [ F "target"]') + initial_state = model.initial_states[0] + assert initial_state == 0 + + env = stormpy.Environment() + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + + task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True) + task.set_produce_schedulers() + # Compute maximal robust + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST) + result = stormpy.check_exact_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) + # Compute maximal cooperative + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.COOPERATIVE) + result = stormpy.check_exact_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4) + + task = stormpy.ExactCheckTask(formulas[1].raw_formula, only_initial_states=True) + task.set_produce_schedulers() + # Compute minimal robust + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST) + result = stormpy.check_exact_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4) + # Compute minimal cooperative + task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.COOPERATIVE) + result = stormpy.check_exact_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) + def test_model_checking_jani_dtmc(self): jani_model, formulas = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 939dabb2f8..f374ca7f2c 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -1,3 +1,5 @@ +from numbers import Rational + import stormpy from helpers.helper import get_example_path import pytest @@ -322,3 +324,22 @@ def test_build_ipomdp(self): assert model.model_type == stormpy.ModelType.POMDP assert type(model) is stormpy.SparseIntervalPomdp + + + def test_build_exact_ipomdp(self): + model = stormpy.build_exact_interval_model_from_drn(get_example_path("ipomdp", "tiny-01.drn")) + assert model.nr_states == 4 + assert model.nr_choices == 5 + assert model.nr_transitions == 8 + assert model.nr_observations == 3 + + for transition in model.transition_matrix.row_iter(0, 0): + if transition.column == 1: + assert transition.value().lower() == stormpy.Rational("1/5") + assert transition.value().upper() == stormpy.Rational("7/10") + elif transition.column == 2: + assert transition.value().lower() == stormpy.Rational("3/10") + assert transition.value().upper() == stormpy.Rational("4/5") + + assert model.model_type == stormpy.ModelType.POMDP + assert type(model) is stormpy.SparseRationalIntervalPomdp \ No newline at end of file From 0e3d804bf9f729305fa0e0972ea2f5852b150094 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Thu, 23 Apr 2026 15:24:48 +0200 Subject: [PATCH 12/14] Fix python format --- lib/stormpy/__init__.py | 1 + tests/storage/test_model.py | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 3cd47531df..1581fa86ab 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -254,6 +254,7 @@ def build_sparse_interval_model(symbolic_description, properties=None): intermediate = _core._build_sparse_interval_model_from_symbolic_description(symbolic_description) return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL) + def build_sparse_exact_interval_model(symbolic_description, properties=None): """ Build an exact interval model in sparse representation from a symbolic description. diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index f374ca7f2c..03b3c51452 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -342,4 +342,4 @@ def test_build_exact_ipomdp(self): assert transition.value().upper() == stormpy.Rational("4/5") assert model.model_type == stormpy.ModelType.POMDP - assert type(model) is stormpy.SparseRationalIntervalPomdp \ No newline at end of file + assert type(model) is stormpy.SparseRationalIntervalPomdp From 7a100cdd4d1e17a30196d68321351ae2cf26c18e Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Thu, 23 Apr 2026 15:27:44 +0200 Subject: [PATCH 13/14] another format fix --- tests/storage/test_model.py | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 03b3c51452..ae875d7664 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -325,7 +325,6 @@ def test_build_ipomdp(self): assert model.model_type == stormpy.ModelType.POMDP assert type(model) is stormpy.SparseIntervalPomdp - def test_build_exact_ipomdp(self): model = stormpy.build_exact_interval_model_from_drn(get_example_path("ipomdp", "tiny-01.drn")) assert model.nr_states == 4 From 9d2287c0b2598bfb4d8fc222afd33735e7ce92f9 Mon Sep 17 00:00:00 2001 From: Luko van der Maas Date: Fri, 24 Apr 2026 09:56:39 +0200 Subject: [PATCH 14/14] format --- lib/stormpy/__init__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 1581fa86ab..a535e85b12 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -422,7 +422,7 @@ def model_checking(model, property, only_initial_states=False, extract_scheduler extract_scheduler=extract_scheduler, force_fully_observable=force_fully_observable, environment=environment, - ) + ) else: assert model.is_symbolic_model if extract_scheduler: