diff --git a/CMakeLists.txt b/CMakeLists.txt index 314824cf7..4b74f4317 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -103,11 +103,9 @@ if(CMAKE_COMPILER_IS_GNUCC) set(STORM_COMPILED_BY "GCC") # Set standard flags for GCC set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic -DBOOST_RESULT_OF_USE_TR1") - # -Werror is atm removed as this gave some problems with existing code - # May be re-set later - # (Thomas Heinemann, 2012-12-21) - + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -Wall -pedantic") + # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") @@ -125,6 +123,8 @@ elseif(MSVC) add_definitions(/D_VARIADIC_MAX=10) # Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max add_definitions(/DNOMINMAX) + # required for using boost's transform iterator + add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE) # since nobody cares at the moment add_definitions(/wd4250) @@ -153,10 +153,9 @@ else(CLANG) set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++") endif() - set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE -ftemplate-depth=1024") - - set (CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -g") - + add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE) + set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-unused-variable -ftemplate-depth=1024") + # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp index 702cce376..3383f3317 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/utility/graph.h" #include "src/exceptions/IllegalFunctionCallException.h" @@ -11,6 +12,11 @@ namespace storm { namespace storage { + namespace { + static std::chrono::high_resolution_clock::duration probabilityRefineTime; + static std::chrono::high_resolution_clock::duration qualitativeRefineTime; + } + template std::size_t DeterministicModelStrongBisimulationDecomposition::Block::blockId = 0; @@ -30,15 +36,15 @@ namespace storm { std::cout << "begin: " << this->begin << " and end: " << this->end << " (number of states: " << this->getNumberOfStates() << ")" << std::endl; std::cout << "states:" << std::endl; for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << partition.states[index] << " "; + std::cout << partition.statesAndValues[index].first << " "; } std::cout << std::endl << "original: " << std::endl; for (storm::storage::sparse::state_type index = this->getOriginalBegin(); index < this->end; ++index) { - std::cout << partition.states[index] << " "; + std::cout << partition.statesAndValues[index].first << " "; } std::cout << std::endl << "values:" << std::endl; for (storm::storage::sparse::state_type index = this->begin; index < this->end; ++index) { - std::cout << std::setprecision(3) << partition.values[index] << " "; + std::cout << std::setprecision(3) << partition.statesAndValues[index].second << " "; } std::cout << std::endl; } @@ -245,28 +251,28 @@ namespace storm { } template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { + DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) { // Create the block and give it an iterator to itself. typename std::list::iterator it = blocks.emplace(this->blocks.end(), 0, numberOfStates, nullptr, nullptr); it->setIterator(it); // Set up the different parts of the internal structure. for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { - states[state] = state; + statesAndValues[state] = std::make_pair(state, storm::utility::zero()); positions[state] = state; stateToBlockMapping[state] = &blocks.back(); } } template - DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates), values(numberOfStates) { + DeterministicModelStrongBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label) : stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates) { typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr); Block& firstBlock = *firstIt; firstBlock.setIterator(firstIt); storm::storage::sparse::state_type position = 0; for (auto state : prob0States) { - states[position] = state; + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); positions[state] = position; stateToBlockMapping[state] = &firstBlock; ++position; @@ -278,7 +284,7 @@ namespace storm { secondBlock.setIterator(secondIt); for (auto state : prob1States) { - states[position] = state; + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); positions[state] = position; stateToBlockMapping[state] = &secondBlock; ++position; @@ -291,7 +297,7 @@ namespace storm { storm::storage::BitVector otherStates = ~(prob0States | prob1States); for (auto state : otherStates) { - states[position] = state; + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); positions[state] = position; stateToBlockMapping[state] = &thirdBlock; ++position; @@ -300,18 +306,16 @@ namespace storm { template void DeterministicModelStrongBisimulationDecomposition::Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { - std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]); - std::swap(this->values[this->positions[state1]], this->values[this->positions[state2]]); + std::swap(this->statesAndValues[this->positions[state1]], this->statesAndValues[this->positions[state2]]); std::swap(this->positions[state1], this->positions[state2]); } - + template void DeterministicModelStrongBisimulationDecomposition::Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { - storm::storage::sparse::state_type state1 = this->states[position1]; - storm::storage::sparse::state_type state2 = this->states[position2]; + storm::storage::sparse::state_type state1 = this->statesAndValues[position1].first; + storm::storage::sparse::state_type state2 = this->statesAndValues[position2].first; - std::swap(this->states[position1], this->states[position2]); - std::swap(this->values[position1], this->values[position2]); + std::swap(this->statesAndValues[position1], this->statesAndValues[position2]); this->positions[state1] = position2; this->positions[state2] = position1; @@ -329,38 +333,33 @@ namespace storm { template storm::storage::sparse::state_type const& DeterministicModelStrongBisimulationDecomposition::Partition::getState(storm::storage::sparse::state_type position) const { - return this->states[position]; + return this->statesAndValues[position].first; } template ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValue(storm::storage::sparse::state_type state) const { - return this->values[this->positions[state]]; + return this->statesAndValues[this->positions[state]].second; } template ValueType const& DeterministicModelStrongBisimulationDecomposition::Partition::getValueAtPosition(storm::storage::sparse::state_type position) const { - return this->values[position]; + return this->statesAndValues[position].second; } template void DeterministicModelStrongBisimulationDecomposition::Partition::setValue(storm::storage::sparse::state_type state, ValueType value) { - this->values[this->positions[state]] = value; - } - - template - std::vector& DeterministicModelStrongBisimulationDecomposition::Partition::getValues() { - return this->values; + this->statesAndValues[this->positions[state]].second = value; } template void DeterministicModelStrongBisimulationDecomposition::Partition::increaseValue(storm::storage::sparse::state_type state, ValueType value) { - this->values[this->positions[state]] += value; + this->statesAndValues[this->positions[state]].second += value; } template - void DeterministicModelStrongBisimulationDecomposition::Partition::updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator last) { + void DeterministicModelStrongBisimulationDecomposition::Partition::updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator last) { for (; first != last; ++first) { - this->stateToBlockMapping[*first] = █ + this->stateToBlockMapping[first->first] = █ } } @@ -380,56 +379,61 @@ namespace storm { } template - std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) { - return this->states.begin() + block.getBegin(); + typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) { + return this->statesAndValues.begin() + block.getBegin(); } template - std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfStates(Block const& block) { - return this->states.begin() + block.getEnd(); + typename std::vector>::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) { + return this->statesAndValues.begin() + block.getEnd(); } template - std::vector::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfStates(Block const& block) const { - return this->states.begin() + block.getBegin(); - } - - template - std::vector::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfStates(Block const& block) const { - return this->states.begin() + block.getEnd(); + typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBegin(Block const& block) const { + return this->statesAndValues.begin() + block.getBegin(); } template - typename std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getBeginOfValues(Block const& block) { - return this->values.begin() + block.getBegin(); - } - - template - typename std::vector::iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEndOfValues(Block const& block) { - return this->values.begin() + block.getEnd(); + typename std::vector>::const_iterator DeterministicModelStrongBisimulationDecomposition::Partition::getEnd(Block const& block) const { + return this->statesAndValues.begin() + block.getEnd(); } template typename DeterministicModelStrongBisimulationDecomposition::Block& DeterministicModelStrongBisimulationDecomposition::Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { - // FIXME: this could be improved by splitting off the smaller of the two resulting blocks. - // In case one of the resulting blocks would be empty, we simply return the current block and do not create // a new one. if (position == block.getBegin() || position == block.getEnd()) { return block; } + // We only split off the smaller of the two resulting blocks so we don't have to update large parts of the + // block mapping. + bool insertAfterCurrent = false; + if ((block.getBegin() + position) > ((block.getEnd() - block.getBegin()) / 2)) { + // If the splitting position is far in the back, we create the new block after the one we are splitting. + insertAfterCurrent = true; + } + // Actually create the new block and insert it at the correct position. - typename std::list::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); + typename std::list::iterator selfIt; + if (insertAfterCurrent) { + selfIt = this->blocks.emplace(block.hasNextBlock() ? block.getNextIterator() : this->blocks.end(), position, block.getEnd(), &block, block.getNextBlockPointer(), block.getLabelPtr()); + } else { + selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr()); + } selfIt->setIterator(selfIt); Block& newBlock = *selfIt; - // Make the current block end at the given position. - block.setBegin(position); + // Resize the current block appropriately. + if (insertAfterCurrent) { + block.setEnd(position); + } else { + block.setBegin(position); + } // Update the mapping of the states in the newly created block. - for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) { - stateToBlockMapping[*it] = &newBlock; + for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { + stateToBlockMapping[it->first] = &newBlock; } return newBlock; @@ -451,8 +455,8 @@ namespace storm { newBlock.setIterator(it); // Update the mapping of the states in the newly created block. - for (auto it = this->getBeginOfStates(newBlock), ite = this->getEndOfStates(newBlock); it != ite; ++it) { - stateToBlockMapping[*it] = &newBlock; + for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) { + stateToBlockMapping[it->first] = &newBlock; } return *it; @@ -464,20 +468,20 @@ namespace storm { Block& block = *blockIterator; // Sort the range of the block such that all states that have the label are moved to the front. - std::sort(this->getBeginOfStates(block), this->getEndOfStates(block), [&statesWithLabel] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statesWithLabel.get(a) && !statesWithLabel.get(b); } ); + std::sort(this->getBegin(block), this->getEnd(block), [&statesWithLabel] (std::pair const& a, std::pair const& b) { return statesWithLabel.get(a.first) && !statesWithLabel.get(b.first); } ); // Update the positions vector. storm::storage::sparse::state_type position = block.getBegin(); - for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) { - this->positions[*stateIt] = position; + for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt, ++position) { + this->positions[stateIt->first] = position; } // Now we can find the first position in the block that does not have the label and create new blocks. - std::vector::iterator it = std::find_if(this->getBeginOfStates(block), this->getEndOfStates(block), [&] (storm::storage::sparse::state_type const& a) { return !statesWithLabel.get(a); }); + typename std::vector>::iterator it = std::find_if(this->getBegin(block), this->getEnd(block), [&] (std::pair const& a) { return !statesWithLabel.get(a.first); }); // If not all the states agreed on the validity of the label, we need to split the block. - if (it != this->getBeginOfStates(block) && it != this->getEndOfStates(block)) { - auto cutPoint = std::distance(this->states.begin(), it); + if (it != this->getBegin(block) && it != this->getEnd(block)) { + auto cutPoint = std::distance(this->statesAndValues.begin(), it); this->splitBlock(block, cutPoint); } else { // Otherwise, we simply proceed to the next block. @@ -492,8 +496,8 @@ namespace storm { } template - std::vector& DeterministicModelStrongBisimulationDecomposition::Partition::getStates() { - return this->states; + std::vector>& DeterministicModelStrongBisimulationDecomposition::Partition::getStatesAndValues() { + return this->statesAndValues; } template @@ -504,14 +508,14 @@ namespace storm { template bool DeterministicModelStrongBisimulationDecomposition::Partition::check() const { for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { - if (this->states[this->positions[state]] != state) { + if (this->statesAndValues[this->positions[state]].first != state) { assert(false); } } for (auto const& block : this->blocks) { assert(block.check()); - for (auto stateIt = this->getBeginOfStates(block), stateIte = this->getEndOfStates(block); stateIt != stateIte; ++stateIt) { - if (this->stateToBlockMapping[*stateIt] != &block) { + for (auto stateIt = this->getBegin(block), stateIte = this->getEnd(block); stateIt != stateIte; ++stateIt) { + if (this->stateToBlockMapping[stateIt->first] != &block) { assert(false); } } @@ -525,8 +529,8 @@ namespace storm { block.print(*this); } std::cout << "states in partition" << std::endl; - for (auto const& state : states) { - std::cout << state << " "; + for (auto const& stateValue : statesAndValues) { + std::cout << stateValue.first << " "; } std::cout << std::endl << "positions: " << std::endl; for (auto const& index : positions) { @@ -695,75 +699,94 @@ namespace storm { template void DeterministicModelStrongBisimulationDecomposition::partitionRefinement(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, Partition& partition, bool buildQuotient) { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); - + // Initially, all blocks are potential splitter, so we insert them in the splitterQueue. + std::chrono::high_resolution_clock::time_point refinementStart = std::chrono::high_resolution_clock::now(); std::deque splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (Block& a) { splitterQueue.push_back(&a); }); // Then perform the actual splitting until there are no more splitters. while (!splitterQueue.empty()) { + std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); refinePartition(backwardTransitions, *splitterQueue.front(), partition, splitterQueue); splitterQueue.pop_front(); } - + std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; + // Now move the states from the internal partition into their final place in the decomposition. We do so in // a way that maintains the block IDs as indices. + std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now(); this->blocks.resize(partition.size()); for (auto const& block : partition.getBlocks()) { // We need to sort the states to allow for rapid construction of the blocks. - std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block)); - this->blocks[block.getId()] = block_type(partition.getBeginOfStates(block), partition.getEndOfStates(block), true); + std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.first < b.first; }); + + // Convert the state-value-pairs to states only. + auto lambda = [] (std::pair const& a) -> storm::storage::sparse::state_type { return a.first; }; + this->blocks[block.getId()] = block_type(boost::make_transform_iterator(partition.getBegin(block), lambda), boost::make_transform_iterator(partition.getEnd(block), lambda), true); } // If we are required to build the quotient model, do so now. if (buildQuotient) { this->buildQuotient(model, partition); } - + + std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; std::chrono::high_resolution_clock::duration totalTime = std::chrono::high_resolution_clock::now() - totalStart; if (storm::settings::generalSettings().isShowStatisticsSet()) { - std::cout << "Computed bisimulation quotient in " << std::chrono::duration_cast(totalTime).count() << "ms." << std::endl; + std::cout << std::endl; + std::cout << "Time breakdown:" << std::endl; + std::cout << " * time for partitioning: " << std::chrono::duration_cast(refinementTime).count() << "ms" << std::endl; + std::cout << " * time for qualitative refinement: " << std::chrono::duration_cast(qualitativeRefineTime).count() << "ms" << std::endl; + std::cout << " * time for probability refinement: " << std::chrono::duration_cast(probabilityRefineTime).count() << "ms" << std::endl; + std::cout << " * time for extraction: " << std::chrono::duration_cast(extractionTime).count() << "ms" << std::endl; + std::cout << "------------------------------------------" << std::endl; + std::cout << " * total time: " << std::chrono::duration_cast(totalTime).count() << "ms" << std::endl; + std::cout << std::endl; } } template void DeterministicModelStrongBisimulationDecomposition::refineBlockProbabilities(Block& block, Partition& partition, std::deque& splitterQueue) { + std::chrono::high_resolution_clock::time_point probabilityRefineStart = std::chrono::high_resolution_clock::now(); + // First, we simplify all the values. For most types this does not change anything, but for rational // functions, this achieves a canonicity that is used for sorting the rational functions later. - for (auto probabilityIt = partition.getBeginOfValues(block), probabilityIte = partition.getEndOfValues(block); probabilityIt != probabilityIte; ++probabilityIt) { - storm::utility::simplify(*probabilityIt); + for (auto probabilityIt = partition.getBegin(block), probabilityIte = partition.getEnd(block); probabilityIt != probabilityIte; ++probabilityIt) { + storm::utility::simplify(probabilityIt->second); } - + // Sort the states in the block based on their probabilities. - std::sort(partition.getBeginOfStates(block), partition.getEndOfStates(block), [&partition] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return partition.getValue(a) < partition.getValue(b); } ); - - // FIXME: This can probably be done more efficiently. - std::sort(partition.getBeginOfValues(block), partition.getEndOfValues(block)); + std::sort(partition.getBegin(block), partition.getEnd(block), [] (std::pair const& a, std::pair const& b) { return a.second < b.second; } ); // Update the positions vector. storm::storage::sparse::state_type position = block.getBegin(); - for (auto stateIt = partition.getBeginOfStates(block), stateIte = partition.getEndOfStates(block); stateIt != stateIte; ++stateIt, ++position) { - partition.setPosition(*stateIt, position); + for (auto stateIt = partition.getBegin(block), stateIte = partition.getEnd(block); stateIt != stateIte; ++stateIt, ++position) { + partition.setPosition(stateIt->first, position); } // Finally, we need to scan the ranges of states that agree on the probability. - storm::storage::sparse::state_type beginIndex = block.getBegin(); - storm::storage::sparse::state_type currentIndex = beginIndex; - storm::storage::sparse::state_type endIndex = block.getEnd(); + typename std::vector>::const_iterator begin = partition.getBegin(block); + typename std::vector>::const_iterator current = begin; + typename std::vector>::const_iterator end = partition.getEnd(block) - 1; + storm::storage::sparse::state_type currentIndex = block.getBegin(); + + // Perform a sanity check that the smallest probability is still not zero. + STORM_LOG_ASSERT(!comparator.isZero(begin->second), "Probability to go to splitter must not be zero."); // Now we can check whether the block needs to be split, which is the case iff the probabilities for the // first and the last state are different. - while (!comparator.isEqual(partition.getValueAtPosition(beginIndex), partition.getValueAtPosition(endIndex - 1))) { + while (!comparator.isEqual(begin->second, end->second)) { // Now we scan for the first state in the block that disagrees on the probability value. // Note that we do not have to check currentIndex for staying within bounds, because we know the matching // state is within bounds. - ValueType const& currentValue = partition.getValueAtPosition(beginIndex); + ValueType const& currentValue = begin->second; - typename std::vector::const_iterator valueIterator = partition.getValues().begin() + beginIndex + 1; + ++begin; ++currentIndex; - while (currentIndex < endIndex && comparator.isEqual(*valueIterator, currentValue)) { - ++valueIterator; + while (begin != end && comparator.isEqual(begin->second, currentValue)) { + ++begin; ++currentIndex; } @@ -773,12 +796,14 @@ namespace storm { splitterQueue.push_back(&newBlock); newBlock.markAsSplitter(); } - beginIndex = currentIndex; - } - - for (auto index = currentIndex; index < endIndex - 1; ++index) { - STORM_LOG_ASSERT(comparator.isEqual(partition.getValueAtPosition(index + 1), partition.getValueAtPosition(index + 1)), "Expected equal probabilities after sorting block, but got '" << partition.getValueAtPosition(index) << "' and '" << partition.getValueAtPosition(index + 1) << "'."); + + for (auto it = partition.getBegin(newBlock), ite = partition.getEnd(newBlock) - 1; it != ite; ++it) { + STORM_LOG_ASSERT(comparator.isEqual(partition.getValueAtPosition(it->first), partition.getValueAtPosition((it + 1)->first)), "Expected equal probabilities after sorting block, but got '" << partition.getValueAtPosition(it->first) << "' and '" << partition.getValueAtPosition((it + 1)->first) << "'."); + } + } + + probabilityRefineTime += std::chrono::high_resolution_clock::now() - probabilityRefineStart; } template @@ -786,9 +811,10 @@ namespace storm { std::list predecessorBlocks; // Iterate over all states of the splitter and check its predecessors. + std::chrono::high_resolution_clock::time_point qualitativeRefineStart = std::chrono::high_resolution_clock::now(); storm::storage::sparse::state_type currentPosition = splitter.getBegin(); - for (auto stateIterator = partition.getBeginOfStates(splitter), stateIte = partition.getEndOfStates(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) { - storm::storage::sparse::state_type currentState = *stateIterator; + for (auto stateIterator = partition.getBegin(splitter), stateIte = partition.getEnd(splitter); stateIterator != stateIte; ++stateIterator, ++currentPosition) { + storm::storage::sparse::state_type currentState = stateIterator->first; uint_fast64_t elementsToSkip = 0; for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { @@ -852,8 +878,8 @@ namespace storm { } // Now we can traverse the list of states of the splitter whose predecessors we have not yet explored. - for (auto stateIterator = partition.getStates().begin() + splitter.getOriginalBegin(), stateIte = partition.getStates().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { - storm::storage::sparse::state_type currentState = *stateIterator; + for (auto stateIterator = partition.getStatesAndValues().begin() + splitter.getOriginalBegin(), stateIte = partition.getStatesAndValues().begin() + splitter.getMarkedPosition(); stateIterator != stateIte; ++stateIterator) { + storm::storage::sparse::state_type currentState = stateIterator->first; for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); @@ -905,6 +931,8 @@ namespace storm { } } + qualitativeRefineTime += std::chrono::high_resolution_clock::now() - qualitativeRefineStart; + // Finally, we walk through the blocks that have a transition to the splitter and split them using // probabilistic information. for (auto blockPtr : blocksToSplit) { diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.h b/src/storage/DeterministicModelStrongBisimulationDecomposition.h index 48360923f..c2fdec62e 100644 --- a/src/storage/DeterministicModelStrongBisimulationDecomposition.h +++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.h @@ -76,6 +76,7 @@ namespace storm { typedef typename std::list::iterator iterator; typedef typename std::list::const_iterator const_iterator; + // Creates a new block with the given begin and end. Block(storm::storage::sparse::state_type begin, storm::storage::sparse::state_type end, Block* prev, Block* next, std::shared_ptr const& label = nullptr); // Prints the block. @@ -284,30 +285,21 @@ namespace storm { // Retrieves the blocks of the partition. std::list& getBlocks(); - - // Retrieves the vector of all the states. - std::vector& getStates(); // Checks the partition for internal consistency. bool check() const; // Returns an iterator to the beginning of the states of the given block. - std::vector::iterator getBeginOfStates(Block const& block); + typename std::vector>::iterator getBegin(Block const& block); // Returns an iterator to the beginning of the states of the given block. - std::vector::iterator getEndOfStates(Block const& block); + typename std::vector>::iterator getEnd(Block const& block); // Returns an iterator to the beginning of the states of the given block. - std::vector::const_iterator getBeginOfStates(Block const& block) const; - - // Returns an iterator to the beginning of the states of the given block. - std::vector::const_iterator getEndOfStates(Block const& block) const; + typename std::vector>::const_iterator getBegin(Block const& block) const; // Returns an iterator to the beginning of the states of the given block. - typename std::vector::iterator getBeginOfValues(Block const& block); - - // Returns an iterator to the beginning of the states of the given block. - typename std::vector::iterator getEndOfValues(Block const& block); + typename std::vector>::const_iterator getEnd(Block const& block) const; // Swaps the positions of the two given states. void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2); @@ -340,13 +332,13 @@ namespace storm { void setValue(storm::storage::sparse::state_type state, ValueType value); // Retrieves the vector with the probabilities going into the current splitter. - std::vector& getValues(); + std::vector>& getStatesAndValues(); // Increases the value for the given state by the specified amount. void increaseValue(storm::storage::sparse::state_type state, ValueType value); // Updates the block mapping for the given range of states to the specified block. - void updateBlockMapping(Block& block, std::vector::iterator first, std::vector::iterator end); + void updateBlockMapping(Block& block, typename std::vector>::iterator first, typename std::vector>::iterator end); // Retrieves the first block of the partition. Block& getFirstBlock(); @@ -357,15 +349,12 @@ namespace storm { // A mapping of states to their blocks. std::vector stateToBlockMapping; - // A vector containing all the states. It is ordered in a special way such that the blocks only need to - // define their start/end indices. - std::vector states; + // A vector containing all the states and their values. It is ordered in a special way such that the + // blocks only need to define their start/end indices. + std::vector> statesAndValues; // This vector keeps track of the position of each state in the state vector. std::vector positions; - - // This vector stores the probabilities of going to the current splitter. - std::vector values; }; /*! diff --git a/src/storage/StronglyConnectedComponent.cpp b/src/storage/StronglyConnectedComponent.cpp index 6540a8acf..8661ebd0e 100644 --- a/src/storage/StronglyConnectedComponent.cpp +++ b/src/storage/StronglyConnectedComponent.cpp @@ -2,6 +2,10 @@ namespace storm { namespace storage { + StronglyConnectedComponent::StronglyConnectedComponent() : isTrivialScc(false) { + // Intentionally left empty. + } + void StronglyConnectedComponent::setIsTrivial(bool trivial) { this->isTrivialScc = trivial; } diff --git a/src/storage/StronglyConnectedComponent.h b/src/storage/StronglyConnectedComponent.h index 1a81742c9..dfbede4a9 100644 --- a/src/storage/StronglyConnectedComponent.h +++ b/src/storage/StronglyConnectedComponent.h @@ -14,7 +14,7 @@ namespace storm { */ class StronglyConnectedComponent : public StateBlock { public: - StronglyConnectedComponent() = default; + StronglyConnectedComponent(); StronglyConnectedComponent(StronglyConnectedComponent const& other) = default; #ifndef WINDOWS StronglyConnectedComponent(StronglyConnectedComponent&& other) = default; diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index 7029063ab..ae54f0b9b 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -118,7 +118,6 @@ namespace storm { } #endif - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { simplify(matrixEntry.getValue()); @@ -126,26 +125,29 @@ namespace storm { } template class ConstantsComparator; - template class ConstantsComparator; - template class ConstantsComparator; template double one(); template double zero(); template double infinity(); + template double simplify(double value); + + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + +#ifdef PARAMETRIC_SYSTEMS + template class ConstantsComparator; + template class ConstantsComparator; + template RationalFunction one(); template RationalFunction zero(); - + template Polynomial one(); template Polynomial zero(); - - template double simplify(double value); - template RationalFunction simplify(RationalFunction value); template RationalFunction& simplify(RationalFunction& value); template RationalFunction&& simplify(RationalFunction&& value); - template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); +#endif } } \ No newline at end of file diff --git a/src/utility/macros.h b/src/utility/macros.h index 8e2a3c5b2..539b6b268 100644 --- a/src/utility/macros.h +++ b/src/utility/macros.h @@ -9,15 +9,8 @@ extern log4cplus::Logger logger; /*! - * Define the macros STORM_LOG_ASSERT, STORM_LOG_DEBUG and STORM_LOG_TRACE. + * Define the macros STORM_LOG_DEBUG and STORM_LOG_TRACE. */ -#define STORM_LOG_ASSERT(cond, message) \ -{ \ - if (!(cond)) { \ - LOG4CPLUS_ERROR(logger, message); \ - assert(cond); \ - } \ -} while (false) #define STORM_LOG_DEBUG(message) \ { \ LOG4CPLUS_DEBUG(logger, message); \ @@ -27,6 +20,18 @@ extern log4cplus::Logger logger; LOG4CPLUS_TRACE(logger, message); \ } while (false) +// Define STORM_LOG_ASSERT which is only checked when NDEBUG is not set. +#ifndef NDEBUG +#define STORM_LOG_ASSERT(cond, message) \ +{ \ +if (!(cond)) { \ +LOG4CPLUS_ERROR(logger, message); \ +assert(cond); \ +} \ +} while (false) +#else +#define STORM_LOG_ASSERT(cond, message) +#endif // Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold. #define STORM_LOG_THROW(cond, exception, message) \ { \