game-based abstraction working with rational numbers

src/storm/abstraction/AbstractionInformation.cpp

@@ -491,7 +491,7 @@ namespace storm {
         template <storm::dd::DdType DdType>
         template <typename ValueType>
         std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> AbstractionInformation<DdType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
-            std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> result;
+            std::map<uint_fast64_t, std::pair<storm::storage::BitVector, ValueType>> result;
             
             storm::dd::Add<DdType, double> lowerChoiceAsAdd = choice.template toAdd<double>();
             for (auto const& successorValuePair : lowerChoiceAsAdd) {
@@ -614,8 +614,10 @@ namespace storm {
         
         template std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> AbstractionInformation<storm::dd::DdType::CUDD>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<storm::dd::DdType::CUDD> const& choice) const;
         template std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>> AbstractionInformation<storm::dd::DdType::Sylvan>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<storm::dd::DdType::Sylvan > const& choice) const;
+        template std::map<uint_fast64_t, std::pair<storm::storage::BitVector, storm::RationalNumber>> AbstractionInformation<storm::dd::DdType::Sylvan>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<storm::dd::DdType::Sylvan > const& choice) const;
 
         template std::vector<std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>>> AbstractionInformation<storm::dd::DdType::CUDD>::decodeChoicesToUpdateSuccessorMapping(std::set<storm::expressions::Variable> const& player2Variables, storm::dd::Bdd<storm::dd::DdType::CUDD> const& choices) const;
         template std::vector<std::map<uint_fast64_t, std::pair<storm::storage::BitVector, double>>> AbstractionInformation<storm::dd::DdType::Sylvan>::decodeChoicesToUpdateSuccessorMapping(std::set<storm::expressions::Variable> const& player2Variables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& choices) const;
+        template std::vector<std::map<uint_fast64_t, std::pair<storm::storage::BitVector, storm::RationalNumber>>> AbstractionInformation<storm::dd::DdType::Sylvan>::decodeChoicesToUpdateSuccessorMapping(std::set<storm::expressions::Variable> const& player2Variables, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& choices) const;
     }
 }

src/storm/api/verification.h

