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 37b8937005..e7df442dbd 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 02be704ce9..a1059487e4 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.
@@ -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:
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/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<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());
 }
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_<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) {
 
 
 }
-
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<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"));
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<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);
\ No newline at end of file
+template void define_typed_result<storm::RationalFunction>(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<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);
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<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);
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_<storm::logic::PathFormula, std::shared_ptr<storm::logic::PathFormula>> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula);
     py::class_<storm::logic::UnaryPathFormula, std::shared_ptr<storm::logic::UnaryPathFormula>> unaryPathFormula(m, "UnaryPathFormula", "Path formula with one operand", pathFormula);
     unaryPathFormula.def_property_readonly("subformula", &storm::logic::UnaryPathFormula::getSubformula, "the subformula");
-    py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula>>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula);
+    py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula>>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula)
+    .def_property_readonly("subformula", &storm::logic::EventuallyFormula::getSubformula, "the subformula");
     py::class_<storm::logic::GloballyFormula, std::shared_ptr<storm::logic::GloballyFormula>>(m, "GloballyFormula", "Formula for globally", unaryPathFormula);
     py::class_<storm::logic::BinaryPathFormula, std::shared_ptr<storm::logic::BinaryPathFormula>> 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_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula>>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula);
+    py::class_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula>>(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_<storm::logic::UntilFormula, std::shared_ptr<storm::logic::UntilFormula>>(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<double>(m, "Double");
     define_transformation_typed<storm::RationalNumber>(m, "Exact");
     define_transformation_typed<storm::RationalFunction>(m, "RatFunc");
+    define_transformation_typed_only_numbers<double>(m, "Double");
+    define_transformation_typed_only_numbers<storm::RationalNumber>(m, "Exact");
     define_sparse_model_simulator<double>(m, "Double");
     define_sparse_model_simulator<storm::RationalNumber>(m, "Exact");
     define_prism_program_simulator<double>(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 <storm/adapters/RationalFunctionAdapter.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/adapters/IntervalAdapter.h>
+#include "pomdp/generator.h"
 #include "pomdp/memory.h"
+#include "pomdp/qualitative_analysis.h"
 #include "pomdp/quantitative_analysis.h"
-#include <storm/adapters/RationalFunctionAdapter.h>
+#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<double>(m, "Double");
     define_transformations<storm::RationalNumber>(m, "Exact");
-    define_belief_exploration<double>(m, "Double");
-
     define_transformations<storm::RationalFunction>(m, "Rf");
+
+    define_transformations_int<double>(m, "Double");
+    define_transformations_int<storm::RationalNumber>(m, "Exact");
+    define_transformations_int<storm::RationalFunction>(m, "Rf");
+    define_transformations_int<storm::Interval>(m, "Interval");
+    define_transformations_int<storm::RationalInterval>(m, "RationalInterval");
+
+    define_belief_exploration<double>(m, "Double");
+    define_verimon_generator<double>(m, "Double");
+    define_verimon_generator<storm::RationalNumber>(m, "Exact");
 }
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<storm::RationalNumber>(m, "Exact");
     define_sparse_model<storm::Interval>(m, "Interval");
     define_sparse_model<storm::RationalFunction>(m, "Parametric");
+    define_sparse_model<storm::RationalInterval>(m, "RationalInterval");
     define_statevaluation(m);
     define_statevaluation_transformer(m);
     define_simplevaluation(m);
     define_sparse_matrix<double>(m, "");
     define_sparse_matrix<storm::RationalNumber>(m, "Exact");
     define_sparse_matrix<storm::Interval>(m, "Interval");
+    define_sparse_matrix<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_matrix<storm::RationalFunction>(m, "Parametric");
     define_sparse_matrix_nt(m);
     define_symbolic_model<storm::dd::DdType::Sylvan, double>(m, "Sylvan");
@@ -51,6 +53,7 @@ PYBIND11_MODULE(_storage, m) {
     define_state<double>(m, "");
     define_state<storm::RationalNumber>(m, "Exact");
     define_state<storm::Interval>(m, "Interval");
+    define_state<storm::RationalInterval>(m, "RationalInterval");
     define_state<storm::RationalFunction>(m, "Parametric");
     define_memorystructure_typed<double>(m, "");
     define_memorystructure_typed<storm::RationalNumber>(m, "Exact");
@@ -66,13 +69,16 @@ PYBIND11_MODULE(_storage, m) {
     define_scheduler<double>(m, "");
     define_scheduler<storm::RationalNumber>(m, "Exact");
     define_scheduler<storm::Interval>(m, "Interval");
+    define_scheduler<storm::RationalInterval>(m, "RationalInterval");
     define_scheduler<storm::RationalFunction>(m, "Parametric");
     define_distribution<double>(m, "");
     define_distribution<storm::RationalNumber>(m, "Exact");
     define_distribution<storm::Interval>(m, "Interval");
+    define_distribution<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_model_components<double>(m, "");
     define_sparse_model_components<storm::RationalNumber>(m, "Exact");
     define_sparse_model_components<storm::Interval>(m, "Interval");
+    define_sparse_model_components<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_model_components<storm::RationalFunction>(m, "Parametric");
     define_geometry<double>(m, "Double");
     define_geometry<storm::RationalNumber>(m, "Exact");
@@ -81,6 +87,6 @@ PYBIND11_MODULE(_storage, m) {
     define_maximal_end_component_decomposition<double>(m, "_double");
     define_maximal_end_component_decomposition<storm::RationalNumber>(m, "_exact");
     define_maximal_end_component_decomposition<storm::Interval>(m, "_interval");
+    define_maximal_end_component_decomposition<storm::RationalInterval>(m, "_ratinterval");
     define_maximal_end_component_decomposition<storm::RationalFunction>(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<double>(m, "Double");
-    define_json<storm::RationalNumber>(m, "Rational");
+  define_ksp(m);
+  define_smt(m);
+  define_chrono(m);
+  define_json<double>(m, "Double");
+  define_json<storm::RationalNumber>(m, "Rational");
+  define_kwek_mehlhorn<storm::RationalNumber>(m, "");
 }
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 <cstdint>
+#include <string>
+#include "storm-pomdp/generator/GenerateMonitorVerifier.h"
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+template<typename ValueType>
+using GenerateMonitorVerifier = storm::generator::GenerateMonitorVerifier<ValueType>;
+template<typename ValueType>
+using SparseDtmc = storm::models::sparse::Dtmc<ValueType>;
+template<typename ValueType>
+using SparseMdp = storm::models::sparse::Mdp<ValueType>;
+template<typename ValueType>
+using SparsePomdp = storm::models::sparse::Pomdp<ValueType>;
+template<typename ValueType>
+using GenerateMonitorVerifierOptions = typename storm::generator::GenerateMonitorVerifier<ValueType>::Options;
+
+template<typename ValueType>
+void define_verimon_generator(py::module &m, std::string const &vtSuffix) {
+    py::class_<storm::generator::MonitorVerifier<ValueType>, std::shared_ptr<storm::generator::MonitorVerifier<ValueType>>> mv(
+        m, ("MonitorVerifier" + vtSuffix).c_str(), "Container for monitor verifier POMDP with associated objects");
+    mv.def(py::init<const SparsePomdp<ValueType> &, const std::map<std::pair<uint32_t, bool>, uint32_t> &, const std::map<uint32_t, std::string> &>(),
+           py::arg("product"), py::arg("observation_map"), py::arg("default_action_map"));
+    mv.def("get_product", &storm::generator::MonitorVerifier<ValueType>::getProduct, py::return_value_policy::copy);
+    mv.def_property_readonly("observation_map", &storm::generator::MonitorVerifier<ValueType>::getObservationMap, py::return_value_policy::copy);
+    mv.def_property_readonly("default_action_map", &storm::generator::MonitorVerifier<ValueType>::getObservationDefaultAction, py::return_value_policy::copy);
+
+    py::class_<storm::generator::GenerateMonitorVerifier<ValueType>> gmv(m, ("GenerateMonitorVerifier" + vtSuffix).c_str(),
+                                                                         "Generator of POMDP used in verifying monitors against markov chains");
+    gmv.def(py::init<SparseDtmc<ValueType> const &, SparseMdp<ValueType> const &, std::shared_ptr<storm::expressions::ExpressionManager> &,
+                     GenerateMonitorVerifierOptions<ValueType> const &>(),
+            py::arg("mc"), py::arg("monitor"), py::arg("expr_manager"), py::arg("options"));
+    gmv.def("create_product", &storm::generator::GenerateMonitorVerifier<ValueType>::createProduct, py::return_value_policy::copy,
+            "Created the verification POMDP");
+    gmv.def("set_risk", &storm::generator::GenerateMonitorVerifier<ValueType>::setRisk, py::arg("risk"));
+
+    py::class_<GenerateMonitorVerifierOptions<ValueType>> gmvopts(m, ("GenerateMonitorVerifier" + vtSuffix + "Options").c_str(),
+                                                                  "Options for corresponding generator");
+    gmvopts.def(py::init<>());
+    gmvopts.def_readwrite("accepting_label", &GenerateMonitorVerifierOptions<ValueType>::acceptingLabel);
+    gmvopts.def_readwrite("step_prefix", &GenerateMonitorVerifierOptions<ValueType>::stepPrefix);
+    gmvopts.def_readwrite("horizon_label", &GenerateMonitorVerifierOptions<ValueType>::horizonLabel);
+    gmvopts.def_readwrite("use_restart_semantics", &GenerateMonitorVerifierOptions<ValueType>::useRestartSemantics);
+}
+
+template void define_verimon_generator<double>(py::module &m, std::string const &vtSuffix);
+template void define_verimon_generator<storm::RationalNumber>(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<typename ValueType>
+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<typename ValueType> using SparsePomdp = storm::models::sparse::Pomdp<Va
 template<typename ValueType> using SparsePomdpTracker = storm::generator::BeliefSupportTracker<ValueType>;
 
 template<typename ValueType> using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker<ValueType, storm::generator::SparseBeliefState<ValueType>>;
-template<typename ValueType> using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker<ValueType, storm::generator::ObservationDenseBeliefState<ValueType>>;
 
 
 template<typename ValueType>
@@ -49,17 +48,6 @@ void define_tracker(py::module& m, std::string const& vtSuffix) {
     ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse<ValueType>::getCurrentObservation);
     ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse<ValueType>::reduce);
     ndetbelieftracker.def("reduction_timed_out", &NDPomdpTrackerSparse<ValueType>::hasTimedOut);
-
-//    py::class_<NDPomdpTrackerDense<double>> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions");
-//    ndetbelieftrackerd.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp"));
-//    ndetbelieftrackerd.def("reset", &NDPomdpTrackerDense<double>::reset);
-//    ndetbelieftrackerd.def("set_risk", &NDPomdpTrackerDense<double>::setRisk, py::arg("risk"));
-//    ndetbelieftrackerd.def("obtain_current_risk",&NDPomdpTrackerDense<double>::getCurrentRisk, py::arg("max")=true);
-//    ndetbelieftrackerd.def("track", &NDPomdpTrackerDense<double>::track, py::arg("observation"));
-//    ndetbelieftrackerd.def("obtain_beliefs", &NDPomdpTrackerDense<double>::getCurrentBeliefs);
-//    ndetbelieftrackerd.def("obtain_last_observation", &NDPomdpTrackerDense<double>::getCurrentObservation);
-//    ndetbelieftrackerd.def("reduce",&NDPomdpTrackerDense<double>::reduce);
-
 }
 
 template void define_tracker<double>(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<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::models::sparse::Pomdp<ValueType> const& pomdp) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::models::sparse::Pomdp<ValueType> const &pomdp) {
     storm::transformer::MakePOMDPCanonic<ValueType> makeCanonic(pomdp);
     return makeCanonic.transform();
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels, bool keepStateValuations) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                       storm::storage::PomdpMemory const &memory, bool addMemoryLabels,
+                                                                       bool keepStateValuations) {
     storm::transformer::PomdpMemoryUnfolder<ValueType> unfolder(pomdp, memory, addMemoryLabels, keepStateValuations);
     return unfolder.transform();
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool keepStateValuations) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const &pomdp, bool keepStateValuations) {
     storm::transformer::BinaryPomdpTransformer<ValueType> transformer;
-    return transformer.transform(pomdp,true, keepStateValuations).transformedPomdp;
+    return transformer.transform(pomdp, true, keepStateValuations).transformedPomdp;
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> apply_unknown_fsc(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::transformer::PomdpFscApplicationMode const& applicationMode) {
+std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> apply_unknown_fsc(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                                         storm::transformer::PomdpFscApplicationMode const &applicationMode) {
     storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> transformer(pomdp);
     return transformer.transform(applicationMode);
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Mdp<ValueType>> unfold_trace(storm::models::sparse::Pomdp<ValueType> const& pomdp, std::shared_ptr<storm::expressions::ExpressionManager>& exprManager, std::vector<uint32_t> const& observationTrace, std::vector<ValueType> const& riskDef ) {
-    storm::pomdp::ObservationTraceUnfolder<ValueType> transformer(pomdp, exprManager);
-    return transformer.transform(observationTrace, riskDef);
+std::shared_ptr<storm::models::sparse::Mdp<ValueType>> unfold_trace(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                    std::shared_ptr<storm::expressions::ExpressionManager> &exprManager,
+                                                                    std::vector<uint32_t> const &observationTrace, std::vector<ValueType> const &riskDef,
+                                                                    bool restartSemantics = true) {
+    storm::pomdp::ObservationTraceUnfolderOptions options = storm::pomdp::ObservationTraceUnfolderOptions();
+    options.useRestartSemantics = restartSemantics;
+    storm::pomdp::ObservationTraceUnfolder<ValueType> 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_<storm::transformer::PomdpFscApplicationMode>(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_<storm::pomdp::ObservationTraceUnfolderOptions> 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<typename ValueType>
-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<ValueType>, "Return a canonicly-ordered POMDP", py::arg("pomdp"));
-    m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory<ValueType>, "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<ValueType>, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false);
-    m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
-    //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace<ValueType>, "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<ValueType>, "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<ValueType>, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations") = false);
+    m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC", py::arg("pomdp"),
+          py::arg("application_mode") = storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
+}
 
-    py::class_<storm::pomdp::ObservationTraceUnfolder<ValueType>> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models");
-    unfolder.def(py::init<storm::models::sparse::Pomdp<ValueType> const&,  std::vector<ValueType> const&, std::shared_ptr<storm::expressions::ExpressionManager>&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"));
+template<typename ValueType>
+void define_transformations_int(py::module &m, std::string const &vtSuffix) {
+    py::class_<storm::pomdp::ObservationTraceUnfolder<ValueType>> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(),
+                                                                           "Unfolds observation traces in models");
+    unfolder.def(py::init<storm::models::sparse::Pomdp<ValueType>, std::vector<ValueType> const &, std::shared_ptr<storm::expressions::ExpressionManager> &,
+                          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<ValueType>::isRestartSemanticsSet);
     unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder<ValueType>::transform, py::arg("trace"));
-    unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<ValueType>::extend, py::arg("new_observation"));
     unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder<ValueType>::reset, py::arg("new_observation"));
+    unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<ValueType>::extend, py::arg("new_observation"));
 }
 
-template void define_transformations<double>(py::module& m, std::string const& vtSuffix);
-template void define_transformations<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
-template void define_transformations<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+template void define_transformations<double>(py::module &m, std::string const &vtSuffix);
+template void define_transformations<storm::RationalNumber>(py::module &m, std::string const &vtSuffix);
+template void define_transformations<storm::RationalFunction>(py::module &m, std::string const &vtSuffix);
+
+template void define_transformations_int<double>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalNumber>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalFunction>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::Interval>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalInterval>(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<typename VT>
-void define_transformations(py::module& m, std::string const& vtSuffix);
+void define_transformations_nt(py::module &m);
+template <typename VT>
+void define_transformations(py::module &m, std::string const &vtSuffix);
+template <typename VT>
+void define_transformations_int(py::module &m, std::string const &vtSuffix);
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<double>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::Interval>(py::module& m, std::string const& vt_suffix);
+template void define_maximal_end_component_decomposition<storm::RationalInterval>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalFunction>(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<double>(py::module&, std::string vt_suffix);
 template void define_distribution<storm::RationalNumber>(py::module&, std::string vt_suffix);
 template void define_distribution<storm::Interval>(py::module&, std::string vt_suffix);
+template void define_distribution<storm::RationalInterval>(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<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_matrix<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalFunction>(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<SparseDtmc<storm::RationalFunction>>();
             }, "Get model as sparse parametric DTMC")
+        .def("_as_sparse_idtmc", [](ModelBase &modelbase) {
+                return modelbase.as<SparseDtmc<storm::Interval>>();
+            }, "Get model as sparse interval DTMC")
+        .def("_as_sparse_exact_idtmc", [](ModelBase &modelbase) {
+                return modelbase.as<SparseDtmc<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval DTMC")
         .def("_as_sparse_mdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<double>>();
             }, "Get model as sparse MDP")
@@ -125,18 +131,24 @@ void define_model(py::module& m) {
         .def("_as_sparse_imdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<storm::Interval>>();
             }, "Get model as sparse interval MDP")
+        .def("_as_sparse_exact_imdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparseMdp<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval MDP")
         .def("_as_sparse_pmdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<storm::RationalFunction>>();
             }, "Get model as sparse parametric MDP")
         .def("_as_sparse_pomdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparsePomdp<double>>();
             }, "Get model as sparse POMDP")
+        .def("_as_sparse_ipomdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparsePomdp<storm::Interval>>();
+            }, "Get model as sparse interval POMDP")
+        .def("_as_sparse_exact_ipomdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparsePomdp<storm::RationalInterval>>();
+            }, "Get model as sparse interval exact POMDP")
         .def("_as_sparse_exact_pomdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparsePomdp<storm::RationalNumber>>();
             }, "Get model as sparse exact POMDP")
