From c27580defc56799b0193dcecae0571ef9ba913ad Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 22 Nov 2016 21:05:31 +0100
Subject: [PATCH] bugfix in flattening of modules

---
 .../abstraction/prism/AbstractProgram.cpp     | 21 +++++++++++++++++--
 src/storm/storage/prism/Program.cpp           |  8 +++----
 2 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp
index 1088a703f..e108945e5 100644
--- a/src/storm/abstraction/prism/AbstractProgram.cpp
+++ b/src/storm/abstraction/prism/AbstractProgram.cpp
@@ -24,6 +24,8 @@ namespace storm {
     namespace abstraction {
         namespace prism {
             
+#undef LOCAL_DEBUG
+            
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
                                                                 std::vector<storm::expressions::Expression> const& initialPredicates,
@@ -180,14 +182,30 @@ namespace storm {
 #ifdef LOCAL_DEBUG
                 std::cout << "command index " << commandIndex << std::endl;
                 std::cout << program.get() << std::endl;
+                
+                for (auto stateValue : pivotState.template toAdd<ValueType>()) {
+                    std::stringstream stateName;
+                    stateName << "\tpl1_";
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        std::cout << "var " << var.getName() << std::endl;
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    std::cout << "pivot is " << stateName.str() << std::endl;
+                }
 #endif
                 storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
                 storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
 #ifdef LOCAL_DEBUG
                 player1Choice.template toAdd<ValueType>().exportToDot("pl1choice_ref.dot");
                 std::cout << concreteCommand << std::endl;
+                
+                (currentGame->getTransitionMatrix() * player1Choice.template toAdd<ValueType>()).exportToDot("cuttrans.dot");
 #endif
-
+                
                 // Check whether there are bottom states in the game and whether one of the choices actually picks the
                 // bottom state as the successor.
                 bool buttomStateSuccessor = false;
@@ -249,7 +267,6 @@ namespace storm {
                             for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
                                 if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
                                     // Now we know the point of the deviation (command, update, predicate).
-                                    std::cout << "pred: " << abstractionInformation.getPredicateByIndex(predicateIndex) << " and update " << concreteCommand.getUpdate(updateIndex) << std::endl;
                                     newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
                                     break;
                                 }
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index 148f666a4..75fe1181f 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -1504,12 +1504,12 @@ namespace storm {
                             if (seenIt == seenCommandCombinations.end()) {
                                 newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second, commandCombination));
                                 seenCommandCombinations.insert(commandCombinationIndices);
+
+                                // Move the counters appropriately.
+                                ++nextCommandIndex;
+                                nextUpdateIndex += newCommands.back().getNumberOfUpdates();
                             }
                             
-                            // Move the counters appropriately.
-                            ++nextCommandIndex;
-                            nextUpdateIndex += newCommands.back().getNumberOfUpdates();
-                            
                             movedAtLeastOneIterator = false;
                             for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
                                 ++iterators[index];