MDP model checker works again.

Former-commit-id: 2c24da6192

src/logic/AtomicExpressionFormula.cpp

@@ -10,10 +10,18 @@ namespace storm {
             return true;
         }
         
-        bool AtomicExpressionFormula::isPropositionalFormula() const {
+        bool AtomicExpressionFormula::isPctlStateFormula() const {
+            return true;
+        }
+                
+        bool AtomicExpressionFormula::isLtlFormula() const {
             return true;
         }
         
+        bool AtomicExpressionFormula::isPropositionalFormula() const {
+            return true;
+        }
+                
         storm::expressions::Expression const& AtomicExpressionFormula::getExpression() const {
             return expression;
         }

src/logic/AtomicExpressionFormula.h

@@ -15,8 +15,11 @@ namespace storm {
             }
             
             virtual bool isAtomicExpressionFormula() const override;
+            
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isLtlFormula() const override;
             virtual bool isPropositionalFormula() const override;
-
+            
             storm::expressions::Expression const& getExpression() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/AtomicLabelFormula.cpp

@@ -10,6 +10,14 @@ namespace storm {
             return true;
         }
         
+        bool AtomicLabelFormula::isPctlStateFormula() const {
+            return true;
+        }
+    
+        bool AtomicLabelFormula::isLtlFormula() const {
+            return true;
+        }
+        
         bool AtomicLabelFormula::isPropositionalFormula() const {
             return true;
         }

src/logic/AtomicLabelFormula.h

@@ -16,8 +16,11 @@ namespace storm {
             }
             
             virtual bool isAtomicLabelFormula() const override;
-            virtual bool isPropositionalFormula() const override;
 
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool isPropositionalFormula() const override;
+            
             std::string const& getLabel() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/BinaryBooleanStateFormula.h

@@ -16,8 +16,9 @@ namespace storm {
             };
             
             virtual bool isBinaryBooleanStateFormula() const override;
+            
             virtual bool isPropositionalFormula() const override;
-
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/BinaryPathFormula.cpp

@@ -10,6 +10,22 @@ namespace storm {
             return true;
         }
         
+        bool BinaryPathFormula::isPctlPathFormula() const {
+            return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
+        }
+        
+        bool BinaryPathFormula::isLtlFormula() const {
+            return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
+        }
+        
+        bool BinaryPathFormula::hasProbabilityOperator() const {
+            return this->getLeftSubformula().hasProbabilityOperator() || this->getRightSubformula().hasProbabilityOperator();
+        }
+        
+        bool BinaryPathFormula::hasNestedProbabilityOperators() const {
+            return this->getLeftSubformula().Formula::hasNestedProbabilityOperators() || this->getRightSubformula().hasNestedProbabilityOperators();
+        }
+        
         Formula const& BinaryPathFormula::getLeftSubformula() const {
             return *leftSubformula;
         }

src/logic/BinaryPathFormula.h

@@ -17,6 +17,11 @@ namespace storm {
             
             virtual bool isBinaryPathFormula() const override;
             
+            virtual bool isPctlPathFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             

src/logic/BinaryStateFormula.cpp

@@ -9,6 +9,23 @@ namespace storm {
         bool BinaryStateFormula::isBinaryStateFormula() const {
             return true;
         }
+        
+        bool BinaryStateFormula::isPctlStateFormula() const {
+            return this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
+        }
+        
+        bool BinaryStateFormula::isLtlFormula() const {
+            return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
+        }
+        
+        bool BinaryStateFormula::hasProbabilityOperator() const {
+            return this->getLeftSubformula().hasProbabilityOperator() || this->getRightSubformula().hasProbabilityOperator();
+        }
+        
+        bool BinaryStateFormula::hasNestedProbabilityOperators() const {
+            return this->getLeftSubformula().hasNestedProbabilityOperators() || this->getRightSubformula().hasNestedProbabilityOperators();
+        }
+        
         Formula const& BinaryStateFormula::getLeftSubformula() const {
             return *leftSubformula;
         }

src/logic/BinaryStateFormula.h

@@ -15,6 +15,11 @@ namespace storm {
             
             virtual bool isBinaryStateFormula() const override;
 
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;
             

src/logic/BooleanLiteralFormula.cpp

@@ -14,6 +14,14 @@ namespace storm {
             return !value;
         }
         
+        bool BooleanLiteralFormula::isPctlStateFormula() const {
+            return true;
+        }
+        
+        bool BooleanLiteralFormula::isLtlFormula() const {
+            return true;
+        }
+        
         bool BooleanLiteralFormula::isPropositionalFormula() const {
             return true;
         }

src/logic/BooleanLiteralFormula.h

@@ -16,8 +16,11 @@ namespace storm {
             virtual bool isBooleanLiteralFormula() const override;
             virtual bool isTrueFormula() const override;
             virtual bool isFalseFormula() const override;
-            virtual bool isPropositionalFormula() const override;
 
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool isPropositionalFormula() const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/BoundedUntilFormula.cpp

@@ -22,6 +22,14 @@ namespace storm {
             return bounds.which() == 0;
         }
         
+        bool BoundedUntilFormula::isPctlPathFormula() const {
+            return this->isIntegerUpperBounded() && this->getLeftSubformula().isPctlStateFormula() && this->getRightSubformula().isPctlStateFormula();
+        }
+        
+        bool BoundedUntilFormula::isCslPathFormula() const {
+            return this->getLeftSubformula().isCslStateFormula() && this->getRightSubformula().isCslStateFormula();
+        }
+        
         std::pair<double, double> const& BoundedUntilFormula::getIntervalBounds() const {
             return boost::get<std::pair<double, double>>(bounds);
         }

src/logic/BoundedUntilFormula.h

@@ -20,6 +20,9 @@ namespace storm {
             std::pair<double, double> const& getIntervalBounds() const;
             uint_fast64_t getUpperBound() const;
             
+            virtual bool isPctlPathFormula() const override;
+            virtual bool isCslPathFormula() const override;
+
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         private:

src/logic/Formula.cpp

@@ -114,14 +114,34 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isCslPathFormula() const {
+            return this->isPctlPathFormula();
+        }
+        
+        bool Formula::isCslStateFormula() const {
+            return this->isPctlStateFormula();
+        }
+        
         bool Formula::isPltlFormula() const {
             return false;
         }
         
+        bool Formula::isLtlFormula() const {
+            return false;
+        }
+        
         bool Formula::isPropositionalFormula() const {
             return false;
         }
         
+        bool Formula::hasProbabilityOperator() const {
+            return false;
+        }
+        
+        bool Formula::hasNestedProbabilityOperators() const {
+            return false;
+        }
+        
         std::shared_ptr<Formula const> Formula::getTrueFormula() {
             return std::shared_ptr<Formula const>(new BooleanLiteralFormula(true));
         }

src/logic/Formula.h

@@ -76,8 +76,13 @@ namespace storm {
 
             virtual bool isPctlPathFormula() const;
             virtual bool isPctlStateFormula() const;
+            virtual bool isCslPathFormula() const;
+            virtual bool isCslStateFormula() const;
             virtual bool isPltlFormula() const;
+            virtual bool isLtlFormula() const;
             virtual bool isPropositionalFormula() const;
+            virtual bool hasProbabilityOperator() const;
+            virtual bool hasNestedProbabilityOperators() const;
             
             static std::shared_ptr<Formula const> getTrueFormula();
             

src/logic/ProbabilityOperatorFormula.cpp

@@ -22,6 +22,22 @@ namespace storm {
             return true;
         }
         
+        bool ProbabilityOperatorFormula::isPctlStateFormula() const {
+            return this->getSubformula().isPctlPathFormula();
+        }
+        
+        bool ProbabilityOperatorFormula::isPltlFormula() const {
+            return this->getSubformula().isLtlFormula();
+        }
+        
+        bool ProbabilityOperatorFormula::hasProbabilityOperator() const {
+            return true;
+        }
+        
+        bool ProbabilityOperatorFormula::hasNestedProbabilityOperators() const {
+            return this->getSubformula().hasProbabilityOperator();
+        }
+        
         ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }

src/logic/ProbabilityOperatorFormula.h

@@ -17,6 +17,11 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isPltlFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             virtual bool isProbabilityOperatorFormula() const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;

src/logic/RewardOperatorFormula.cpp

@@ -22,6 +22,10 @@ namespace storm {
             return true;
         }
         
+        bool RewardOperatorFormula::isPctlStateFormula() const {
+            return this->getSubformula().isRewardPathFormula();
+        }
+        
         RewardOperatorFormula::RewardOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }

src/logic/RewardOperatorFormula.h

@@ -19,6 +19,8 @@ namespace storm {
             
             virtual bool isRewardOperatorFormula() const override;
             
+            virtual bool isPctlStateFormula() const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }

src/logic/SteadyStateOperatorFormula.cpp

@@ -22,6 +22,18 @@ namespace storm {
             return true;
         }
         
+        bool SteadyStateOperatorFormula::isPctlStateFormula() const {
+            return this->getSubformula().isPctlStateFormula();
+        }
+        
+        bool SteadyStateOperatorFormula::hasProbabilityOperator() const {
+            return this->getSubformula().hasProbabilityOperator();
+        }
+        
+        bool SteadyStateOperatorFormula::hasNestedProbabilityOperators() const {
+            return this->getSubformula().hasNestedProbabilityOperators();
+        }
+        
         SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }

src/logic/SteadyStateOperatorFormula.h

@@ -19,6 +19,10 @@ namespace storm {
             
             virtual bool isSteadyStateOperatorFormula() const override;
             
+            virtual bool isPctlStateFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }

src/logic/UnaryPathFormula.cpp

@@ -9,7 +9,23 @@ namespace storm {
         bool UnaryPathFormula::isUnaryPathFormula() const {
             return true;
         }
-                
+        bool UnaryPathFormula::isPctlPathFormula() const {
+            return this->getSubformula().isPctlStateFormula();
+        }
+        
+        bool UnaryPathFormula::isLtlFormula() const {
+            return this->getSubformula().isLtlFormula();
+        }
+        
+        bool UnaryPathFormula::hasProbabilityOperator() const {
+            return this->getSubformula().hasProbabilityOperator();
+        }
+        
+        bool UnaryPathFormula::hasNestedProbabilityOperators() const {
+            return this->getSubformula().hasNestedProbabilityOperators();
+        }
+        
         Formula const& UnaryPathFormula::getSubformula() const {
             return *subformula;
         }

src/logic/UnaryPathFormula.h

@@ -17,6 +17,11 @@ namespace storm {
 
             virtual bool isUnaryPathFormula() const override;
             
+            virtual bool isPctlPathFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             Formula const& getSubformula() const;
             
         private:

src/logic/UnaryStateFormula.cpp

@@ -14,6 +14,22 @@ namespace storm {
             return this->getSubformula().isPropositionalFormula();
         }
         
+        bool UnaryStateFormula::isPctlStateFormula() const {
+            return this->getSubformula().isPctlStateFormula();
+        }
+        
+        bool UnaryStateFormula::isLtlFormula() const {
+            return this->getSubformula().isLtlFormula();
+        }
+        
+        bool UnaryStateFormula::hasProbabilityOperator() const {
+            return getSubformula().hasProbabilityOperator();
+        }
+        
+        bool UnaryStateFormula::hasNestedProbabilityOperators() const {
+            return getSubformula().hasNestedProbabilityOperators();
+        }
+        
         Formula const& UnaryStateFormula::getSubformula() const {
             return *subformula;
         }

src/logic/UnaryStateFormula.h

@@ -14,8 +14,13 @@ namespace storm {
             }
             
             virtual bool isUnaryStateFormula() const override;
-            virtual bool isPropositionalFormula() const override;
 
+            virtual bool isPropositionalFormula() const override;
+            virtual bool isPctlStateFormula() const override;
+            virtual bool isLtlFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
             Formula const& getSubformula() const;
             
         private:

src/modelchecker/AbstractModelChecker.cpp

@@ -7,7 +7,7 @@
 namespace storm {
     namespace modelchecker {
         std::unique_ptr<CheckResult> AbstractModelChecker::check(storm::logic::Formula const& formula) {
-            STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check this formula.");
+            STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
             if (formula.isStateFormula()) {
                 return this->checkStateFormula(formula.asStateFormula());
             } else if (formula.isPathFormula()) {
@@ -20,15 +20,15 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeProbabilities(storm::logic::PathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             if (pathFormula.isBoundedUntilFormula()) {
-                return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula());
+                return this->computeBoundedUntilProbabilities(pathFormula.asBoundedUntilFormula(), qualitative, optimalityType);
             } else if (pathFormula.isConditionalPathFormula()) {
-                return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula());
+                return this->computeConditionalProbabilities(pathFormula.asConditionalPathFormula(), qualitative, optimalityType);
             } else if (pathFormula.isEventuallyFormula()) {
-                return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula());
+                return this->computeEventuallyProbabilities(pathFormula.asEventuallyFormula(), qualitative, optimalityType);
             } else if (pathFormula.isGloballyFormula()) {
-                return this->computeGloballyProbabilities(pathFormula.asGloballyFormula());
+                return this->computeGloballyProbabilities(pathFormula.asGloballyFormula(), qualitative, optimalityType);
             } else if (pathFormula.isUntilFormula()) {
-                return this->computeUntilProbabilities(pathFormula.asUntilFormula());
+                return this->computeUntilProbabilities(pathFormula.asUntilFormula(), qualitative, optimalityType);
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
         }
@@ -43,7 +43,7 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeEventuallyProbabilities(storm::logic::EventuallyFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             storm::logic::UntilFormula newFormula(storm::logic::Formula::getTrueFormula(), pathFormula.getSubformula().asSharedPointer());
-            return this->check(newFormula);
+            return this->computeUntilProbabilities(newFormula, qualitative, optimalityType);
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
@@ -60,11 +60,11 @@ namespace storm {
         
         std::unique_ptr<CheckResult> AbstractModelChecker::computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             if (rewardPathFormula.isCumulativeRewardFormula()) {
-                return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula());
+                return this->computeCumulativeRewards(rewardPathFormula.asCumulativeRewardFormula(), qualitative, optimalityType);
             } else if (rewardPathFormula.isInstantaneousRewardFormula()) {
-                return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula());
+                return this->computeInstantaneousRewards(rewardPathFormula.asInstantaneousRewardFormula(), qualitative, optimalityType);
             } else if (rewardPathFormula.isReachabilityRewardFormula()) {
-                return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula());
+                return this->computeReachabilityRewards(rewardPathFormula.asReachabilityRewardFormula(), qualitative, optimalityType);
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
         }
@@ -134,15 +134,23 @@ namespace storm {
                     qualitative = true;
                 }
             }
+            
+            std::unique_ptr<CheckResult> result;
             if (stateFormula.hasOptimalityType()) {
-                return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType());
+                result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative, stateFormula.getOptimalityType());
+            } else {
+                result = this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative);
+            }
+            
+            if (stateFormula.hasBound()) {
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
-                return this->computeProbabilities(stateFormula.getSubformula().asPathFormula(), qualitative);
+                return result;
             }
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) {
-            STORM_LOG_THROW(stateFormula.getSubformula().isRewardOperatorFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+            STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
             // If the probability bound is 0, is suffices to do qualitative model checking.
             bool qualitative = false;

src/modelchecker/CheckResult.cpp

@@ -20,6 +20,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result.");
         }
         
+        std::unique_ptr<CheckResult> CheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result.");
+        }
+        
         bool CheckResult::isExplicit() const {
             return false;
         }

src/modelchecker/CheckResult.h

@@ -2,6 +2,9 @@
 #define STORM_MODELCHECKER_CHECKRESULT_H_
 
 #include <iostream>
+#include <memory>
+
+#include "src/logic/ComparisonType.h"
 
 namespace storm {
     namespace modelchecker {
@@ -18,6 +21,8 @@ namespace storm {
             virtual CheckResult& operator|=(CheckResult const& other);
             virtual void complement();
             
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const;
+            
             friend std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);
 
             virtual bool isExplicit() const;

src/modelchecker/ExplicitQuantitativeCheckResult.cpp

@@ -1,5 +1,7 @@
 #include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
 
+#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
+#include "src/storage/BitVector.h"
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
 
@@ -22,6 +24,42 @@ namespace storm {
             return out;
         }
         
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+            storm::storage::BitVector result(values.size());
+            switch (comparisonType) {
+                case logic::Less:
+                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
+                        if (result[index] < bound) {
+                            result.set(index);
+                        }
+                    }
+                    break;
+                case logic::LessEqual:
+                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
+                        if (result[index] <= bound) {
+                            result.set(index);
+                        }
+                    }
+                    break;
+                case logic::Greater:
+                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
+                        if (result[index] > bound) {
+                            result.set(index);
+                        }
+                    }
+                    break;
+                case logic::GreaterEqual:
+                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
+                        if (result[index] >= bound) {
+                            result.set(index);
+                        }
+                    }
+                    break;
+            }
+            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
+        }
+        
         template<typename ValueType>
         ValueType ExplicitQuantitativeCheckResult<ValueType>::operator[](uint_fast64_t index) const {
             return values[index];

src/modelchecker/ExplicitQuantitativeCheckResult.h

@@ -36,6 +36,8 @@ namespace storm {
             ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default;
 #endif
             
+            virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
+            
             ValueType operator[](uint_fast64_t index) const;
             
             virtual bool isExplicit() const override;

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -13,106 +13,108 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace prctl {
+        template<typename ValueType>
-            template<typename ValueType>
+        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver) : model(model), linearEquationSolver(std::move(linearEquationSolver)) {
-            SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver) : model(model), linearEquationSolver(std::move(linearEquationSolver)) {
+            // Intentionally left empty.
-                // Intentionally left empty.
+        }
-            }
+        template<typename ValueType>
-            
+        SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<ValueType>()) {
-            template<typename ValueType>
+            // Intentionally left empty.
-            SparseDtmcPrctlModelChecker<ValueType>::SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model), linearEquationSolver(storm::utility::solver::getLinearEquationSolver<ValueType>()) {
+        }
-                // Intentionally left empty.
+        template<typename ValueType>
-            }
+        bool SparseDtmcPrctlModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula();
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) {
+            std::vector<ValueType> result(model.getNumberOfStates(), storm::utility::zero<ValueType>());
             
-            template<typename ValueType>
+            // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
-            bool SparseDtmcPrctlModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
-                return formula.isPctlStateFormula() || formula.isPctlPathFormula();
+            STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
-            }
             
