Exact intervals

resources/examples/testfiles/imdp/tiny-03.drn

@@ -14,8 +14,8 @@ state 0 init
 		1 : [0.4, 0.9]
 		2 : [0.5, 0.8]
 	action 1
-    	1 : [0.4, 0.9]
-    	2 : [0.5, 0.8]
+    	1 : [0.3, 0.7]
+    	2 : [0.4, 0.8]
 state 1 target
 	action 0
 		1 : [1, 1]

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -9,6 +9,7 @@
 
 #include "storm-parsers/parser/ValueParser.h"
 #include "storm/adapters/IntervalAdapter.h"
+#include "storm/adapters/IntervalForward.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/exceptions/AbortException.h"
@@ -87,6 +88,8 @@ bool isCompatibleValueType(DirectEncodingValueType fileValueType) {
         return fileValueType == Double || fileValueType == Rational;
     } else if constexpr (std::is_same_v<OutputValueType, storm::Interval>) {
         return fileValueType == Double || fileValueType == Rational || fileValueType == DoubleInterval || fileValueType == RationalInterval;
+    } else if constexpr (std::is_same_v<OutputValueType, storm::RationalInterval>) {
+        return fileValueType == Double || fileValueType == Rational || fileValueType == DoubleInterval || fileValueType == RationalInterval;
     } else if constexpr (std::is_same_v<OutputValueType, storm::RationalFunction>) {
         return fileValueType == Double || fileValueType == Rational || fileValueType == Parametric;
     } else {
@@ -581,6 +584,8 @@ template std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> pa
     std::filesystem::path const& file, DirectEncodingParserOptions const& options);
 template std::shared_ptr<storm::models::sparse::Model<storm::Interval>> parseDirectEncodingModel<storm::Interval>(std::filesystem::path const& file,
                                                                                                                   DirectEncodingParserOptions const& options);
+template std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> parseDirectEncodingModel<storm::RationalInterval>(
+    std::filesystem::path const& file, DirectEncodingParserOptions const& options);
 template std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> parseDirectEncodingModel<storm::RationalFunction>(
     std::filesystem::path const& file, DirectEncodingParserOptions const& options);
 

src/storm-parsers/parser/ValueParser.cpp

@@ -119,6 +119,51 @@ bool parseInterval(std::string const& value, storm::Interval& result) {
     return true;
 }
 
