Stormpy additions for storm PRs about explicit qualitative scheduler, exact intervals, monitoring and conditional algs.

.gitignore

@@ -9,6 +9,9 @@ dist/
 __pycache__/
 _build/
 .pytest_cache/
+.idea/
+.vscode/
 cmake-build-debug/
-
+.cache/
 .DS_Store
+.venv/

CMakeLists.txt

@@ -49,7 +49,7 @@
 # Python version should be synced with pyproject.toml
 find_package(Python 3.10 COMPONENTS Interpreter Development.Module REQUIRED)
 # Pybind11 version should be synced with pyproject.toml
 find_package(pybind11 3.0.3 EXACT CONFIG REQUIRED)
 message(STATUS "Stormpy - Using pybind11 version ${pybind11_VERSION}")
 
 # Helper function to print path where library was found and check whether hint was used
@@ -411,4 +411,4 @@
     endif()
 else()
     MESSAGE(WARNING "Stormpy - No support for carl-parser")
-endif()
+endif()

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.
@@ -374,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:
@@ -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:

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)

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:

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<storm::RationalNumber>, "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<storm::RationalFunction>, "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<storm::Interval>, "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<storm::RationalInterval>, "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<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") = "");
 
     m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "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<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_to_drn_interval", &exportDRN<storm::Interval>, "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<storm::RationalInterval>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_exact_to_drn", &exportDRN<storm::RationalNumber>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
 }

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_<storm::solver::EquationSolverType>(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_<storm::modelchecker::multiobjective::MultiObjectiveMethod>(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_<storm::SteadyStateDistributionAlgorithm>(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_<storm::ConditionalAlgorithmSetting>(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_<storm::MultiObjectiveModelCheckerEnvironment::PrecisionType>(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_<storm::MultiObjectiveModelCheckerEnvironment::EncodingType>(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_<storm::storage::SchedulerClass::MemoryPattern>(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_<storm::storage::SchedulerClass>(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<uint64_t>()); })
+        .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_<storm::Environment>(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_<storm::ModelCheckerEnvironment>(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<std::string>()); },
+            "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_<storm::MultiObjectiveModelCheckerEnvironment>(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<std::string>()); })
+        .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<std::string>()); })
+        .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<std::string>()); })
+        .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<uint64_t>()); })
+        .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<storm::storage::SchedulerClass>()); })
+        .def_property("print_results", &storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet, &storm::MultiObjectiveModelCheckerEnvironment::setPrintResults)
+        .def_property("lexicographic_model_checking", &storm::MultiObjectiveModelCheckerEnvironment::isLexicographicModelCheckingSet, &storm::MultiObjectiveModelCheckerEnvironment::setLexicographicModelChecking)
     ;
 
     py::class_<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers")
@@ -62,4 +163,3 @@ void define_environment(py::module& m) {
 
 
 }
-

src/core/modelchecking.cpp

@@ -59,6 +59,11 @@ std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalMdp(std::shared_p
     return checker.check(env, task);
 }
 
+std::shared_ptr<storm::modelchecker::CheckResult> checkRationalIntervalMdp(std::shared_ptr<storm::models::sparse::Mdp<storm::RationalInterval>> mdp, CheckTask<storm::RationalNumber> const& task, storm::Environment& env) {
+    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalInterval>>(*mdp);
+    return checker.check(env, task);
+}
+
 std::vector<double> computeAllUntilProbabilities(storm::Environment const& env, CheckTask<double> const& task, std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
     storm::solver::SolveGoal<double> 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<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());
     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<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));