Add upper and lowerbounds to check results.

resources/examples/testfiles/mdp/maybe_state_end_component.nm

@@ -0,0 +1,15 @@
+// An MDP whose maybe states contain an end component: staying in x=0 or x=1 forever is a choice, so a sound
+// method has to eliminate that end component before it can solve for the maximal probability of reaching x=2.
+mdp
+
+module main
+	x : [0..3];
+
+	[] x=0 -> (x'=0);
+	[] x=0 -> 0.5 : (x'=1) + 0.5 : (x'=3);
+	[] x=1 -> (x'=0);
+	[] x=1 -> 0.5 : (x'=2) + 0.5 : (x'=3);
+	[] x>=2 -> true;
+endmodule
+
+label "target" = x=2;

src/storm-counterexamples/api/counterexamples.cpp

@@ -51,7 +51,7 @@ std::shared_ptr<storm::counterexamples::Counterexample> computeKShortestPathCoun
     storm::storage::BitVector phiStates(model->getNumberOfStates(), true);
     auto results = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeUntilProbabilities(
         env, false, model->getTransitionMatrix(), model->getBackwardTransitions(), phiStates, subQualitativeResult.getTruthValuesVector(), true);
-    double reachProb = results.at(initialState);
+    double reachProb = results.values.at(initialState);
     STORM_LOG_THROW((reachProb > threshold) || (strictBound && reachProb >= threshold), storm::exceptions::InvalidArgumentException,
                     "Given probability threshold " << threshold << " cannot be " << (strictBound ? "achieved" : "exceeded")
                                                    << " in model with maximal reachability probability of " << reachProb << ".");

src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -1669,7 +1669,8 @@ class SMTMinimalLabelSetGenerator {
             if (rewardName == boost::none) {
                 results.push_back(storm::utility::zero<T>());
                 allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<T>::computeUntilProbabilities(
-                    env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false);
+                                      env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false)
+                                      .values;
                 for (auto state : model.getInitialStates()) {
                     STORM_LOG_TRACE("Found probability " << allStatesResult[state]);
                     results.back() = std::max(results.back(), allStatesResult[state]);
@@ -1689,10 +1690,10 @@ class SMTMinimalLabelSetGenerator {
             if (rewardName == boost::none) {
                 results.push_back(storm::utility::zero<T>());
                 storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
-                allStatesResult = std::move(
+                allStatesResult =
                     modelCheckerHelper
                         .computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, false)
-                        .values);
+                        .values;
                 for (auto state : model.getInitialStates()) {
                     results.back() = std::max(results.back(), allStatesResult[state]);
                 }

src/storm-dft/modelchecker/DFTModelChecker.cpp

@@ -471,7 +471,7 @@ std::vector<typename DFTModelChecker<ValueType>::ExtendedValueType> DFTModelChec
 
         if (result) {
             result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>(model->getInitialStates()));
-            results.push_back(result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second);
+            results.push_back(result->asExplicitQuantitativeCheckResult<ValueType>().getValueVector().front());
         } else {
             STORM_LOG_WARN("The property '" << *property << "' could not be checked with the current settings.");
             results.push_back(-storm::utility::one<ExtendedValueType>());

src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1286,8 +1286,10 @@ void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection cons
             }
         }
         auto dtmcMatrix = dtmcMatrixBuilder.build();
-        std::vector<ValueType> sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(
-            Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
+        std::vector<ValueType> sanityValues =
+            storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(
+                Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false)
+                .values;
 
         ValueType maxDiff = storm::utility::zero<ValueType>();
         uint64_t maxState = 0;
@@ -1325,7 +1327,8 @@ void postProcessStrategies(uint64_t iteration, storm::OptimizationDirection cons
         }
         dtmcMatrix = dtmcMatrixBuilder.build();
         sanityValues = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(
-            Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false);
+                           Environment(), storm::solver::SolveGoal<ValueType>(), dtmcMatrix, dtmcMatrix.transpose(), constraintStates, targetStates, false)
+                           .values;
 
         maxDiff = storm::utility::zero<ValueType>();
         maxState = 0;

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -95,8 +95,9 @@ std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::com
     ExplicitQualitativeCheckResult<ValueType> const& subResult = subResultPointer->template asExplicitQualitativeCheckResult<ValueType>();
     auto probabilisticTransitions = this->getModel().computeProbabilityMatrix();
     std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeGloballyProbabilities(
-        env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), probabilisticTransitions, probabilisticTransitions.transpose(),
-        subResult.getTruthValuesVector(), checkTask.isQualitativeSet());
+                                               env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), probabilisticTransitions,
+                                               probabilisticTransitions.transpose(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet())
+                                               .values;
     return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
 }
 

