added debug output and fixed some bugs

Former-commit-id: 8d2b7a4dd5

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -71,6 +71,7 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
                 STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
+                std::cout << "recomputing " << command.get() << std::endl;
                 
                 // Create a mapping from source state DDs to their distributions.
                 std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
@@ -171,6 +172,10 @@ namespace storm {
                 // Insert the new variables into the record of relevant source variables.
                 relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end());
                 std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
+                std::cout << "sorted!" << std::endl;
+                for (auto const& el : relevantPredicatesAndVariables.first) {
+                    std::cout << el.first.getName() << " // " << el.second << std::endl;
+                }
                 
                 // Do the same for every update.
                 for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
@@ -190,6 +195,7 @@ namespace storm {
                 STORM_LOG_TRACE("Building source state BDD.");
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
+                    std::cout << "size: " << ddInformation.predicateBdds.size() << " and index " << variableIndexPair.second << std::endl;
                     if (model.getBooleanValue(variableIndexPair.first)) {
                         result &= ddInformation.predicateBdds[variableIndexPair.second].first;
                     } else {
@@ -244,11 +250,17 @@ namespace storm {
             storm::dd::Bdd<DdType> AbstractCommand<DdType, ValueType>::computeMissingSourceStateIdentities() const {
                 auto relevantIt = relevantPredicatesAndVariables.first.begin();
                 auto relevantIte = relevantPredicatesAndVariables.first.end();
+                std::cout << "the size is " << relevantPredicatesAndVariables.first.size() << std::endl;
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) {
                     if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
+                        std::cout << (relevantIt == relevantIte) << std::endl;
+                        std::cout << relevantIt->second << " vs " << predicateIndex << std::endl;
+                        std::cout << "multiplying identity " << predicateIndex << std::endl;
                         result &= ddInformation.predicateIdentities[predicateIndex];
+                    } else {
+                        ++relevantIt;
                     }
                 }
                 return result;

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -68,23 +68,34 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+                std::cout << "refining!" << std::endl;
+
                 // Add the predicates to the global list of predicates.
                 uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
                 expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());
                 
+                // Create DD variables and some auxiliary data structures for the new predicates.
+                for (auto const& predicate : predicates) {
+                    ddInformation.addPredicate(predicate);
+                }
+
                 // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors.
                 std::vector<uint_fast64_t> newPredicateIndices;
-                for (uint_fast64_t index = firstNewPredicateIndex; expressionInformation.predicates.size(); ++index) {
+                for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.predicates.size(); ++index) {
                     newPredicateIndices.push_back(index);
                 }
                 
+                std::cout << "refining modules" << std::endl;
                 // Refine all abstract modules.
                 for (auto& module : modules) {
                     module.refine(newPredicateIndices);
                 }
                 
+                std::cout << "refining initial" << std::endl;
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(newPredicateIndices);
+                
+                std::cout << "done " << std::endl;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -97,6 +108,8 @@ namespace storm {
                     return lastAbstractAdd;
                 }
                 
+                std::cout << "abstr DD new " << std::endl;
+                
                 // Otherwise, we remember that the abstract BDD changed and perform a reachability analysis.
                 lastAbstractBdd = gameBdd.first;
 
@@ -106,10 +119,14 @@ namespace storm {
                     variablesToAbstract.insert(ddInformation.optionDdVariables[index].first);
                 }
 
+                std::cout << "reachability... " << std::endl;
+                
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
 
+                std::cout << "done " << std::endl;
+                
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
                 deadlockStates = reachableStates && !deadlockStates;

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -26,7 +26,12 @@ TEST(PrismMenuGame, CommandAbstractionTest) {
     storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
     storm::dd::Add<storm::dd::DdType::CUDD> abstraction = abstractProgram.getAbstractAdd();
-    abstraction.exportToDot("abstr.dot");
+    abstraction.exportToDot("abstr1.dot");
+    
+    abstractProgram.refine({manager.getVariableExpression("s") == manager.integer(7)});
+    abstraction = abstractProgram.getAbstractAdd();
+    abstraction.exportToDot("abstr2.dot");
+    
 }
 
 #endif