+bool parseRationalInterval(std::string const& value, storm::RationalInterval& result) {
+    // Try whether it is a constant.
+    if (storm::RationalNumber pointResult; parseNumber(value, pointResult)) {
+        result = storm::RationalInterval(pointResult);
+        return true;
+    }
+
+    std::string intermediate = value;
+    boost::trim(intermediate);
+    carl::BoundType leftBound;
+    carl::BoundType rightBound;
+    if (intermediate.front() == '(') {
+        leftBound = carl::BoundType::STRICT;
+    } else if (intermediate.front() == '[') {
+        leftBound = carl::BoundType::WEAK;
+    } else {
+        return false;  // Expect start with '(' or '['.
+    }
+    if (intermediate.back() == ')') {
+        rightBound = carl::BoundType::STRICT;
+    } else if (intermediate.back() == ']') {
+        rightBound = carl::BoundType::WEAK;
+    } else {
+        return false;  // Expected end with ')' or ']'.
+    }
+    intermediate = intermediate.substr(1, intermediate.size() - 2);
+
+    std::vector<std::string> words;
+    boost::split(words, intermediate, boost::is_any_of(","));
+    if (words.size() != 2) {
+        return false;  // Did not find exactly one comma.
+    }
+    storm::RationalNumber leftVal, rightVal;
+    boost::trim(words[0]);
+    if (!parseNumber(words[0], leftVal)) {
+        return false;  // lower value of interval invalid.
+    }
+    boost::trim(words[1]);
+    if (!parseNumber(words[1], rightVal)) {
+        return false;  // upper value of interval invalid.
+    }
+    result = storm::RationalInterval(leftVal, leftBound, rightVal, rightBound);
+    return true;
+}
+
 template<typename NumberType>
 bool parseNumber(std::string const& value, NumberType& result) {
     if constexpr (std::is_same_v<NumberType, double>) {
@@ -127,6 +172,8 @@ bool parseNumber(std::string const& value, NumberType& result) {
         return carl::try_parse(value, result);
     } else if constexpr (std::is_same_v<NumberType, storm::Interval>) {
         return parseInterval(value, result);
+    } else if constexpr (std::is_same_v<NumberType, storm::RationalInterval>) {
+        return parseRationalInterval(value, result);
     } else {
         return boost::conversion::try_lexical_convert(value, result);
     }
@@ -137,6 +184,7 @@ template class ValueParser<double>;
 template class ValueParser<storm::RationalNumber>;
 template class ValueParser<storm::RationalFunction>;
 template class ValueParser<storm::Interval>;
+template class ValueParser<storm::RationalInterval>;
 
 template std::size_t parseNumber<std::size_t>(std::string const&);
 

src/storm/adapters/IntervalForward.h

@@ -1,5 +1,7 @@
 #pragma once
 
+#include "storm/adapters/RationalNumberForward.h"
+
 namespace carl {
 template<typename Number>
 class Interval;
@@ -11,6 +13,7 @@ namespace storm {
  * Interval type
  */
 typedef carl::Interval<double> Interval;
+typedef carl::Interval<storm::RationalNumber> RationalInterval;
 
 namespace detail {
 template<typename ValueType>
@@ -23,6 +26,11 @@ struct IntervalMetaProgrammingHelper<Interval> {
     using BaseType = double;
     static const bool isInterval = true;
 };
+template<>
+struct IntervalMetaProgrammingHelper<RationalInterval> {
+    using BaseType = storm::RationalNumber;
+    static const bool isInterval = true;
+};
 }  // namespace detail
 
 /*!

src/storm/builder/ExplicitModelBuilder.cpp

@@ -431,6 +431,7 @@ template class ExplicitModelBuilder<RationalNumber, storm::models::sparse::Stand
 template class ExplicitModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
 template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;  // TODO: where is this used?
 template class ExplicitModelBuilder<storm::Interval, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
+template class ExplicitModelBuilder<storm::RationalInterval, storm::models::sparse::StandardRewardModel<storm::RationalInterval>, uint32_t>;
 
 }  // namespace builder
 }  // namespace storm

src/storm/builder/RewardModelBuilder.cpp

@@ -66,6 +66,7 @@ template class RewardModelBuilder<double>;
 template class RewardModelBuilder<storm::RationalNumber>;
 template class RewardModelBuilder<storm::RationalFunction>;
 template class RewardModelBuilder<storm::Interval>;
+template class RewardModelBuilder<storm::RationalInterval>;
 
 }  // namespace builder
 }  // namespace storm

src/storm/generator/Choice.cpp

@@ -205,5 +205,6 @@ template struct Choice<double>;
 template struct Choice<storm::RationalNumber>;
 template struct Choice<storm::RationalFunction>;
 template struct Choice<storm::Interval>;
+template struct Choice<storm::RationalInterval>;
 }  // namespace generator
 }  // namespace storm

src/storm/generator/Distribution.cpp

@@ -129,10 +129,12 @@ template class Distribution<uint32_t, double>;
 template class Distribution<uint32_t, storm::RationalNumber>;
 template class Distribution<uint32_t, storm::RationalFunction>;
 template class Distribution<uint32_t, storm::Interval>;
+template class Distribution<uint32_t, storm::RationalInterval>;
 
 template class Distribution<storm::storage::BitVector, double>;
 template class Distribution<storm::storage::BitVector, storm::RationalNumber>;
 template class Distribution<storm::storage::BitVector, storm::RationalFunction>;
 template class Distribution<storm::storage::BitVector, storm::Interval>;
+template class Distribution<storm::storage::BitVector, storm::RationalInterval>;
 
 }  // namespace storm::generator

src/storm/generator/DistributionEntry.cpp

@@ -1,4 +1,5 @@
 #include "storm/generator/DistributionEntry.h"
+#include <cstdint>
 
 #include "storm/adapters/IntervalAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -41,10 +42,12 @@ template class DistributionEntry<uint32_t, double>;
 template class DistributionEntry<uint32_t, storm::RationalNumber>;
 template class DistributionEntry<uint32_t, storm::RationalFunction>;
 template class DistributionEntry<uint32_t, storm::Interval>;
+template class DistributionEntry<uint32_t, storm::RationalInterval>;
 
 template class DistributionEntry<storm::storage::BitVector, double>;
 template class DistributionEntry<storm::storage::BitVector, storm::RationalNumber>;
 template class DistributionEntry<storm::storage::BitVector, storm::RationalFunction>;
 template class DistributionEntry<storm::storage::BitVector, storm::Interval>;
+template class DistributionEntry<storm::storage::BitVector, storm::RationalInterval>;
 
 }  // namespace storm::generator

src/storm/generator/NextStateGenerator.cpp

@@ -363,5 +363,9 @@ template class NextStateGenerator<storm::RationalFunction>;
 template class ActionMask<storm::Interval>;
 template class StateValuationFunctionMask<storm::Interval>;
 template class NextStateGenerator<storm::Interval>;
+
+template class ActionMask<storm::RationalInterval>;
+template class StateValuationFunctionMask<storm::RationalInterval>;
+template class NextStateGenerator<storm::RationalInterval>;
 }  // namespace generator
 }  // namespace storm

src/storm/generator/PrismNextStateGenerator.cpp

@@ -1100,5 +1100,6 @@ template class PrismNextStateGenerator<double>;
 template class PrismNextStateGenerator<storm::RationalNumber>;
 template class PrismNextStateGenerator<storm::RationalFunction>;
 template class PrismNextStateGenerator<storm::Interval>;
+template class PrismNextStateGenerator<storm::RationalInterval>;
 }  // namespace generator
 }  // namespace storm

src/storm/generator/StateBehavior.cpp

@@ -76,5 +76,6 @@ template class StateBehavior<double>;
 template class StateBehavior<storm::RationalNumber>;
 template class StateBehavior<storm::RationalFunction>;
 template class StateBehavior<storm::Interval>;
+template class StateBehavior<storm::RationalInterval>;
 }  // namespace generator
 }  // namespace storm

src/storm/io/DirectEncodingExporter.cpp

@@ -72,6 +72,8 @@ void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::
         os << "rational";
     } else if constexpr (std::is_same_v<ValueType, storm::Interval>) {
         os << "double-interval";
+    } else if constexpr (std::is_same_v<ValueType, storm::RationalInterval>) {
+        os << "rational-interval";
     } else if constexpr (std::is_same_v<ValueType, storm::RationalFunction>) {
         os << "parametric";
     } else {
@@ -338,5 +340,8 @@ template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& o
                                                                  std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);
 template void explicitExportSparseModel<storm::Interval>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::Interval>> sparseModel,
                                                          std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);
+template void explicitExportSparseModel<storm::RationalInterval>(std::ostream& os,
+                                                                 std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> sparseModel,
+                                                                 std::vector<std::string> const& parameters, DirectEncodingExporterOptions const& options);
 }  // namespace io
 }  // namespace storm

src/storm/modelchecker/AbstractModelChecker.cpp

@@ -473,6 +473,9 @@ template class AbstractModelChecker<storm::models::sparse::Smg<double>>;
 template class AbstractModelChecker<storm::models::sparse::Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
 template class AbstractModelChecker<storm::models::sparse::Smg<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
 
+template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>>;
+template class AbstractModelChecker<storm::models::sparse::Smg<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>>;
+
 template class AbstractModelChecker<storm::models::sparse::Model<storm::RationalNumber>>;
 template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
 template class AbstractModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
@@ -491,6 +494,9 @@ template class AbstractModelChecker<storm::models::sparse::Smg<storm::RationalFu
 template class AbstractModelChecker<storm::models::sparse::Mdp<storm::Interval>>;
 template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::Interval>>;
 
+template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalInterval>>;
+template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalInterval>>;
+
 // DD
 template class AbstractModelChecker<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>>;
 template class AbstractModelChecker<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>>;

src/storm/modelchecker/AbstractModelChecker.h

@@ -15,13 +15,31 @@ class CheckResult;
 
 template<typename ModelType>
 class AbstractModelChecker {
+   private:
+    // Due to a GCC bug we have to add this dummy template type here
+    // https://stackoverflow.com/questions/49707184/explicit-specialization-in-non-namespace-scope-does-not-compile-in-gcc
+    template<typename T, typename Dummy>
+    struct GetSolutionType {
+        using type = T;
+    };
+
+    template<typename Dummy>
+    struct GetSolutionType<storm::Interval, Dummy> {
+        using type = double;
+    };
+
+    template<typename Dummy>
+    struct GetSolutionType<storm::RationalInterval, Dummy> {
+        using type = storm::RationalNumber;
+    };
+
    public:
     virtual ~AbstractModelChecker() {
         // Intentionally left empty.
     }
 
     typedef typename ModelType::ValueType ValueType;
-    using SolutionType = typename std::conditional<std::is_same_v<ValueType, storm::Interval>, double, ValueType>::type;
+    using SolutionType = typename GetSolutionType<ValueType, void>::type;
 
     /*!
      * Returns the name of the model checker class (e.g., for display in error messages).

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -105,7 +105,8 @@ std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAu
     std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
     ExplicitQualitativeCheckResult<ValueType> const& subResult = subResultPointer->template asExplicitQualitativeCheckResult<ValueType>();
     std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNextProbabilities(
-        env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector());
+        env, checkTask.getOptimizationDirection(), checkTask.getUncertaintyResolutionMode(), this->getModel().getTransitionMatrix(),
+        subResult.getTruthValuesVector());
     return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
 }