src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -259,7 +259,8 @@ std::vector<ValueType> SparseCtmcCslHelper::computeUntilProbabilities(Environmen
                                                                       std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& phiStates,
                                                                       storm::storage::BitVector const& psiStates, bool qualitative) {
     return SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env, std::move(goal), computeProbabilityMatrix(rateMatrix, exitRateVector),
-                                                                       backwardTransitions, phiStates, psiStates, qualitative);
+                                                                       backwardTransitions, phiStates, psiStates, qualitative)
+        .values;
 }
 
 template<typename ValueType>

src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp

@@ -315,8 +315,9 @@ std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAPr
 
     } else {
         prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(
-            env, std::move(solveGoalProduct), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions(), bvTrue,
-            acceptingStates, this->isQualitativeSet());
+                                env, std::move(solveGoalProduct), product->getProductModel().getTransitionMatrix(),
+                                product->getProductModel().getBackwardTransitions(), bvTrue, acceptingStates, this->isQualitativeSet())
+                                .values;
     }
 
     std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_transitionMatrix.getRowGroupCount(), prodNumericResult);

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -98,7 +98,8 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
         auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
         auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeRewardBoundedValues(
             env, this->getModel(), formula);
-        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
+        // The helper returns one value per initial state, in the order in which the bit vector selects them.
+        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(this->getModel().getInitialStates(), std::move(numericResult)));
     } else {
         STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
         STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula lower step bound must be discrete/integral.");
@@ -151,12 +152,13 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
     std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
     ExplicitQualitativeCheckResult<SolutionType> const& leftResult = leftResultPointer->template asExplicitQualitativeCheckResult<SolutionType>();
     ExplicitQualitativeCheckResult<SolutionType> const& rightResult = rightResultPointer->template asExplicitQualitativeCheckResult<SolutionType>();
-    std::vector<SolutionType> numericResult =
-        storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeUntilProbabilities(
-            env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
-            this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
-            checkTask.getHint());
-    return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
+    auto ret = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeUntilProbabilities(
+        env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
+        this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
+        checkTask.getHint());
+    auto result = std::make_unique<ExplicitQuantitativeCheckResult<SolutionType>>(std::move(ret.values));
+    result->setBounds(std::move(ret.solutionBounds));
+    return result;
 }
 
 template<typename SparseDtmcModelType>
@@ -168,11 +170,12 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
         storm::logic::GloballyFormula const& pathFormula = checkTask.getFormula();
         std::unique_ptr<CheckResult> subResultPointer = this->check(env, pathFormula.getSubformula());
         ExplicitQualitativeCheckResult<SolutionType> const& subResult = subResultPointer->template asExplicitQualitativeCheckResult<SolutionType>();
-        std::vector<SolutionType> numericResult =
-            storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeGloballyProbabilities(
-                env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
-                this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet());
-        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
+        auto ret = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeGloballyProbabilities(
+            env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
+            this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet());
+        auto result = std::make_unique<ExplicitQuantitativeCheckResult<SolutionType>>(std::move(ret.values));
+        result->setBounds(std::move(ret.solutionBounds));
+        return result;
     }
 }
 