-            template<typename ValueType>
+            if (!statesWithProbabilityGreater0.empty()) {
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) {
+                // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                std::vector<ValueType> result(model.getNumberOfStates());
+                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
                 
-                // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
+                // Compute the new set of target states in the reduced system.
-                storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+                storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
-                STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.")
-
-                if (!statesWithProbabilityGreater0.empty()) {
-                    // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                    storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, true);
-                    
-                    // Compute the new set of target states in the reduced system.
-                    storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
-                    
-                    // Make all rows absorbing that satisfy the second sub-formula.
-                    submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
-                    
-                    // Create the vector with which to multiply.
-                    std::vector<ValueType> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
-                    storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one<ValueType>());
-                    
-                    // Perform the matrix vector multiplication as often as required by the formula bound.
-                    STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                    this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound);
-                    
-                    // Set the values of the resulting vector accordingly.
-                    storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
-                }
-                storm::utility::vector::setVectorValues<ValueType>(result, ~statesWithProbabilityGreater0, storm::utility::zero<ValueType>());
                 
-                return result;
+                // Make all rows absorbing that satisfy the second sub-formula.
-            }
+                submatrix.makeRowsAbsorbing(rightStatesInReducedSystem);
-            
+                // Create the vector with which to multiply.
-            template<typename ValueType>
+                std::vector<ValueType> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+                storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one<ValueType>());
-                std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
-                std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-                ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-                ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound())));
-            }
-            
-            template<typename ValueType>
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates) {
-                // Create the vector with which to multiply and initialize it correctly.
-                std::vector<ValueType> result(model.getNumberOfStates());
-                storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
                 
-                // Perform one single matrix-vector multiplication.
+                // Perform the matrix vector multiplication as often as required by the formula bound.
                 STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result);
