From 692587495fcec5c14ec556c56b852ffcdca8f0fa Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 7 Apr 2018 11:22:43 +0200
Subject: [PATCH] fixed bug in quotient extraction

---
 .../storage/dd/bisimulation/QuotientExtractor.cpp      | 10 ++++++++--
 src/storm/storage/dd/cudd/InternalCuddBdd.cpp          |  2 +-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
index a4c3b014a..1ba224331 100644
--- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
+++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp
@@ -1006,7 +1006,10 @@ namespace storm {
                     STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
 
                     storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
-                    storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates;
+                    
+                    std::set<storm::expressions::Variable> blockPrimeAndNondeterminismVariables = model.getNondeterminismVariables();
+                    blockPrimeAndNondeterminismVariables.insert(blockPrimeVariableSet.begin(), blockPrimeVariableSet.end());
+                    storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeAndNondeterminismVariables) && reachableStates;
                     
                     start = std::chrono::high_resolution_clock::now();
                     std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<DdType, ValueType>> quotientRewardModels;
@@ -1127,7 +1130,10 @@ namespace storm {
                     STORM_LOG_INFO("Quotient transition matrix extracted in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
                     
                     storm::dd::Bdd<DdType> quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero();
-                    storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(model.getColumnVariables()) && reachableStates;
+                    
+                    std::set<storm::expressions::Variable> columnAndNondeterminismVariables = model.getColumnVariables();
+                    columnAndNondeterminismVariables.insert(model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end());
+                    storm::dd::Bdd<DdType> deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(columnAndNondeterminismVariables) && reachableStates;
                     
                     start = std::chrono::high_resolution_clock::now();
                     std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<DdType, ValueType>> quotientRewardModels;
diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
index 5fc12e567..b69040372 100644
--- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
+++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp
@@ -294,7 +294,7 @@ namespace storm {
             } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
                 return;
             }
-            
+                        
             // If we are at the maximal level, the value to be set is stored as a constant in the DD.
             if (currentRowLevel == maxLevel) {
                 result.set(currentRowOffset, true);