-        .def("_as_sparse_ipomdp", [](ModelBase &modelbase) {
-            return modelbase.as<SparsePomdp<storm::Interval>>();
-            }, "Get model as sparse interval POMDP")
         .def("_as_sparse_ppomdp", [](ModelBase &modelbase) {
             return modelbase.as<SparsePomdp<storm::RationalFunction>>();
             }, "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<double>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::Interval>(py::module& m, std::string const& vt_suffix);
+template void define_sparse_model<storm::RationalInterval>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
 
 template void define_symbolic_model<storm::dd::DdType::Sylvan, double>(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<ValueType>::observabilityClasses, "The POMDP observations")
+        .def_readwrite("observation_valuations", &SparseModelComponents<ValueType>::observationValuations, "The POMDP observation valuations")
 
         // Continuous time specific components (CTMCs, Markov Automata):
         .def_readwrite("rate_transitions", &SparseModelComponents<ValueType>::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<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_model_components<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::RationalFunction>(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<storm::models::sparse::Model<ValueType>> 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<ValueType, storm::Interval>) {
+    if constexpr (!std::is_same_v<ValueType, storm::Interval> && !std::is_same_v<ValueType, storm::RationalInterval>) {
         // Conversion from Interval not implemented
         scheduler
             .def("cast_to_double_datatype", &Scheduler::template toValueType<double>, "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<ValueType, storm::RationalFunction>) {
             // Conversion from RationalFunction to Interval not implemented
             scheduler.def("cast_to_interval_datatype", &Scheduler::template toValueType<storm::Interval>, "Construct the scheduler with `interval` value type");
+            scheduler.def("cast_to_exact_interval_datatype", &Scheduler::template toValueType<storm::RationalInterval>, "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<double>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::RationalNumber>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::Interval>(py::module& m, std::string vt_suffix);
+template void define_scheduler<storm::RationalInterval>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::RationalFunction>(py::module& m, std::string vt_suffix);
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<double>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_state<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::RationalFunction>(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 <pybind11/pybind11.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/utility/KwekMehlhorn.h>
+
+template <typename RationalValueType>
+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<RationalValueType,
+                                                      double>(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<storm::RationalNumber>(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 <typename RationalValueType>
+void define_kwek_mehlhorn(py::module &m, std::string const &vtSuffix);
\ No newline at end of file