+                this->linearEquationSolver->performMatrixVectorMultiplication(submatrix, subresult, nullptr, stepBound);
-                return result;
+                // Set the values of the resulting vector accordingly.
+                storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
+                storm::utility::vector::setVectorValues<ValueType>(result, ~statesWithProbabilityGreater0, storm::utility::zero<ValueType>());
             }
             
-            template<typename ValueType>
+            return result;
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+        }
-                std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
+        template<typename ValueType>
-                ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(subResult.getTruthValues())));
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
-            }
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
+            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
+            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound())));
             
-            template<typename ValueType>
+            return result;
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
+        }
-                // We need to identify the states which have to be taken out of the matrix, i.e.
+        template<typename ValueType>
-                // all states that have probability 0 and 1 of satisfying the until-formula.
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates) {
-                std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates);
+            // Create the vector with which to multiply and initialize it correctly.
-                storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
+            std::vector<ValueType> result(model.getNumberOfStates());
-                storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
+            storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
-                
+            // Perform one single matrix-vector multiplication.
-                // Perform some logging.
+            STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result);
-                STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+            return result;
-                STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+        }
-                STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+        template<typename ValueType>
-                
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-                // Create resulting vector.
+            std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
-                std::vector<ValueType> result(model.getNumberOfStates());
+            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-                
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(subResult.getTruthValues())));
-                // Check whether we need to compute exact probabilities for some states.
+        }
-                if (qualitative) {
+        template<typename ValueType>
-                    // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
-                    storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5));
+            // We need to identify the states which have to be taken out of the matrix, i.e.
-                } else {
+            // all states that have probability 0 and 1 of satisfying the until-formula.
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates);
+            storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
+            storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
+            
+            // Perform some logging.
+            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+            STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+            STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+            
+            // Create resulting vector.
+            std::vector<ValueType> result(model.getNumberOfStates());
+            
+            // Check whether we need to compute exact probabilities for some states.
+            if (qualitative) {
+                // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5));
+            } else {
+                if (!maybeStates.empty()) {
                     // In this case we have have to compute the probabilities.
                     
                     // We can eliminate the rows and columns from the original transition probability matrix.
@@ -138,177 +140,177 @@ namespace storm {
                     // Set values of resulting vector according to result.
                     storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
                 }
-                
-                // Set values of resulting vector that are known exactly.
-                storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
-                storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
-                
-                return result;
             }
             
-            template<typename ValueType>
+            // Set values of resulting vector that are known exactly.
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
-                std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+            storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
-                std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-                ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-                ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), qualitative)));
-            }
             
-            template<typename ValueType>
+            return result;
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(uint_fast64_t stepBound) const {
+        }
-                // Only compute the result if the model has at least one reward model.
+        template<typename ValueType>
-                STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
-                // Compute the reward vector to add in each step based on the available reward models.
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-                std::vector<ValueType> totalRewardVector;
+            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-                if (model.hasTransitionRewards()) {
+            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-                    totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), qualitative)));
-                    if (model.hasStateRewards()) {
+        }
-                        storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
+        template<typename ValueType>
-                    }
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(uint_fast64_t stepBound) const {
-                } else {
+            // Only compute the result if the model has at least one reward model.
-                    totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
+            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-                }
+            // Compute the reward vector to add in each step based on the available reward models.
-                
+            std::vector<ValueType> totalRewardVector;
-                // Initialize result to either the state rewards of the model or the null vector.
+            if (model.hasTransitionRewards()) {
-                std::vector<ValueType> result;
+                totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
                 if (model.hasStateRewards()) {
-                    result = std::vector<ValueType>(model.getStateRewardVector());
+                    storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
-                } else {
-                    result.resize(model.getNumberOfStates());
                 }
-                
+            } else {
-                // Perform the matrix vector multiplication as often as required by the formula bound.
+                totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
-                STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, &totalRewardVector, stepBound);
-                
-                return result;
             }
             
-            template<typename ValueType>
+            // Initialize result to either the state rewards of the model or the null vector.
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            std::vector<ValueType> result;
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getStepBound())));
+            if (model.hasStateRewards()) {
+                result = std::vector<ValueType>(model.getStateRewardVector());
+            } else {
+                result.resize(model.getNumberOfStates());
             }
             
-            template<typename ValueType>
+            // Perform the matrix vector multiplication as often as required by the formula bound.
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const {
+            STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                // Only compute the result if the model has a state-based reward model.
+            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, &totalRewardVector, stepBound);
-                STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
-                
-                // Initialize result to state rewards of the model.
-                std::vector<ValueType> result(model.getStateRewardVector());
-                
-                // Perform the matrix vector multiplication as often as required by the formula bound.
-                STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, nullptr, stepCount);
-
-                return result;
-            }
             
-            template<typename ValueType>
+            return result;
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+        }
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getStepCount())));
+        template<typename ValueType>
-            }
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getStepBound())));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const {
+            // Only compute the result if the model has a state-based reward model.
+            STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Initialize result to state rewards of the model.
+            std::vector<ValueType> result(model.getStateRewardVector());
+            
+            // Perform the matrix vector multiplication as often as required by the formula bound.
+            STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
+            this->linearEquationSolver->performMatrixVectorMultiplication(model.getTransitionMatrix(), result, nullptr, stepCount);
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getStepCount())));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const {
+            // Only compute the result if the model has at least one reward model.
+            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Determine which states have a reward of infinity by definition.
+            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, targetStates);
+            infinityStates.complement();
+            storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
+            STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
+            STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
+            STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+            
+            // Create resulting vector.
+            std::vector<ValueType> result(model.getNumberOfStates());
             
-            template<typename ValueType>
+            // Check whether we need to compute exact rewards for some states.
-            std::vector<ValueType> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const {
+            if (qualitative) {
-                // Only compute the result if the model has at least one reward model.
+                // Set the values for all maybe-states to 1 to indicate that their reward values
-                STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+                // are neither 0 nor infinity.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
+            } else {
+                // In this case we have to compute the reward values for the remaining states.
+                // We can eliminate the rows and columns from the original transition probability matrix.
+                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
                 
-                // Determine which states have a reward of infinity by definition.
+                // Converting the matrix from the fixpoint notation to the form needed for the equation
-                storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+                // system. That is, we go from x = A*x + b to (I-A)x = b.
-                storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, targetStates);
+                submatrix.convertToEquationSystem();
-                infinityStates.complement();
-                storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
-                STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
-                STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
-                STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
                 
-                // Create resulting vector.
+                // Initialize the x vector with 1 for each element. This is the initial guess for
-                std::vector<ValueType> result(model.getNumberOfStates());
+                // the iterative solvers.
+                std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>());
                 
-                // Check whether we need to compute exact rewards for some states.
+                // Prepare the right-hand side of the equation system.
-                if (qualitative) {
+                std::vector<ValueType> b(submatrix.getRowCount());
-                    // Set the values for all maybe-states to 1 to indicate that their reward values
+                if (model.hasTransitionRewards()) {
-                    // are neither 0 nor infinity.
+                    // If a transition-based reward model is available, we initialize the right-hand
-                    storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
+                    // side to the vector resulting from summing the rows of the pointwise product
-                } else {
+                    // of the transition probability matrix and the transition reward matrix.
-                    // In this case we have to compute the reward values for the remaining states.
+                    std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
-                    // We can eliminate the rows and columns from the original transition probability matrix.
+                    storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
-                    storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, true);
-
-                    // Converting the matrix from the fixpoint notation to the form needed for the equation
-                    // system. That is, we go from x = A*x + b to (I-A)x = b.
-                    submatrix.convertToEquationSystem();
-                    
-                    // Initialize the x vector with 1 for each element. This is the initial guess for
-                    // the iterative solvers.
-                    std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>());
                     
