From eaf01ab443aed1a6b9a3cecaa84bce2dab2c9859 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 31 May 2018 22:18:54 +0200
Subject: [PATCH] bugfix

---
 .../abstraction/ValidBlockAbstractor.cpp      | 32 ++++++++++++++-----
 src/storm/abstraction/ValidBlockAbstractor.h  |  2 +-
 .../abstraction/prism/CommandAbstractor.cpp   |  2 +-
 3 files changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/storm/abstraction/ValidBlockAbstractor.cpp b/src/storm/abstraction/ValidBlockAbstractor.cpp
index 16364b156..bf213964d 100644
--- a/src/storm/abstraction/ValidBlockAbstractor.cpp
+++ b/src/storm/abstraction/ValidBlockAbstractor.cpp
@@ -5,6 +5,7 @@
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/utility/solver.h"
+#include "storm/utility/Stopwatch.h"
 
 namespace storm {
     namespace abstraction {
@@ -68,25 +69,39 @@ namespace storm {
         template <storm::dd::DdType DdType>
         void ValidBlockAbstractor<DdType>::recomputeValidBlocks() {
             storm::dd::Bdd<DdType> newValidBlocks = abstractionInformation.get().getDdManager().getBddOne();
-            
+
             for (uint64_t blockIndex = 0; blockIndex < localExpressionInformation.getNumberOfBlocks(); ++blockIndex) {
                 std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
                 
                 // If the size of the block changed, we need to add the appropriate variables and recompute the solution.
                 if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) {
-                    recomputeValidBlockForPredicateBlock(blockIndex);
+                    recomputeValidBlocksForPredicateBlock(blockIndex);
                 }
-                
-                newValidBlocks &= validBlocksForPredicateBlocks[blockIndex];
             }
             
-            validBlocks = newValidBlocks;
+            // Now compute the conjunction of all blocks.
+            std::vector<storm::dd::Bdd<DdType>> blocks = validBlocksForPredicateBlocks;
+            std::vector<storm::dd::Bdd<DdType>> newBlocks;
+            while (blocks.size() > 1) {
+                storm::utility::Stopwatch conj(true);
+                for (uint64_t blockIndex = 0; blockIndex < blocks.size(); ++blockIndex) {
+                    if (blockIndex < localExpressionInformation.getNumberOfBlocks() - 1) {
+                        newBlocks.emplace_back(blocks[blockIndex] && blocks[blockIndex + 1]);
+                    } else {
+                        newBlocks.emplace_back(blocks[blockIndex]);
+                    }
+                }
+                conj.stop();
+
+                std::swap(blocks, newBlocks);
+            }
+            
+            validBlocks = blocks.front();
         }
         
         template <storm::dd::DdType DdType>
-        void ValidBlockAbstractor<DdType>::recomputeValidBlockForPredicateBlock(uint64_t blockIndex) {
+        void ValidBlockAbstractor<DdType>::recomputeValidBlocksForPredicateBlock(uint64_t blockIndex) {
             std::set<uint64_t> const& predicateBlock = localExpressionInformation.getExpressionBlock(blockIndex);
-            
             std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newVariables = this->getAbstractionInformation().declareNewVariables(relevantVariablesAndPredicates[blockIndex], predicateBlock);
             for (auto const& element : newVariables) {
                 smtSolvers[blockIndex]->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
@@ -121,7 +136,8 @@ namespace storm {
         template <storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> ValidBlockAbstractor<DdType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, uint64_t blockIndex) const {
             storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
-            for (auto const& variableIndexPair : relevantVariablesAndPredicates[blockIndex]) {
+            for (auto variableIndexPairIt = relevantVariablesAndPredicates[blockIndex].rbegin(), variableIndexPairIte = relevantVariablesAndPredicates[blockIndex].rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) {
+                auto const& variableIndexPair = *variableIndexPairIt;
                 if (model.getBooleanValue(variableIndexPair.first)) {
                     result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
                 } else {
diff --git a/src/storm/abstraction/ValidBlockAbstractor.h b/src/storm/abstraction/ValidBlockAbstractor.h
index 33f7fb590..145638def 100644
--- a/src/storm/abstraction/ValidBlockAbstractor.h
+++ b/src/storm/abstraction/ValidBlockAbstractor.h
@@ -44,7 +44,7 @@ namespace storm {
             /*!
              * Recomputed the valid blocks for the given predicate block.
              */
-            void recomputeValidBlockForPredicateBlock(uint64_t blockIndex);
+            void recomputeValidBlocksForPredicateBlock(uint64_t blockIndex);
             
             /*!
              * Retrieves the abstraction information object.
diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp
index 39d95845b..26a3d2c69 100644
--- a/src/storm/abstraction/prism/CommandAbstractor.cpp
+++ b/src/storm/abstraction/prism/CommandAbstractor.cpp
@@ -344,7 +344,7 @@ namespace storm {
                     
                     // We now compute how many variables we need to encode the choices. We add one to the maximal number of
                     // choices to account for a possible transition to a bottom state.
-                    uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0))));
+                    uint_fast64_t numberOfVariablesNeeded = maximalNumberOfChoices > 1 ? static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)))) : 0;
                     
                     // Finally, build overall result.
                     storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();