@@ -38,7 +38,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
+        typename std::enable_if<std::is_same<ValueType, double>::value || std::is_same<ValueType, storm::RationalNumber>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
             STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine.");
             
             std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -60,7 +60,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        typename std::enable_if<!std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const&) {
+        typename std::enable_if<!std::is_same<ValueType, double>::value && !std::is_same<ValueType, storm::RationalNumber>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const&) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type.");
         }
         

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -713,13 +713,19 @@ namespace storm {
                 quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
                 quantitativeWatch.stop();
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
+                totalSolutionWatch.add(quantitativeWatch);
                 if (result) {
-                    totalSolutionWatch.add(quantitativeWatch);
                     return result;
                 }
                                 
-                totalSolutionWatch.add(quantitativeWatch);
-                STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                ValueType minVal = quantitativeResult.min.getInitialStatesRange().first;
+                ValueType maxVal = quantitativeResult.max.getInitialStatesRange().second;
+                if (std::is_same<ValueType, double>::value) {
+                    STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                } else {
+                    STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                }
+
                 
                 // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
                 result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
@@ -1142,7 +1148,7 @@ namespace storm {
                 ValueType maxDiff = storm::utility::zero<ValueType>();
                 uint64_t maxState = 0;
                 for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
-                    ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMin().getValues()[state]);
+                    ValueType diff = storm::utility::abs(ValueType(sanityValues[state] - quantitativeResult.getMin().getValues()[state]));
                     if (diff > maxDiff) {
                         maxState = state;
                         maxDiff = diff;
@@ -1180,7 +1186,7 @@ namespace storm {
                 maxDiff = storm::utility::zero<ValueType>();
                 maxState = 0;
                 for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
-                    ValueType const& diff = storm::utility::abs(sanityValues[state] - quantitativeResult.getMax().getValues()[state]);
+                    ValueType diff = storm::utility::abs(ValueType(sanityValues[state] - quantitativeResult.getMax().getValues()[state]));
                     if (diff > maxDiff) {
                         maxState = state;
                         maxDiff = diff;
@@ -1373,11 +1379,18 @@ namespace storm {
                 quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, odd, &quantitativeResult.getMin(), &minStrategyPair));
                 quantitativeWatch.stop();
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates));
+                totalSolutionWatch.add(quantitativeWatch);
                 if (result) {
-                    totalSolutionWatch.add(quantitativeWatch);
                     return result;
                 }
-                STORM_LOG_INFO("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                
+                ValueType minVal = quantitativeResult.getMin().getRange(initialStates).first;
+                ValueType maxVal = quantitativeResult.getMax().getRange(initialStates).second;
+                if (std::is_same<ValueType, double>::value) {
+                    STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                } else {
+                    STORM_LOG_INFO("Obtained quantitative bounds [" << minVal << ", " << maxVal << "] (approx. [" << storm::utility::convertNumber<double>(minVal) << ", " << storm::utility::convertNumber<double>(maxVal) << "]) on the actual value for the initial states in " << quantitativeWatch.getTimeInMilliseconds() << "ms.");
+                }
                 
                 // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
                 result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.getMin().getRange(initialStates).first, quantitativeResult.getMax().getRange(initialStates).second, comparator);

src/storm/utility/ConstantsComparator.cpp

@@ -112,7 +112,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        ConstantsComparator<storm::RationalNumber>::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(false) {
+        ConstantsComparator<storm::RationalNumber>::ConstantsComparator(storm::RationalNumber precision, bool relative) : precision(precision), relative(relative) {
             // Intentionally left empty.
         }
         
@@ -120,7 +120,7 @@ namespace storm {
             if (storm::utility::isZero(precision)) {
                 return storm::utility::isOne(value);
             }
-            return storm::utility::abs(value - one<double>()) <= precision;
+            return storm::utility::abs(storm::RationalNumber(value - one<storm::RationalNumber>())) <= precision;
         }
         
         bool ConstantsComparator<storm::RationalNumber>::isZero(storm::RationalNumber const& value) const {
@@ -136,9 +136,9 @@ namespace storm {
             }
             
             if (relative) {
-                return value1 == value2 || storm::utility::abs(value1 - value2)/storm::utility::abs(value1 + value2) <= precision;
+                return value1 == value2 || storm::utility::abs(storm::RationalNumber(value1 - value2))/storm::utility::abs(storm::RationalNumber(value1 + value2)) <= precision;
             } else {
-                return storm::utility::abs(value1 - value2) <= precision;
+                return storm::utility::abs(storm::RationalNumber(value1 - value2)) <= precision;
             }
         }
         

src/storm/utility/constants.h

@@ -38,7 +38,7 @@ namespace storm {
             
             struct DoubleLess {
                 bool operator()(double a, double b) const {
-                    return b - a > 1e-17;
+                    return b - a > 1e-18;
                 }
             };
             
@@ -54,7 +54,7 @@ namespace storm {
             
             struct DoubleGreater {
                 bool operator()(double a, double b) const {
-                    return a - b > 1e-17;
+                    return a - b > 1e-18;
                 }
             };
             

src/storm/utility/graph.cpp

@@ -1736,6 +1736,10 @@ namespace storm {
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
+            template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<storm::RationalNumber> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair);
+            
+            template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<storm::RationalNumber> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategyPair* strategyPair, boost::optional<storm::storage::BitVector> const& player1Candidates);
+            
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
             // End of instantiations for storm::RationalNumber.
             
@@ -1908,6 +1912,10 @@ namespace storm {
 
             template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
 
+            template SymbolicGameProb01Result<storm::dd::DdType::Sylvan> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
+
+            template SymbolicGameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::dd::Bdd<storm::dd::DdType::Sylvan>> const& player1Candidates);
+
             // Instantiations for Sylvan (rational function).
             
             template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());