-                    // Prepare the right-hand side of the equation system.
+                    if (model.hasStateRewards()) {
-                    std::vector<ValueType> b(submatrix.getRowCount());
+                        // If a state-based reward model is also available, we need to add this vector
-                    if (model.hasTransitionRewards()) {
+                        // as well. As the state reward vector contains entries not just for the states
-                        // If a transition-based reward model is available, we initialize the right-hand
+                        // that we still consider (i.e. maybeStates), we need to extract these values
-                        // side to the vector resulting from summing the rows of the pointwise product
-                        // of the transition probability matrix and the transition reward matrix.
-                        std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
-                        storm::utility::vector::selectVectorValues(b, maybeStates, pointwiseProductRowSumVector);
-                        
-                        if (model.hasStateRewards()) {
-                            // If a state-based reward model is also available, we need to add this vector
-                            // as well. As the state reward vector contains entries not just for the states
-                            // that we still consider (i.e. maybeStates), we need to extract these values
-                            // first.
-                            std::vector<ValueType> subStateRewards(b.size());
-                            storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector());
-                            storm::utility::vector::addVectorsInPlace(b, subStateRewards);
-                        }
-                    } else {
-                        // If only a state-based reward model is  available, we take this vector as the
-                        // right-hand side. As the state reward vector contains entries not just for the
-                        // states that we still consider (i.e. maybeStates), we need to extract these values
                         // first.
-                        storm::utility::vector::selectVectorValues(b, maybeStates, model.getStateRewardVector());
+                        std::vector<ValueType> subStateRewards(b.size());
+                        storm::utility::vector::selectVectorValues(subStateRewards, maybeStates, model.getStateRewardVector());
+                        storm::utility::vector::addVectorsInPlace(b, subStateRewards);
                     }
-                    
+                } else {
-                    // Now solve the resulting equation system.
+                    // If only a state-based reward model is  available, we take this vector as the
-                    STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
+                    // right-hand side. As the state reward vector contains entries not just for the
-                    this->linearEquationSolver->solveEquationSystem(submatrix, x, b);
+                    // states that we still consider (i.e. maybeStates), we need to extract these values
-                    
+                    // first.
-                    // Set values of resulting vector according to result.
+                    storm::utility::vector::selectVectorValues(b, maybeStates, model.getStateRewardVector());
-                    storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
                 }
                 
-                // Set values of resulting vector that are known exactly.
+                // Now solve the resulting equation system.
-                storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero<ValueType>());
+                STORM_LOG_THROW(linearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
-                storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
+                this->linearEquationSolver->solveEquationSystem(submatrix, x, b);
                 
-                return result;
+                // Set values of resulting vector according to result.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
             }
             
-            template<typename ValueType>
+            // Set values of resulting vector that are known exactly.
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero<ValueType>());
-                std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
-                ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(subResult.getTruthValues(), qualitative)));
-            }
-            
-            template<typename ValueType>
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
-                if (stateFormula.isTrueFormula()) {
-                    return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
-                } else {
-                    return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
-                }
-            }
             
-            template<typename ValueType>
+            return result;
-            std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+        }
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(subResult.getTruthValues(), qualitative)));
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+            if (stateFormula.isTrueFormula()) {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
+            } else {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
             }
-
-            template class SparseDtmcPrctlModelChecker<double>;
         }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        }
+        
+        template class SparseDtmcPrctlModelChecker<double>;
     }
 }

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h

@@ -1,5 +1,5 @@
-#ifndef STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
 
 #include "src/modelchecker/AbstractModelChecker.h"
 #include "src/models/Dtmc.h"
@@ -8,43 +8,41 @@
 
 namespace storm {
     namespace modelchecker {
-        namespace prctl {
+        template<class ValueType>
+        class SparseDtmcPrctlModelChecker : public AbstractModelChecker {
+        public:
+            explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model);
+            explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver);
             
-            template<class ValueType>
+            // The implemented methods of the AbstractModelChecker interface.
-            class SparseDtmcPrctlModelChecker : public AbstractModelChecker {
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
-            public:
+            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model);
+            virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<ValueType> const& model, std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>>&& linearEquationSolver);
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                // The implemented methods of the AbstractModelChecker interface.
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                virtual bool canHandle(storm::logic::Formula const& formula) const override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
-                virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
-                virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            // The methods that perform the actual checking.
-                virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound);
-                virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            std::vector<ValueType> computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates);
-                virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
-                virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
+            std::vector<ValueType> computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const;
-                virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            std::vector<ValueType> computeCumulativeRewardsHelper(uint_fast64_t stepBound) const;
-                
+            std::vector<ValueType> computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const;
-                // The methods that perform the actual checking.
+        private:
-                std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound);
+            // The model this model checker is supposed to analyze.
-                std::vector<ValueType> computeNextProbabilitiesHelper(storm::storage::BitVector const& nextStates);
+            storm::models::Dtmc<ValueType> const& model;
-                std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
-                std::vector<ValueType> computeInstantaneousRewardsHelper(uint_fast64_t stepCount) const;
-                std::vector<ValueType> computeCumulativeRewardsHelper(uint_fast64_t stepBound) const;
-                std::vector<ValueType> computeReachabilityRewardsHelper(storm::storage::BitVector const& targetStates, bool qualitative) const;
-
-            private:
-                // The model this model checker is supposed to analyze.
-                storm::models::Dtmc<ValueType> const& model;
-
-                // An object that is used for solving linear equations and performing matrix-vector multiplication.
-                std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linearEquationSolver;
-            };
             
-        } // namespace prctl
+            // An object that is used for solving linear equations and performing matrix-vector multiplication.
+            std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> linearEquationSolver;
+        };
+        
     } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ */

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -0,0 +1,327 @@
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+
+#include <vector>
+
+#include "src/utility/ConstantsComparator.h"
+#include "src/utility/macros.h"
+#include "src/utility/vector.h"
+#include "src/utility/graph.h"
+
+#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model) : model(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        SparseMdpPrctlModelChecker<ValueType>::SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver) : model(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        bool SparseMdpPrctlModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            return formula.isPctlStateFormula() || formula.isPctlPathFormula() || formula.isRewardPathFormula();
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound) {
+            std::vector<ValueType> result(model.getNumberOfStates(), storm::utility::zero<ValueType>());
+            
+            // Determine the states that have 0 probability of reaching the target states.
+            storm::storage::BitVector statesWithProbabilityGreater0;
+            if (minimize) {
+                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+            } else {
+                statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates, true, stepBound);
+            }
+            STORM_LOG_INFO("Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states.");
+            
+            if (!statesWithProbabilityGreater0.empty()) {
+                // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
+                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false);
+                
+                // Compute the new set of target states in the reduced system.
+                storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
+                
+                // Make all rows absorbing that satisfy the second sub-formula.
+                submatrix.makeRowGroupsAbsorbing(rightStatesInReducedSystem);
+                
+                // Create the vector with which to multiply.
+                std::vector<ValueType> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
+                storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::one<ValueType>());
+            
+                STORM_LOG_THROW(nondeterministicLinearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
+                this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, submatrix, subresult, nullptr, stepBound);
+                
+                // Set the values of the resulting vector accordingly.
+                storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
+                storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::zero<ValueType>());
+            }
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
+            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
+            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound())));
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeNextProbabilitiesHelper(bool minimize, storm::storage::BitVector const& nextStates) {
+            // Create the vector with which to multiply and initialize it correctly.
+            std::vector<ValueType> result(model.getNumberOfStates());
+            storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>());
+            
+            STORM_LOG_THROW(nondeterministicLinearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid equation solver available.");
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result);
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
+            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValues())));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver, bool qualitative) {
+            size_t numberOfStates = phiStates.size();
+            
+            // We need to identify the states which have to be taken out of the matrix, i.e.
+            // all states that have probability 0 and 1 of satisfying the until-formula.
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
+            if (minimize) {
+                statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
+            } else {
+                statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
+            }
+            storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
+            storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
+            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+            LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+            LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+            
+            // Create resulting vector.
+            std::vector<ValueType> result(numberOfStates);
+            
+            // Check whether we need to compute exact probabilities for some states.
+            if (qualitative) {
+                // Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5));
+            } else {
+                if (!maybeStates.empty()) {
+                    // In this case we have have to compute the probabilities.
+
+                    // First, we can eliminate the rows and columns from the original transition probability matrix for states
+                    // whose probabilities are already known.
+                    storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
+                    
+                    // Prepare the right-hand side of the equation system. For entry i this corresponds to
+                    // the accumulated probability of going from state i to some 'yes' state.
+                    std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1);
+                    
+                    // Create vector for results for maybe states.
+                    std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
+                    
+                    // Solve the corresponding system of equations.
+                    nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
+                    
+                    // Set values of resulting vector according to result.
+                    storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+                }
+            }
+            
+            // Set values of resulting vector that are known exactly.
+            storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>());
+            storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>());
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
+            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), leftResult.getTruthValues(), rightResult.getTruthValues(), nondeterministicLinearEquationSolver, qualitative)));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const {
+            // Only compute the result if the model has at least one reward model.
+            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Compute the reward vector to add in each step based on the available reward models.
+            std::vector<ValueType> totalRewardVector;
+            if (model.hasTransitionRewards()) {
+                totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
+                if (model.hasStateRewards()) {
+                    storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
+                }
+            } else {
+                totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
+            }
+            
+            // Initialize result to either the state rewards of the model or the null vector.
+            std::vector<ValueType> result;
+            if (model.hasStateRewards()) {
+                result = std::vector<ValueType>(model.getStateRewardVector());
+            } else {
+                result.resize(model.getNumberOfStates());
+            }
+            
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result, &totalRewardVector, stepBound);
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepBound())));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const {
+            // Only compute the result if the model has a state-based reward model.
+            STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Initialize result to state rewards of the model.
+            std::vector<ValueType> result(model.getStateRewardVector());
+            
+            STORM_LOG_THROW(nondeterministicLinearEquationSolver != nullptr, storm::exceptions::InvalidStateException, "No valid linear equation solver available.");
+            this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(minimize, model.getTransitionMatrix(), result, nullptr, stepCount);
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepCount())));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
+            // Only compute the result if the model has at least one reward model.
+            STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Determine which states have a reward of infinity by definition.
+            storm::storage::BitVector infinityStates;
+            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+            if (minimize) {
+                infinityStates = std::move(storm::utility::graph::performProb1A(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), trueStates, targetStates));
+            } else {
+                infinityStates = std::move(storm::utility::graph::performProb1E(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), trueStates, targetStates));
+            }
+            infinityStates.complement();
+            storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
+            LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
+            LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
+            LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+            
+            // Create resulting vector.
+            std::vector<ValueType> result(model.getNumberOfStates());
+            
+            // Check whether we need to compute exact rewards for some states.
+            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
+                LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
+                               << " No exact rewards were computed.");
+                // Set the values for all maybe-states to 1 to indicate that their reward values
+                // are neither 0 nor infinity.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
+            } else {
+                // In this case we have to compute the reward values for the remaining states.
+                
+                // We can eliminate the rows and columns from the original transition probability matrix for states
+                // whose reward values are already known.
+                storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false);
+                
+                // Prepare the right-hand side of the equation system. For entry i this corresponds to
+                // the accumulated probability of going from state i to some 'yes' state.
+                std::vector<ValueType> b(submatrix.getRowCount());
+                
+                if (model.hasTransitionRewards()) {
+                    // If a transition-based reward model is available, we initialize the right-hand
+                    // side to the vector resulting from summing the rows of the pointwise product
+                    // of the transition probability matrix and the transition reward matrix.
+                    std::vector<ValueType> pointwiseProductRowSumVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
+                    storm::utility::vector::selectVectorValues(b, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector);
+                    
+                    if (model.hasStateRewards()) {
+                        // If a state-based reward model is also available, we need to add this vector
+                        // as well. As the state reward vector contains entries not just for the states
+                        // that we still consider (i.e. maybeStates), we need to extract these values
+                        // first.
+                        std::vector<ValueType> subStateRewards(b.size());
+                        storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), model.getStateRewardVector());
+                        storm::utility::vector::addVectorsInPlace(b, subStateRewards);
+                    }
+                } else {
+                    // If only a state-based reward model is  available, we take this vector as the
+                    // right-hand side. As the state reward vector contains entries not just for the
+                    // states that we still consider (i.e. maybeStates), we need to extract these values
+                    // first.
+                    storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, model.getTransitionMatrix().getRowGroupIndices(), model.getStateRewardVector());
+                }
+                
+                // Create vector for results for maybe states.
+                std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
+                
+                // Solve the corresponding system of equations.
+                this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
+                
+                // Set values of resulting vector according to result.
+                storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
+            }
+            
+            // Set values of resulting vector that are known exactly.
+            storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero<ValueType>());
+            storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>());
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValues(), qualitative)));
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+            if (stateFormula.isTrueFormula()) {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
+            } else {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
+            }
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        }
+        
+        template class SparseMdpPrctlModelChecker<double>;
+    }
+}

