Implemented quantiles for DTMCs.

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -7,9 +7,11 @@
 
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 
 #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
 #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
+#include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
 
 #include "storm/logic/FragmentSpecification.h"
 
@@ -31,7 +33,13 @@ namespace storm {
         template<typename SparseDtmcModelType>
         bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true));
+            if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true))) {
+                return true;
+            } else if (formula.isInFragment(storm::logic::quantiles())) {
+                if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
+                return true;
+            }
+            return false;
         }
         
         template<typename SparseDtmcModelType>
@@ -184,6 +192,28 @@ namespace storm {
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
         
+        
+        template<>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Quantiles for parametric models are not implemented.");
+        }
+        
+        template<typename SparseDtmcModelType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for the initial states of a model.");
+            STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, "Quantiles not supported on models with multiple initial states.");
+            uint64_t initialState = *this->getModel().getInitialStates().begin();
+
+            helper::rewardbounded::QuantileHelper<SparseDtmcModelType> qHelper(this->getModel(), checkTask.getFormula());
+            auto res = qHelper.computeQuantile(env);
+            
+            if (res.size() == 1 && res.front().size() == 1) {
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initialState, std::move(res.front().front())));
+            } else {
+                return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<ValueType>(initialState, std::move(res)));
+            }
+        }
+        
         template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>;
 
 #ifdef STORM_HAVE_CARL

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -34,6 +34,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
+            virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) override;
         };
         
     } // namespace modelchecker

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -228,7 +228,7 @@ namespace storm {
         
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) {
-            STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for models with a single initial states.");
+            STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Computing quantiles is only supported for the initial states of a model.");
             STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidOperationException, "Quantiles not supported on models with multiple initial states.");
             uint64_t initialState = *this->getModel().getInitialStates().begin();
 

src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp

@@ -8,6 +8,7 @@
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 
 #include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Dtmc.h"
 #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/storage/expressions/Expressions.h"
@@ -360,7 +361,12 @@ namespace storm {
                     auto lowerBound = rewardUnfolding.getLowerObjectiveBound();
                     auto upperBound = rewardUnfolding.getUpperObjectiveBound();
                     std::vector<ValueType> x, b;
-                    std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver;
+                    std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> minMaxSolver; // Needed for MDP
+                    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linEqSolver; // Needed for DTMC
+                    if (!model.isNondeterministicModel()) {
+                        rewardUnfolding.setEquationSystemFormatForEpochModel(storm::solver::GeneralLinearEquationSolverFactory<ValueType>().getEquationProblemFormat(env));
+                    }
+
                     swExploration.start();
                     bool progress = true;
                     for (CostLimit candidateCostLimitSum(0); progress; ++candidateCostLimitSum.get()) {
@@ -395,7 +401,11 @@ namespace storm {
                                     ++numCheckedEpochs;
                                     swEpochAnalysis.start();
                                     auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
-                                    rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env,boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound));
+                                    if (model.isNondeterministicModel()) {
+                                        rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env, boundedUntilOperator.getOptimalityType(), x, b, minMaxSolver, lowerBound, upperBound));
+                                    } else {
+                                        rewardUnfolding.setSolutionForCurrentEpoch(epochModel.analyzeSingleObjective(env, x, b, linEqSolver, lowerBound, upperBound));
+                                    }
                                     swEpochAnalysis.stop();
 
                                     CostLimits epochAsCostLimits;
@@ -431,6 +441,8 @@ namespace storm {
 
                 template class QuantileHelper<storm::models::sparse::Mdp<double>>;
                 template class QuantileHelper<storm::models::sparse::Mdp<storm::RationalNumber>>;
+                template class QuantileHelper<storm::models::sparse::Dtmc<double>>;
+                template class QuantileHelper<storm::models::sparse::Dtmc<storm::RationalNumber>>;
 
             }
         }