Add exact interval (RationalInterval) support

lib/stormpy/__init__.py

@@ -27,6 +27,7 @@ class _ValueType(Enum):
     EXACT = 2
     PARAMETRIC = 3
     INTERVAL = 4
+    EXACT_INTERVAL = 5
 
 
 def _convert_sparse_model(model, value_type=_ValueType.DOUBLE):
@@ -103,6 +104,22 @@ def _convert_sparse_model(model, value_type=_ValueType.DOUBLE):
                 return model._as_sparse_ismg()
             else:
                 raise stormpy.exceptions.StormError("Not supported interval model constructed")
+        case _ValueType.EXACT_INTERVAL:
+            assert model.supports_uncertainty and model.is_exact
+            if model.model_type == ModelType.DTMC:
+                return model._as_sparse_exact_idtmc()
+            elif model.model_type == ModelType.MDP:
+                return model._as_sparse_exact_imdp()
+            elif model.model_type == ModelType.POMDP:
+                return model._as_sparse_exact_ipomdp()
+            elif model.model_type == ModelType.CTMC:
+                return model._as_sparse_exact_ictmc()
+            elif model.model_type == ModelType.MA:
+                return model._as_sparse_exact_ima()
+            elif model.model_type == ModelType.SMG:
+                return model._as_sparse_exact_ismg()
+            else:
+                raise stormpy.exceptions.StormError("Not supported exact interval model constructed")
         case _:
             raise stormpy.exceptions.StormError("Not supported model type constructed")
 
@@ -238,6 +255,25 @@ def build_sparse_interval_model(symbolic_description, properties=None):
     return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL)
 
 
+def build_sparse_exact_interval_model(symbolic_description, properties=None):
+    """
+    Build an exact interval model in sparse representation from a symbolic description.
+
+    :param symbolic_description: Symbolic model description to translate into a model.
+    :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
+    :return: Exact interval model in sparse representation.
+    """
+    if not symbolic_description.undefined_constants_are_graph_preserving:
+        raise stormpy.exceptions.StormError("Program still contains undefined constants")
+
+    if properties:
+        formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
+        intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description, formulae)
+    else:
+        intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description)
+    return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL)
+
+
 def build_symbolic_model(symbolic_description, properties=None):
     """
     Build a model in symbolic representation from a symbolic description.
@@ -312,6 +348,18 @@ 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)
+    return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL)
+
+
 def perform_bisimulation(model, properties, bisimulation_type, graph_preserving=True):
     """
     Perform bisimulation on model.
@@ -741,6 +789,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/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

@@ -124,16 +124,19 @@ void define_build(py::module& m) {
     m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel<storm::RationalNumber>, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_interval_model_from_symbolic_description", &buildSparseModel<storm::Interval>, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
+    m.def("_build_sparse_exact_interval_model_from_symbolic_description", &buildSparseModel<storm::RationalInterval>, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("build_sparse_model_with_options", &buildSparseModelWithOptions<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_exact_model_with_options", &buildSparseModelWithOptions<storm::RationalNumber>, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions<storm::RationalFunction>, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_interval_model_with_options", &buildSparseModelWithOptions<storm::Interval>, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("options"));
+    m.def("build_sparse_exact_interval_model_with_options", &buildSparseModelWithOptions<storm::RationalInterval>, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     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 +210,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/modelchecking.cpp

@@ -54,11 +54,21 @@ std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalDtmc(std::shared_
     return checker.check(env, task);
 }
 
+std::shared_ptr<storm::modelchecker::CheckResult> checkRationalIntervalDtmc(std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalInterval>> dtmc, CheckTask<storm::RationalNumber> const& task, storm::Environment& env) {
+    auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalInterval>>(*dtmc);
+    return checker.check(env, task);
+}
+
 std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalMdp(std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp, CheckTask<double> const& task, storm::Environment& env) {
     auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
     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);
@@ -146,7 +156,9 @@ void define_modelchecking(py::module& m) {
     m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, double>, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
     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_exact_interval_dtmc", &checkRationalIntervalDtmc, "Check exact interval DTMC");
     m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP");
+    m.def("check_exact_interval_mdp", &checkRationalIntervalMdp, "Check exact interval MDP");
     m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities");
     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"));

src/helpers.h

@@ -28,4 +28,3 @@ std::string containerToString(T& t) {
 // Be warned: Enabling something like this will break everything about Monomial,
 // as to Python the shared_ptr (Arg) IS the Monomial
 //  //PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T>);
-

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";

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");
-
 }

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, "");
 }

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);

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);