src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -1,687 +1,48 @@
-/*
+#ifndef STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
- * SparseMdpPrctlModelChecker.h
+#define STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
- *
- *  Created on: 15.02.2013
- *      Author: Christian Dehnert
- */
 
-#ifndef STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
+#include "src/modelchecker/AbstractModelChecker.h"
-#define STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
-
-#include <vector>
-#include <fstream>
-
-#include "src/modelchecker/prctl/AbstractModelChecker.h"
-#include "src/solver/NondeterministicLinearEquationSolver.h"
-#include "src/solver/LinearEquationSolver.h"
 #include "src/models/Mdp.h"
-#include "src/utility/vector.h"
-#include "src/utility/graph.h"
 #include "src/utility/solver.h"
-#include "src/settings/SettingsManager.h"
+#include "src/solver/NondeterministicLinearEquationSolver.h"
-#include "src/storage/TotalScheduler.h"
 
 namespace storm {
     namespace modelchecker {
-        namespace prctl {
+        template<class ValueType>
+        class SparseMdpPrctlModelChecker : public AbstractModelChecker {
+        public:
+            explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model);
+            explicit SparseMdpPrctlModelChecker(storm::models::Mdp<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver);
             
-            /*!
+            // The implemented methods of the AbstractModelChecker interface.
-             * This class represents the base class for all PRCTL model checkers for MDPs.
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
-             */
+            virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            template<class Type>
+            virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            class SparseMdpPrctlModelChecker : public AbstractModelChecker<Type> {
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            public:
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                /*!
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-                 * Constructs a SparseMdpPrctlModelChecker with the given model.
+            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
-                 *
+            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
-                 * @param model The MDP to be checked.
+            // The methods that perform the actual checking.
-                 */
+            std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound);
-				explicit SparseMdpPrctlModelChecker(storm::models::Mdp<Type> const& model) : AbstractModelChecker<Type>(model), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<Type>()) {
+            std::vector<ValueType> computeNextProbabilitiesHelper(bool minimize, storm::storage::BitVector const& nextStates);
-                    // Intentionally left empty.
+            std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
-                }
+            static std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver, bool qualitative);
-                
+            std::vector<ValueType> computeInstantaneousRewardsHelper(bool minimize, uint_fast64_t stepCount) const;
-				explicit SparseMdpPrctlModelChecker(storm::models::Mdp<Type> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver) : AbstractModelChecker<Type>(model), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
+            std::vector<ValueType> computeCumulativeRewardsHelper(bool minimize, uint_fast64_t stepBound) const;
-					// Intentionally left empty.
+            std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const;
-				}
+        protected:
-
+            // The model this model checker is supposed to analyze.
-                /*!
+            storm::models::Mdp<ValueType> const& model;
-                 * Copy constructs a SparseMdpPrctlModelChecker from the given model checker. In particular, this means that the newly
+            // A solver that is used for solving systems of linear equations that are the result of nondeterministic choices.
-                 * constructed model checker will have the model of the given model checker as its associated model.
+            std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver;
-                 */
+        };
-                explicit SparseMdpPrctlModelChecker(storm::modelchecker::prctl::SparseMdpPrctlModelChecker<Type> const& modelchecker)
-                : AbstractModelChecker<Type>(modelchecker), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<Type>()) {
-                    // Intentionally left empty.
-                }
-                
-                /*!
-				 * Virtual destructor. Needs to be virtual, because this class has virtual methods.
-				 */
-                virtual ~SparseMdpPrctlModelChecker() {
-                	// Intentionally left empty.
-                }
-
-                /*!
-                 * Returns a constant reference to the MDP associated with this model checker.
-                 * @returns A constant reference to the MDP associated with this model checker.
-                 */
-                storm::models::Mdp<Type> const& getModel() const {
-                    return AbstractModelChecker<Type>::template getModel<storm::models::Mdp<Type>>();
-                }
-
-            	/*!
-            	 * Checks the given formula that is a P operator over a path formula featuring a value bound.
-            	 *
-            	 * @param formula The formula to check.
-            	 * @return The set of states satisfying the formula represented by a bit vector.
-            	 */
-            	virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::properties::prctl::ProbabilisticBoundOperator<Type> const& formula) const override {
-
-            		// For P< and P<= the MDP satisfies the formula iff the probability maximizing scheduler is used.
-            		// For P> and P>=                "              iff the probability minimizing         "        .
-					if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) {
-						this->minimumOperatorStack.push(false);
-					}
-					else {
-						this->minimumOperatorStack.push(true);
-					}
-
-            		// First, we need to compute the probability for satisfying the path formula for each state.
-            		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
-
-            		//Remove the minimizing operator entry from the stack.
-            		this->minimumOperatorStack.pop();
-
-            		// Create resulting bit vector that will hold the yes/no-answer for every state.
-            		storm::storage::BitVector result(quantitativeResult.size());
-
-            		// Now, we can compute which states meet the bound specified in this operator and set the
-            		// corresponding bits to true in the resulting vector.
-            		for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
-            			if (formula.meetsBound(quantitativeResult[i])) {
-            				result.set(i, true);
-            			}
-            		}
-
-            		return result;
-            	}
-
-            	/*!
-            	 * Checks the given formula that is an R operator over a reward formula featuring a value bound.
-            	 *
-            	 * @param formula The formula to check.
-            	 * @return The set of states satisfying the formula represented by a bit vector.
-            	 */
-            	virtual storm::storage::BitVector checkRewardBoundOperator(const storm::properties::prctl::RewardBoundOperator<Type>& formula) const override {
-
-            		// For R< and R<= the MDP satisfies the formula iff the reward maximizing scheduler is used.
-					// For R> and R>=                "              iff the reward minimizing         "        .
-					if(formula.getComparisonOperator() == storm::properties::LESS || formula.getComparisonOperator() == storm::properties::LESS_EQUAL) {
-						this->minimumOperatorStack.push(false);
-					}
-					else {
-						this->minimumOperatorStack.push(true);
-					}
-
-            		// First, we need to compute the probability for satisfying the path formula for each state.
-            		std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
-
-            		//Remove the minimizing operator entry from the stack.
-					this->minimumOperatorStack.pop();
-
-            		// Create resulting bit vector that will hold the yes/no-answer for every state.
-            		storm::storage::BitVector result(quantitativeResult.size());
-
-            		// Now, we can compute which states meet the bound specified in this operator and set the
-            		// corresponding bits to true in the resulting vector.
-            		for (uint_fast64_t i = 0; i < quantitativeResult.size(); ++i) {
-            			if (formula.meetsBound(quantitativeResult[i])) {
-            				result.set(i, true);
-            			}
-            		}
-
-            		return result;
-            	}
-
-                /*!
-                 * Computes the probability to satisfy phi until psi within a limited number of steps for each state.
-                 *
-                 * @param phiStates A bit vector indicating which states satisfy phi.
-                 * @param psiStates A bit vector indicating which states satisfy psi.
-                 * @param stepBound The upper bound for the number of steps.
-                 * @param qualitative A flag indicating whether the check only needs to be done qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @return The probabilities for satisfying phi until psi within a limited number of steps for each state.
-                 * If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                std::vector<Type> checkBoundedUntil(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, bool qualitative) const {
-                    // First test if it is specified if the minimum or maximum probabilities are to be computed.
-                	if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-                	}
-
-                	std::vector<Type> result(this->getModel().getNumberOfStates());
-
-                    // Determine the states that have 0 probability of reaching the target states.
-                    storm::storage::BitVector statesWithProbabilityGreater0;
-                    if (this->minimumOperatorStack.top()) {
-                        statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
-                    } else {
-                        statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound);
-                    }
-                    
-                    // Check if we already know the result (i.e. probability 0) for all initial states and
-                    // don't compute anything in this case.
-                    if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
-                        LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
-                                       << " No exact probabilities were computed.");
-                        // Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and
-                        // not necessarily 1).
-                        storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, Type(0.5));
-                    } else {
-                        // In this case we have have to compute the probabilities.
-                        
-                        // We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
-                        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, statesWithProbabilityGreater0, statesWithProbabilityGreater0, false);
-                        
-                        // Compute the new set of target states in the reduced system.
-                        storm::storage::BitVector rightStatesInReducedSystem = psiStates % statesWithProbabilityGreater0;
-                        
-                        // Make all rows absorbing that satisfy the second sub-formula.
-                        submatrix.makeRowGroupsAbsorbing(rightStatesInReducedSystem);
-                        
-                        // Create the vector with which to multiply.
-                        std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
-                        storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constantOne<Type>());
-                        
-                        this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, nullptr, stepBound);
-                        
-                        // Set the values of the resulting vector accordingly.
-                        storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
-                        storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::constantZero<Type>());
-                    }
-                    
-                    return result;
-                }
-                
-                /*!
-                 * Checks the given formula that is a bounded-until formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @return The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkBoundedUntil(storm::properties::prctl::BoundedUntil<Type> const& formula, bool qualitative) const {
-                    return checkBoundedUntil(formula.getLeft()->check(*this), formula.getRight()->check(*this), formula.getBound(), qualitative);
-                }
-                
-                /*!
-                 * Computes the probability to reach the given set of states in the next step for each state.
-                 *
-                 * @param nextStates A bit vector defining the states to reach in the next state.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @return The probabilities to reach the gien set of states in the next step for each state. If the
-                 * qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkNext(storm::storage::BitVector const& nextStates, bool qualitative) const {
-                	// First test if it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    // Create the vector with which to multiply and initialize it correctly.
-                    std::vector<Type> result(this->getModel().getNumberOfStates());
-                    storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constantOne<Type>());
-                    
-                    this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result);
-                    
-                    return result;
-                }
-                
-                /*!
-                 * Checks the given formula that is a next formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @return The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkNext(const storm::properties::prctl::Next<Type>& formula, bool qualitative) const {
-                    return checkNext(formula.getChild()->check(*this), qualitative);
-                }
-                
-                /*!
-                 * Checks the given formula that is a bounded-eventually formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkBoundedEventually(const storm::properties::prctl::BoundedEventually<Type>& formula, bool qualitative) const {
-                    // Create equivalent temporary bounded until formula and check it.
-                    storm::properties::prctl::BoundedUntil<Type> temporaryBoundedUntilFormula(std::shared_ptr<storm::properties::prctl::Ap<Type>>(new storm::properties::prctl::Ap<Type>("true")), formula.getChild(), formula.getBound());
-                    return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative);
-                }
-                
-                /*!
-                 * Checks the given formula that is an eventually formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkEventually(const storm::properties::prctl::Eventually<Type>& formula, bool qualitative) const {
-                    // Create equivalent temporary until formula and check it.
-                    storm::properties::prctl::Until<Type> temporaryUntilFormula(std::shared_ptr<storm::properties::prctl::Ap<Type>>(new storm::properties::prctl::Ap<Type>("true")), formula.getChild());
-                    return this->checkUntil(temporaryUntilFormula, qualitative);
-                }
-                
-                /*!
-                 * Checks the given formula that is a globally formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @returns The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkGlobally(const storm::properties::prctl::Globally<Type>& formula, bool qualitative) const {
-                    // Create "equivalent" temporary eventually formula and check it.
-                    storm::properties::prctl::Eventually<Type> temporaryEventuallyFormula(std::shared_ptr<storm::properties::prctl::Not<Type>>(new storm::properties::prctl::Not<Type>(formula.getChild())));
-                    std::vector<Type> result = this->checkEventually(temporaryEventuallyFormula, qualitative);
-                    
-                    // Now subtract the resulting vector from the constant one vector to obtain final result.
-                    storm::utility::vector::subtractFromConstantOneVector(result);
-                    return result;
-                }
-                
-                /*!
-                 * Check the given formula that is an until formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @param scheduler If <code>qualitative</code> is false and this vector is non-null and has as many elements as
-                 * there are states in the MDP, this vector will represent a scheduler for the model that achieves the probability
-                 * returned by model checking. To this end, the vector will hold the nondeterministic choice made for each state.
-                 * @return The probabilities for the given formula to hold on every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact probabilities might not be computed.
-                 */
-                virtual std::vector<Type> checkUntil(const storm::properties::prctl::Until<Type>& formula, bool qualitative) const {
-                	// First test if it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    return this->checkUntil(this->minimumOperatorStack.top(), formula.getLeft()->check(*this), formula.getRight()->check(*this), qualitative).first;
-                }
-                
-                /*!
-                 * Computes the extremal probability to satisfy phi until psi for each state in the model.
-                 *
-                 * @param minimize If set, the probability is minimized and maximized otherwise.
-                 * @param phiStates A bit vector indicating which states satisfy phi.
-                 * @param psiStates A bit vector indicating which states satisfy psi.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bounds 0 and 1.
-                 * @param scheduler If <code>qualitative</code> is false and this vector is non-null and has as many elements as
-                 * there are states in the MDP, this vector will represent a scheduler for the model that achieves the probability
-                 * returned by model checking. To this end, the vector will hold the nondeterministic choice made for each state.
-                 * @return The probabilities for the satisfying phi until psi for each state of the model. If the
-                 * qualitative flag is set, exact probabilities might not be computed.
-                 */
-                static std::pair<std::vector<Type>, storm::storage::TotalScheduler> computeUnboundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, storm::storage::SparseMatrix<Type> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver, bool qualitative) {
-                    size_t numberOfStates = phiStates.size();
-
-                    // We need to identify the states which have to be taken out of the matrix, i.e.
-                    // all states that have probability 0 and 1 of satisfying the until-formula.
-                    std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
-                    if (minimize) {
-                        statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
-
-                    } else {
-                        statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates);
-                    }
-                    storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
-                    storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
-                    storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-                    LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
-                    LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
-                    LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-
-                    // Create resulting vector.
-                    std::vector<Type> result(numberOfStates);
-                    
-                    // Check whether we need to compute exact probabilities for some states.
-                    if (initialStates.isDisjointFrom(maybeStates) || qualitative) {
-                        if (qualitative) {
-                            LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed.");
-                        } else {
-                            LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
-                                           << " No exact probabilities were computed.");
-                        }
-                        // Set the values for all maybe-states to 0.5 to indicate that their probability values
-                        // are neither 0 nor 1.
-                        storm::utility::vector::setVectorValues<Type>(result, maybeStates, Type(0.5));
-                    } else {
-                        // In this case we have have to compute the probabilities.
-
-                        // First, we can eliminate the rows and columns from the original transition probability matrix for states
-                        // whose probabilities are already known.
-                        storm::storage::SparseMatrix<Type> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false);
-                        
-                        // Prepare the right-hand side of the equation system. For entry i this corresponds to
-                        // the accumulated probability of going from state i to some 'yes' state.
-                        std::vector<Type> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1);
-                        
-                        // Create vector for results for maybe states.
-                        std::vector<Type> x(maybeStates.getNumberOfSetBits());
-                        
-                        // Solve the corresponding system of equations.
-                        nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
-                        
-                        // Set values of resulting vector according to result.
-                        storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
-                    }
-                    
-                    // Set values of resulting vector that are known exactly.
-                    storm::utility::vector::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constantZero<Type>());
-                    storm::utility::vector::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constantOne<Type>());
-                    
-                    // Finally, compute a scheduler that achieves the extramal value.
-                    storm::storage::TotalScheduler scheduler = computeExtremalScheduler(minimize, transitionMatrix, result);
-
-                    return std::make_pair(result, scheduler);
-                }
-                
-                std::pair<std::vector<Type>, storm::storage::TotalScheduler> checkUntil(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const {
-                    return computeUnboundedUntilProbabilities(minimize, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getInitialStates(), phiStates, psiStates, this->nondeterministicLinearEquationSolver, qualitative);
-                }
-                
-                /*!
-                 * Checks the given formula that is an instantaneous reward formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bound 0. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bound 0.
-                 * @return The reward values for the given formula for every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact values might not be computed.
-                 */
-                virtual std::vector<Type> checkInstantaneousReward(const storm::properties::prctl::InstantaneousReward<Type>& formula, bool qualitative) const {
-                    // Only compute the result if the model has a state-based reward model.
-                    if (!this->getModel().hasStateRewards()) {
-                        LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula.");
-                        throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula.";
-                    }
-                    
-                    // Now test whether it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    // Initialize result to state rewards of the model.
-                    std::vector<Type> result(this->getModel().getStateRewardVector());
-                    
-                    this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, nullptr, formula.getBound());
-                    
-                    return result;
-                }
-                
-                /*!
-                 * Check the given formula that is a cumulative reward formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bound 0. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bound 0.
-                 * @return The reward values for the given formula for every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact values might not be computed.
-                 */
-                virtual std::vector<Type> checkCumulativeReward(const storm::properties::prctl::CumulativeReward<Type>& formula, bool qualitative) const {
-                    // Only compute the result if the model has at least one reward model.
-                    if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) {
-                        LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
-                        throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
-                    }
-                    
-                    // Now test whether it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    // Compute the reward vector to add in each step based on the available reward models.
-                    std::vector<Type> totalRewardVector;
-                    if (this->getModel().hasTransitionRewards()) {
-                        totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
-                        if (this->getModel().hasStateRewards()) {
-                            storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
-                        }
-                    } else {
-                        totalRewardVector = std::vector<Type>(this->getModel().getStateRewardVector());
-                    }
-                    
-                    // Initialize result to either the state rewards of the model or the null vector.
-                    std::vector<Type> result;
-                    if (this->getModel().hasStateRewards()) {
-                        result = std::vector<Type>(this->getModel().getStateRewardVector());
-                    } else {
-                        result.resize(this->getModel().getNumberOfStates());
-                    }
-                    
-					this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, &totalRewardVector, static_cast<uint_fast64_t>(formula.getBound()));
-                    
-                    return result;
-                }
-                
-                /*!
-                 * Checks the given formula that is a reachability reward formula.
-                 *
-                 * @param formula The formula to check.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bound 0. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bound 0.
-                 * @return The reward values for the given formula for every state of the model associated with this model
-                 * checker. If the qualitative flag is set, exact values might not be computed.
-                 */
-                virtual std::vector<Type> checkReachabilityReward(const storm::properties::prctl::ReachabilityReward<Type>& formula, bool qualitative) const {
-                	// First test whether it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    return this->checkReachabilityReward(this->minimumOperatorStack.top(), formula.getChild()->check(*this), qualitative).first;
-                }
-                
-                /*!
-                 * Computes the expected reachability reward that is gained before a target state is reached for each state.
-                 *
-                 * @param minimize If set, the reward is to be minimized and maximized otherwise.
-                 * @param targetStates The target states before which rewards can be gained.
-                 * @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the
-                 * results are only compared against the bound 0. If set to true, this will most likely results that are only
-                 * qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the
-                 * bound 0.
-                 * @param scheduler If <code>qualitative</code> is false and this vector is non-null and has as many elements as
-                 * there are states in the MDP, this vector will represent a scheduler for the model that achieves the probability
-                 * returned by model checking. To this end, the vector will hold the nondeterministic choice made for each state.
-                 * @return The expected reward values gained before a target state is reached for each state. If the
-                 * qualitative flag is set, exact values might not be computed.
-                 */
-                virtual std::pair<std::vector<Type>, storm::storage::TotalScheduler> checkReachabilityReward(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
-                    // Only compute the result if the model has at least one reward model.
-                    if (!(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards())) {
-                        LOG4CPLUS_ERROR(logger, "Missing reward model for formula.");
-                        throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula.";
-                    }
-                    
-                    // Also test whether it is specified if the minimum or maximum probabilities are to be computed.
-					if(this->minimumOperatorStack.empty()) {
-						LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.");
-						throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models.";
-					}
-
-                    // Determine which states have a reward of infinity by definition.
-                    storm::storage::BitVector infinityStates;
-                    storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
-                    if (minimize) {
-                        infinityStates = std::move(storm::utility::graph::performProb1A(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
-                    } else {
-                        infinityStates = std::move(storm::utility::graph::performProb1E(this->getModel().getTransitionMatrix(), this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getBackwardTransitions(), trueStates, targetStates));
-                    }
-                    infinityStates.complement();
-                    storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
-                    LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
-                    LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
-                    LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
-                    
-                    // Create resulting vector.
-                    std::vector<Type> result(this->getModel().getNumberOfStates());
-                    
-                    // Check whether we need to compute exact rewards for some states.
-                    if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) {
-                        LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
-                                       << " No exact rewards were computed.");
-                        // Set the values for all maybe-states to 1 to indicate that their reward values
-                        // are neither 0 nor infinity.
-                        storm::utility::vector::setVectorValues<Type>(result, maybeStates, storm::utility::constantOne<Type>());
-                    } else {
-                        // In this case we have to compute the reward values for the remaining states.
-                        
-                        // We can eliminate the rows and columns from the original transition probability matrix for states
-                        // whose reward values are already known.
-                        storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false);
-                        
-                        // Prepare the right-hand side of the equation system. For entry i this corresponds to
-                        // the accumulated probability of going from state i to some 'yes' state.
-                        std::vector<Type> b(submatrix.getRowCount());
-                        
-                        if (this->getModel().hasTransitionRewards()) {
-                            // If a transition-based reward model is available, we initialize the right-hand
-                            // side to the vector resulting from summing the rows of the pointwise product
-                            // of the transition probability matrix and the transition reward matrix.
-                            std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
-                            storm::utility::vector::selectVectorValues(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), pointwiseProductRowSumVector);
-                            
-                            if (this->getModel().hasStateRewards()) {
-                                // If a state-based reward model is also available, we need to add this vector
-                                // as well. As the state reward vector contains entries not just for the states
-                                // that we still consider (i.e. maybeStates), we need to extract these values
-                                // first.
-                                std::vector<Type> subStateRewards(b.size());
-                                storm::utility::vector::selectVectorValuesRepeatedly(subStateRewards, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
-                                storm::utility::vector::addVectorsInPlace(b, subStateRewards);
-                            }
-                        } else {
-                            // If only a state-based reward model is  available, we take this vector as the
-                            // right-hand side. As the state reward vector contains entries not just for the
-                            // states that we still consider (i.e. maybeStates), we need to extract these values
-                            // first.
-                            storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getTransitionMatrix().getRowGroupIndices(), this->getModel().getStateRewardVector());
-                        }
-                        
-                        // Create vector for results for maybe states.
-                        std::vector<Type> x(maybeStates.getNumberOfSetBits());
-                        
-                        // Solve the corresponding system of equations.
-                        this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b);
-                        
-                        // Set values of resulting vector according to result.
-                        storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
-                    }
-                    
-                    // Set values of resulting vector that are known exactly.
-                    storm::utility::vector::setVectorValues(result, targetStates, storm::utility::constantZero<Type>());
-                    storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constantInfinity<Type>());
-                    
-                    // Finally, compute a scheduler that achieves the extramal value.
-                    storm::storage::TotalScheduler scheduler = computeExtremalScheduler(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().hasStateRewards() ? &this->getModel().getStateRewardVector() : nullptr, this->getModel().hasTransitionRewards() ? &this->getModel().getTransitionRewardMatrix() : nullptr);
-
-                    return std::make_pair(result, scheduler);
-                }
-                
-            protected:
-                /*!
-                 * Computes the vector of choices that need to be made to minimize/maximize the model checking result for each state.
-                 *
-                 * @param minimize If set, all choices are resolved such that the solution value becomes minimal and maximal otherwise.
-                 * @param nondeterministicResult The model checking result for nondeterministic choices of all states.
-                 * @param takenChoices The output vector that is to store the taken choices.
-                 */
-                static storm::storage::TotalScheduler computeExtremalScheduler(bool minimize, storm::storage::SparseMatrix<Type> const& transitionMatrix, std::vector<Type> const& result, std::vector<Type> const* stateRewardVector = nullptr, storm::storage::SparseMatrix<Type> const* transitionRewardMatrix = nullptr) {
-                    std::vector<Type> temporaryResult(result.size());
-                    std::vector<Type> nondeterministicResult(transitionMatrix.getRowCount());
-                    transitionMatrix.multiplyWithVector(result, nondeterministicResult);
-                                                        
-                    if (stateRewardVector != nullptr || transitionRewardMatrix != nullptr) {
-                        std::vector<Type> totalRewardVector;
-                        if (transitionRewardMatrix != nullptr) {
-                            totalRewardVector = transitionMatrix.getPointwiseProductRowSumVector(*transitionRewardMatrix);
-                            if (stateRewardVector != nullptr) {
-                                std::vector<Type> stateRewards(totalRewardVector.size());
-                                storm::utility::vector::selectVectorValuesRepeatedly(stateRewards, storm::storage::BitVector(stateRewardVector->size(), true), transitionMatrix.getRowGroupIndices(), *stateRewardVector);
-                                storm::utility::vector::addVectorsInPlace(totalRewardVector, stateRewards);
-                            }
-                        } else {
-                            totalRewardVector.resize(nondeterministicResult.size());
-                            storm::utility::vector::selectVectorValuesRepeatedly(totalRewardVector, storm::storage::BitVector(stateRewardVector->size(), true), transitionMatrix.getRowGroupIndices(), *stateRewardVector);
-                        }
-                        storm::utility::vector::addVectorsInPlace(nondeterministicResult, totalRewardVector);
-                    }
-                    
-                    std::vector<uint_fast64_t> choices(result.size());
-                    
-                    if (minimize) {
-                        storm::utility::vector::reduceVectorMin(nondeterministicResult, temporaryResult, transitionMatrix.getRowGroupIndices(), &choices);
-                    } else {
-                        storm::utility::vector::reduceVectorMax(nondeterministicResult, temporaryResult, transitionMatrix.getRowGroupIndices(), &choices);
-                    }
-
-                    return storm::storage::TotalScheduler(choices);
-                }
-
-                /*!
-                 * A solver that is used for solving systems of linear equations that are the result of nondeterministic choices.
-                 */
-                std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver;
-            };
-        } // namespace prctl
     } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_ */