@@ -236,7 +239,8 @@ std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::c
             auto formula = std::make_shared<storm::logic::RewardOperatorFormula>(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo);
             auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType, RewardModelType, SolutionType>::computeRewardBoundedValues(
                 env, this->getModel(), formula);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            // The helper returns one value per initial state, in the order in which the bit vector selects them.
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->getModel().getInitialStates(), std::move(numericResult)));
         } else {
             STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
             auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -134,7 +134,9 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
             helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
             auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, SolutionType>::computeRewardBoundedValues(
                 env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
+            // The helper returns one value per initial state, in the order in which the bit vector selects them.
+            return std::unique_ptr<CheckResult>(
+                new ExplicitQuantitativeCheckResult<SolutionType>(this->getModel().getInitialStates(), std::move(numericResult)));
         }
     } else {
         STORM_LOG_THROW(pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper step bound.");
@@ -182,6 +184,7 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
         this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(),
         checkTask.isProduceSchedulersSet(), checkTask.getHint());
     std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
+    result->asExplicitQuantitativeCheckResult<SolutionType>().setBounds(std::move(ret.solutionBounds));
     if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
         result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
     }
@@ -200,6 +203,7 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
         env, storm::solver::SolveGoal<ValueType, SolutionType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(),
         this->getModel().getBackwardTransitions(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet());
     std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(ret.values)));
+    result->asExplicitQuantitativeCheckResult<SolutionType>().setBounds(std::move(ret.solutionBounds));
     if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
         result->asExplicitQuantitativeCheckResult<SolutionType>().setScheduler(std::move(ret.scheduler));
     }
@@ -314,7 +318,8 @@ std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::com
         helper::rewardbounded::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
         auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType, SolutionType>::computeRewardBoundedValues(
             env, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates());
-        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(std::move(numericResult)));
+        // The helper returns one value per initial state, in the order in which the bit vector selects them.
+        return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<SolutionType>(this->getModel().getInitialStates(), std::move(numericResult)));
     } else {
         STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
         auto rewardModel = storm::utility::createFilteredRewardModel(this->getModel(), checkTask);

src/storm/modelchecker/prctl/helper/DTMCModelCheckingHelperReturnType.h

@@ -0,0 +1,34 @@
+#pragma once
+
+#include <utility>
+#include <vector>
+
+#include "storm/solver/SolutionBounds.h"
+
+namespace storm {
+namespace modelchecker {
+namespace helper {
+
+/*!
+ * The outcome of a quantitative model checking query on a sparse DTMC. Unlike its MDP counterpart it carries no
+ * scheduler, as a DTMC has no nondeterminism to resolve.
+ */
+template<typename ValueType>
+struct DTMCSparseModelCheckingHelperReturnType {
+    DTMCSparseModelCheckingHelperReturnType(DTMCSparseModelCheckingHelperReturnType const&) = delete;
+    DTMCSparseModelCheckingHelperReturnType(DTMCSparseModelCheckingHelperReturnType&&) = default;
+    DTMCSparseModelCheckingHelperReturnType& operator=(DTMCSparseModelCheckingHelperReturnType&&) = default;
+
+    explicit DTMCSparseModelCheckingHelperReturnType(std::vector<ValueType>&& values) : values(std::move(values)) {
+        // Intentionally left empty.
+    }
+
+    // The values computed for the states.
+    std::vector<ValueType> values;
+
+    storm::solver::SolutionBounds<ValueType> solutionBounds;
+};
+
+}  // namespace helper
+}  // namespace modelchecker
+}  // namespace storm

src/storm/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h

@@ -2,6 +2,7 @@
 
 #include <memory>
 #include <vector>
+#include "storm/solver/SolutionBounds.h"
 #include "storm/storage/Scheduler.h"
 
 namespace storm {
@@ -30,6 +31,8 @@ struct MDPSparseModelCheckingHelperReturnType {
 
     // A scheduler, if it was computed.
     std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
+
+    storm::solver::SolutionBounds<ValuesType> solutionBounds;
 };
 }  // namespace helper