Update monitoring and conditional model checking bindings

.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

@@ -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:

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)

src/core/environment.cpp

@@ -1,8 +1,15 @@
 #include "environment.h"
+#include <pybind11/pytypes.h>
+#include <storm/settings/SettingsManager.h>
+#include <storm/utility/constants.h>
 #include "src/helpers.h"
 #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"
 
 void define_environment(py::module& m) {
     py::enum_<storm::solver::EquationSolverType>(m, "EquationSolverType", "Solver type for equation systems")
@@ -36,9 +43,111 @@ 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::ConditionalModelCheckerEnvironment>(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking")
+        .def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm, "algorithm 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_<storm::ModelCheckerEnvironment>(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("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("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")
+    ;
+
+    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 +171,3 @@ void define_environment(py::module& m) {
 
 
 }
-

src/core/result.cpp

@@ -28,7 +28,7 @@ std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterSymboli
 void define_result(py::module& m) {
 
     // CheckResult
-    py::class_<storm::modelchecker::CheckResult, std::shared_ptr<storm::modelchecker::CheckResult>>(m, "_CheckResult", "Base class for all modelchecking results")
+    auto checkResult = py::class_<storm::modelchecker::CheckResult, std::shared_ptr<storm::modelchecker::CheckResult>>(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::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>, storm::modelchecker::CheckResult>(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results");
+    py::class_<storm::modelchecker::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult);
 
-    py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>, storm::modelchecker::QualitativeCheckResult>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result")
-        .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>::getTruthValuesVector, "Get Dd representing the truth values")
+    py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult)
+            .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>::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<ValueType>::getTruthValuesVector, "Get BitVector representing the truth values")
+        .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQualitativeCheckResult<ValueType> const& res) {return res.getScheduler();}, "get scheduler")
     ;
 
     py::class_<storm::modelchecker::QuantitativeCheckResult<ValueType>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<ValueType>>, 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<double>(py::module& m, std::string const& vtSuffix);
 template void define_typed_result<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
-template void define_typed_result<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+template void define_typed_result<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);

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<typename VT>
@@ -84,6 +85,16 @@ void define_transformation_typed(py::module& m, std::string const& vtSuffix) {
     m.def(("_construct_subsystem_" + vtSuffix).c_str(), &constructSubsystem<ValueType>, "build a subsystem of a sparse model");
 }
 
+template<typename ValueType>
+void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix) {
+    py::class_<storm::transformer::AddUncertainty<ValueType>>(m, ("AddUncertainty" + vtSuffix).c_str(), "Transform model into interval model with specified uncertainty")
+        .def(py::init<std::shared_ptr<storm::models::sparse::Model<ValueType>> const&>(), py::arg("model"))
+        .def("transform", &storm::transformer::AddUncertainty<ValueType>::transform, "transform the model", py::arg("additiveUncertainty"), py::arg("minimalValue") = storm::utility::convertNumber<ValueType>(0.0001), py::arg("maxSuccessors") = std::optional<uint64_t>{});
+}
+
 template void define_transformation_typed<double>(py::module& m, std::string const& vtSuffix);
 template void define_transformation_typed<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_transformation_typed<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+
+template void define_transformation_typed_only_numbers<double>(py::module& m, std::string const& vtSuffix);
+template void define_transformation_typed_only_numbers<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);

src/core/transformation.h

@@ -5,3 +5,5 @@
 void define_transformation(py::module& m);
 template<typename ValueType>
 void define_transformation_typed(py::module& m, std::string const& suffix);
+template<typename ValueType>
+void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix);