moved abstraction computation load from refine functions to abstract fcts

src/storm/abstraction/prism/AbstractCommand.cpp

@@ -51,21 +51,12 @@ namespace storm {
                 // whether they changed.
                 std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
                 
-                // If the DD does not need recomputation, we can return the cached result.
-                bool recomputeDd = forceRecomputation || this->relevantPredicatesChanged(newRelevantPredicates);
-                if (!recomputeDd) {
-                    // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities.
-                    cachedDd.bdd &= computeMissingGlobalIdentities();
-                } else {
-                    // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver.
+                // Check whether we need to recompute the abstraction.
+                bool relevantPredicatesChanged = this->relevantPredicatesChanged(newRelevantPredicates);
+                if (relevantPredicatesChanged) {
                     addMissingPredicates(newRelevantPredicates);
-                    
-                    // Finally recompute the cached BDD.
-                    this->recomputeCachedBdd();
-                    
-                    // Disable forcing recomputation until it is set again.
-                    forceRecomputation = false;
                 }
+                forceRecomputation |= relevantPredicatesChanged;
                 
                 // Refine bottom state abstractor. Note that this does not trigger a recomputation yet.
                 bottomStateAbstractor.refine(predicates);
@@ -141,6 +132,7 @@ namespace storm {
                 auto end = std::chrono::high_resolution_clock::now();
                 
                 STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                forceRecomputation = false;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -318,6 +310,12 @@ namespace storm {
 
             template <storm::dd::DdType DdType, typename ValueType>
             GameBddResult<DdType> AbstractCommand<DdType, ValueType>::getAbstractBdd() {
+                if (forceRecomputation) {
+                    this->recomputeCachedBdd();
+                } else {
+                    cachedDd.bdd &= computeMissingGlobalIdentities();
+                }
+                
                 return cachedDd;
             }
             

src/storm/abstraction/prism/AbstractProgram.cpp

@@ -31,7 +31,7 @@ namespace storm {
             AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
                                                                 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
                                                                 bool addAllGuards)
-            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr) {
+            : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr), refinementPerformed(false) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
@@ -103,13 +103,16 @@ namespace storm {
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(newPredicateIndices);
                 
-                // Finally, we rebuild the game.
-                currentGame = buildGame();
+                // Update the flag that stores whether a refinement was performed.
+                refinementPerformed = refinementPerformed || !newPredicateIndices.empty();
             }
                                     
             template <storm::dd::DdType DdType, typename ValueType>
-            MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
-                STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
+            MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::abstract() {
+                if (refinementPerformed) {
+                    currentGame = buildGame();
+                    refinementPerformed = true;
+                }
                 return *currentGame;
             }
             

src/storm/abstraction/prism/AbstractProgram.h

@@ -55,7 +55,7 @@ namespace storm {
                  *
                  * @return The abstract stochastic two player game.
                  */
-                MenuGame<DdType, ValueType> getAbstractGame();
+                MenuGame<DdType, ValueType> abstract();
                 
                 /*!
                  * Retrieves information about the abstraction.
@@ -142,6 +142,9 @@ namespace storm {
                 
                 // The current game-based abstraction.
                 std::unique_ptr<MenuGame<DdType, ValueType>> currentGame;
+                
+                // A flag storing whether a refinement was performed.
+                bool refinementPerformed;
             };
         }
     }

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -16,7 +16,7 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             storm::abstraction::MenuGame<DdType, ValueType> PrismMenuGameAbstractor<DdType, ValueType>::abstract() {
-                return abstractProgram.getAbstractGame();
+                return abstractProgram.abstract();
             }
             
             template <storm::dd::DdType DdType, typename ValueType>