more value-reuse

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -44,9 +44,7 @@ namespace storm {
                 for (auto predicateIndex : predicates) {
                     localExpressionInformation.addExpression(predicateIndex);
                 }
-                
-                STORM_LOG_TRACE("Current variable partition is: " << localExpressionInformation);
-                
+                                
                 // Next, we check whether there is work to be done by recomputing the relevant predicates and checking
                 // whether they changed.
                 std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -41,7 +41,7 @@ namespace storm {
         using storm::abstraction::QuantitativeResultMinMax;
         
         template<storm::dd::DdType Type, typename ModelType>
-        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false) {
+        GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) {
             STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Currently only PRISM models are supported by the game-based model checker.");
             storm::prism::Program const& originalProgram = model.asPrismProgram();
             STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
@@ -54,7 +54,9 @@ namespace storm {
                 preprocessedModel = originalProgram;
             }
             
-            reuseQualitativeResults = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseQualitativeResultsSet();
+            bool reuseAll = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseAllResultsSet();
+            reuseQualitativeResults = reuseAll || storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseQualitativeResultsSet();
+            reuseQuantitativeResults = reuseAll || storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseQuantitativeResultsSet();
         }
 
         template<storm::dd::DdType Type, typename ModelType>
@@ -292,6 +294,7 @@ namespace storm {
             
             // Enter the main-loop of abstraction refinement.
             boost::optional<QualitativeResultMinMax<Type>> previousQualitativeResult = boost::none;
+            boost::optional<QuantitativeResult<Type, ValueType>> previousMinQuantitativeResult = boost::none;
             for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
                 auto iterationStart = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Starting iteration " << iterations << ".");
@@ -367,7 +370,8 @@ namespace storm {
                     QuantitativeResultMinMax<Type, ValueType> quantitativeResult;
                     
                     // (7) Solve the min values and check whether we can give the answer already.
-                    quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin);
+                    quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
+                    previousMinQuantitativeResult = quantitativeResult.min;
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue);
                     if (result) {
                         printStatistics(abstractor, game);

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -92,6 +92,9 @@ namespace storm {
             
             /// A flag indicating whether to reuse the qualitative results.
             bool reuseQualitativeResults;
+            
+            /// A flag indicating whether to reuse the quantitative results.
+            bool reuseQuantitativeResults;
         };
     }
 }

src/storm/settings/modules/AbstractionSettings.cpp

@@ -21,6 +21,8 @@ namespace storm {
             const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic";
             const std::string AbstractionSettings::invalidBlockStrategyOptionName = "invalid-blocks";
             const std::string AbstractionSettings::reuseQualitativeResultsOptionName = "reuse-qualitative";
+            const std::string AbstractionSettings::reuseQuantitativeResultsOptionName = "reuse-quantitative";
+            const std::string AbstractionSettings::reuseAllResultsOptionName = "reuse-all";
 
             AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, addAllGuardsOptionName, true, "Sets whether all guards are added as initial predicates.").build());
@@ -40,6 +42,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'command' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, reuseAllResultsOptionName, true, "Sets whether to reuse all results.").build());
             }
             
             bool AbstractionSettings::isAddAllGuardsSet() const {
@@ -97,6 +101,15 @@ namespace storm {
             bool AbstractionSettings::isReuseQualitativeResultsSet() const {
                 return this->getOption(reuseQualitativeResultsOptionName).getHasOptionBeenSet();
             }
+            
+            bool AbstractionSettings::isReuseQuantitativeResultsSet() const {
+                return this->getOption(reuseQuantitativeResultsOptionName).getHasOptionBeenSet();
+            }
+            
+            bool AbstractionSettings::isReuseAllResultsSet() const {
+                return this->getOption(reuseAllResultsOptionName).getHasOptionBeenSet();
+            }
+
         }
     }
 }

src/storm/settings/modules/AbstractionSettings.h

@@ -88,12 +88,26 @@ namespace storm {
                 InvalidBlockDetectionStrategy getInvalidBlockDetectionStrategy() const;
                 
                 /*!
-                 * Retrieves whether the option to reuse the qualitative results.
+                 * Retrieves whether the option to reuse the qualitative results was set.
                  *
                  * @param True iff the option was set.
                  */
                 bool isReuseQualitativeResultsSet() const;
+                
+                /*!
+                 * Retrieves whether the option to reuse the quantitative results was set.
+                 *
+                 * @param True iff the option was set.
+                 */
+                bool isReuseQuantitativeResultsSet() const;
 
+                /*!
+                 * Retrieves whether the option to reuse all results was set.
+                 *
+                 * @param True iff the option was set.
+                 */
+                bool isReuseAllResultsSet() const;
+                
                 const static std::string moduleName;
                 
             private:
@@ -108,6 +122,8 @@ namespace storm {
                 const static std::string pivotHeuristicOptionName;
                 const static std::string invalidBlockStrategyOptionName;
                 const static std::string reuseQualitativeResultsOptionName;
+                const static std::string reuseQuantitativeResultsOptionName;
+                const static std::string reuseAllResultsOptionName;
             };
             
         }

src/storm/solver/SymbolicGameSolver.cpp

@@ -41,7 +41,7 @@ namespace storm {
             }
             boost::optional<storm::dd::Add<Type, ValueType>> previousPlayer2Values;
             if (generatePlayer2Strategy) {
-                if (basePlayer2Strategy) {
+                if (basePlayer2Strategy && player2Goal == storm::OptimizationDirection::Maximize) {
                     player2Strategy = basePlayer2Strategy.get();
 
                     // If we are required to generate a player 2 strategy based on another one that is not the zero strategy,