src/parser/FormulaParser.cpp

@@ -38,7 +38,7 @@ namespace storm {
             booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
             booleanLiteralFormula.name("boolean literal formula");
             
-            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | qi::lit("(") > stateFormula > qi::lit(")");
+            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")"));
             atomicStateFormula.name("atomic state formula");
 
             notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
@@ -74,7 +74,7 @@ namespace storm {
             formula = stateFormula | pathFormula;
             formula.name("formula");
             
-            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | qi::lit("=") > qi::lit("?")))[qi::_val = phoenix::construct<std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(qi::_a, qi::_b, qi::_c)];
+            operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct<std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(qi::_a, qi::_b, qi::_c)];
             operatorInformation.name("operator information");
             
             steadyStateOperator = (qi::lit("S") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createSteadyStateOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];

test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp

@@ -19,7 +19,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
 	ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
 	ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
 
-	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+	storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
     
     auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("one");
     auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -27,7 +27,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
-	ASSERT_LT(std::abs(quantitativeResult1[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
     labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
     eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -35,7 +35,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
     result = checker.check(*eventuallyFormula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
-	ASSERT_LT(std::abs(quantitativeResult2[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
     labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
     eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@@ -43,7 +43,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
     result = checker.check(*eventuallyFormula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
-	ASSERT_LT(std::abs(quantitativeResult3[0] - ((double)1.0/6.0)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
     auto done = std::make_shared<storm::logic::AtomicLabelFormula>("done");
     auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(done);
@@ -51,72 +51,79 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
     result = checker.check(*reachabilityRewardFormula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
     
-	ASSERT_LT(std::abs(quantitativeResult4[0] - ((double)11/3)), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 }
 
-//TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
+TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
-//	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
-//
+	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
-//	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
-//
+	ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
-//	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+	ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
-//
+    storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-//	ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-//	ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
-//	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observe0Greater1");
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
-//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//
+    result = checker.check(*eventuallyFormula);
-//	std::vector<double> result = eventuallyFormula->check(mc, false);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
-//
+    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeIGreater1");
+    result = checker.check(*eventuallyFormula);
-//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	result = eventuallyFormula->check(mc, false);
+}
-//
+TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
-//	ASSERT_LT(std::abs(result[0] - 0.1522194965), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
-//
+	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("observeOnlyTrueSender");
+	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
-//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+	ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
-//
+	ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
-//	result = eventuallyFormula->check(mc, false);
+    storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
-//
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//	ASSERT_LT(std::abs(result[0] - 0.32153724292835045), storm::settings::gmmxxEquationSolverSettings().getPrecision());
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//}
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
-//
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-//TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
+	EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//
+    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-//	ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
-//	std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
+    result = checker.check(*boundedUntilFormula);
-//
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-//	ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
+	EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//
+    auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
-//	storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
+    result = checker.check(*reachabilityRewardFormula);
-//
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+	EXPECT_NEAR(1.044879046, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+}
-//
-//	std::vector<double> result = eventuallyFormula->check(mc, false);
-//
-//	ASSERT_LT(std::abs(result[0] - 1.0), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-//	auto boundedUntilFormula = std::make_shared<storm::properties::prctl::BoundedUntil<double>>(std::make_shared<storm::properties::prctl::Ap<double>>("true"), apFormula, 20);
-//
-//	result = boundedUntilFormula->check(mc, false);
-//
-//	ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
-//
-//	result = reachabilityRewardFormula->check(mc, false);
-//
-//	ASSERT_LT(std::abs(result[0] - 1.044879046), storm::settings::gmmxxEquationSolverSettings().getPrecision());
-//}

test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@@ -1,148 +1,196 @@
-//#include "gtest/gtest.h"
+#include "gtest/gtest.h"
-//#include "storm-config.h"
+#include "storm-config.h"
-//
+#include "src/logic/Formulas.h"
-//#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
+#include "src/solver/NativeNondeterministicLinearEquationSolver.h"
-//#include "src/settings/SettingsManager.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
-//#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
-//#include "src/parser/AutoParser.h"
+#include "src/settings/SettingsManager.h"
-//
+#include "src/parser/AutoParser.h"
-//TEST(SparseMdpPrctlModelCheckerTest, Dice) {
+TEST(SparseMdpPrctlModelCheckerTest, Dice) {
-//	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
-//    
+	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
-//	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
+	std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
-//    
+	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
-//	std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
+	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
-//    
+    storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-//	ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
-//	ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//    
+    auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
-//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
-//    
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("two");
+	EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
-//    
+    result = checker.check(*maxProbabilityOperatorFormula);
-//	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-//    
+	EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
-//    
+    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
+    minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
-//
+    result = checker.check(*minProbabilityOperatorFormula);
-//	ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), storm::settings::nativeEquationSolverSettings().getPrecision());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-//    
+	EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("three");
+    maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
-//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    result = checker.check(*maxProbabilityOperatorFormula);
-//    
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
+	EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//    
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
-//	ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
+    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//    
+    minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
+    result = checker.check(*minProbabilityOperatorFormula);
-//
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
-//	ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), storm::settings::nativeEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//    
+    maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("four");
+    result = checker.check(*maxProbabilityOperatorFormula);
-//	eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
-//    
+	EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, true);
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
-//    
+	auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
-//	ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
+    auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
-//
+    result = checker.check(*minRewardOperatorFormula);
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
-//    
+	EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), storm::settings::nativeEquationSolverSettings().getPrecision());
+    auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
-//
+    result = checker.check(*maxRewardOperatorFormula);
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
-//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
+	EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//
+	abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
-//	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
+	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
-//
+	std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
-//	ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
+    storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-//
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
-//	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
+    reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
-//
+    minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
-//	ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
+	result = stateRewardModelChecker.check(*minRewardOperatorFormula);
-//    
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
-//	abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
+	EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//    
+    maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
-//	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
+	result = stateRewardModelChecker.check(*maxRewardOperatorFormula);
-//    
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
-//	std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
+	EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//    
+	abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
-//    storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
-//
+	std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
+	storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-//	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
-//
+    reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
-//	result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
+    minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
-//    
+    result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula);
-//	ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	result = stateRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
+    maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
-//
+    result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula);
-//	ASSERT_LT(std::abs(result[0] - 7.333329499), storm::settings::nativeEquationSolverSettings().getPrecision());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
-//    
+	EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
+}
-//    
+TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
-//	ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
+	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
-//    
+	ASSERT_EQ(storm::models::MDP, abstractModel->getType());
-//	std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
+	std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
-//    
+	ASSERT_EQ(3172ull, mdp->getNumberOfStates());
-//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+	ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
-//    
+    storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("done");
+    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//	reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
+    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
-//    
+    auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
-//	result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, true);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
-//    
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
-//	ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//
+    auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
-//	result = stateAndTransitionRewardModelChecker.checkOptimizingOperator(*reachabilityRewardFormula, false);
+    result = checker.check(*maxProbabilityOperatorFormula);
-//
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
-//	ASSERT_LT(std::abs(result[0] - 14.666658998), storm::settings::nativeEquationSolverSettings().getPrecision());
+	EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//}
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//
+    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-//TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
+    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
-//	std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
+    minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
-//
+    result = checker.check(*minProbabilityOperatorFormula);
-//	ASSERT_EQ(storm::models::MDP, abstractModel->getType());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
+    maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
-//
+    result = checker.check(*maxProbabilityOperatorFormula);
-//	ASSERT_EQ(3172ull, mdp->getNumberOfStates());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
-//	ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
+	EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//
+    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-//	storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
+    auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
-//
+    auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
-//	auto apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
+    result = checker.check(*minRewardOperatorFormula);
-//	auto eventuallyFormula = std::make_shared<storm::properties::prctl::Eventually<double>>(apFormula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	std::vector<double> result = mc.checkOptimizingOperator(*eventuallyFormula, true);
+    auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
-//
+    result = checker.check(*maxRewardOperatorFormula);
-//	ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
-//
+	EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
-//	result = mc.checkOptimizingOperator(*eventuallyFormula, false);
+}
-//
-//	ASSERT_LT(std::abs(result[0] - 1), storm::settings::nativeEquationSolverSettings().getPrecision());
-//
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-//	auto boundedEventuallyFormula = std::make_shared<storm::properties::prctl::BoundedEventually<double>>(apFormula, 25);
-//
-//	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, true);
-//
-//	ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
-//
-//	result = mc.checkOptimizingOperator(*boundedEventuallyFormula, false);
-//
-//	ASSERT_LT(std::abs(result[0] - 0.0625), storm::settings::nativeEquationSolverSettings().getPrecision());
-//
-//	apFormula = std::make_shared<storm::properties::prctl::Ap<double>>("elected");
-//	auto reachabilityRewardFormula = std::make_shared<storm::properties::prctl::ReachabilityReward<double>>(apFormula);
-//
-//	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, true);
-//
-//	ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
-//
-//	result = mc.checkOptimizingOperator(*reachabilityRewardFormula, false);
-//
-//	ASSERT_LT(std::abs(result[0] - 4.285689611), storm::settings::nativeEquationSolverSettings().getPrecision());
-//}

test/functional/parser/FormulaParserTest.cpp

@@ -96,7 +96,7 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) {
     std::shared_ptr<storm::logic::Formula> formula(nullptr);
     ASSERT_NO_THROW(formula = parser.parseFromString(input));
     
-    EXPECT_TRUE(formula->isRewardOperatorFormula());
+    EXPECT_TRUE(formula->isProbabilityOperatorFormula());
     storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula();
     EXPECT_TRUE(probFormula.getSubformula().isConditionalPathFormula());
 }