From fa14b993e476e7e77a6640e5a9d27cb4735e9785 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 1 Jun 2018 08:37:12 +0200 Subject: [PATCH] fixing valid block abstractor --- .../abstraction/ValidBlockAbstractor.cpp | 21 +++---------------- 1 file changed, 3 insertions(+), 18 deletions(-) diff --git a/src/storm/abstraction/ValidBlockAbstractor.cpp b/src/storm/abstraction/ValidBlockAbstractor.cpp index bf213964d..dbc84dd13 100644 --- a/src/storm/abstraction/ValidBlockAbstractor.cpp +++ b/src/storm/abstraction/ValidBlockAbstractor.cpp @@ -77,26 +77,11 @@ namespace storm { if (relevantVariablesAndPredicates[blockIndex].size() < predicateBlock.size()) { recomputeValidBlocksForPredicateBlock(blockIndex); } + + newValidBlocks &= validBlocksForPredicateBlocks[blockIndex]; } - // Now compute the conjunction of all blocks. - std::vector> blocks = validBlocksForPredicateBlocks; - std::vector> 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(); + validBlocks = newValidBlocks; } template