From 422a31740738c6cd6011965d542b98d0a99d4fce Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 12 Aug 2014 23:12:12 +0200 Subject: [PATCH] Made the OptimalSCC algorithm MUCH faster. Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp. Former-commit-id: 77ba352a295faff6ff23ef3f83cdf4c7ff285d54 --- .../AtomicPropositionLabelingParser.cpp | 23 ++++---- src/parser/SparseStateRewardParser.cpp | 17 +++--- ...onNondeterministicLinearEquationSolver.cpp | 56 +++++++++++++------ 3 files changed, 60 insertions(+), 36 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 0dac9a8c9..dffdd030a 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -29,8 +29,8 @@ namespace storm { // Open the given file. if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process."; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."); + throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."; } MappedFile file(filename.c_str()); @@ -68,10 +68,10 @@ namespace storm { // If #DECLARATION or #END have not been found, the file format is wrong. if (!(foundDecl && foundEnd)) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted."); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive)."); if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive)."; } @@ -100,8 +100,8 @@ namespace storm { if (cnt >= sizeof(proposition)) { // if token is longer than our buffer, the following strncpy code might get risky... - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found."); - throw storm::exceptions::WrongFormatException(); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."; } else if (cnt > 0) { @@ -127,6 +127,7 @@ namespace storm { uint_fast64_t state = 0; uint_fast64_t lastState = (uint_fast64_t)-1; + uint_fast64_t const startIndexComparison = lastState; cnt = 0; // Now parse the assignments of labels to nodes. @@ -137,9 +138,9 @@ namespace storm { state = checked_strtol(buf, &buf); // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). - if(state <= lastState && lastState != (uint_fast64_t)-1) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). State " << state << " was found but has already been read or skipped previously."); - throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + if (state <= lastState && lastState != startIndexComparison) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."; } while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { @@ -159,8 +160,8 @@ namespace storm { // Has the label been declared in the header? if(!labeling.containsAtomicProposition(proposition)) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition" << proposition << " was found but not declared."); - throw storm::exceptions::WrongFormatException(); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."; } labeling.addAtomicPropositionToState(proposition, state); buf += cnt; diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 679bb5e7e..e707dbe3b 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -4,7 +4,7 @@ * Created on: 23.12.2012 * Author: Christian Dehnert */ - +#include #include "src/parser/SparseStateRewardParser.h" #include "src/exceptions/WrongFormatException.h" @@ -37,6 +37,7 @@ namespace storm { // Now parse state reward assignments. uint_fast64_t state = 0; uint_fast64_t lastState = (uint_fast64_t)-1; + uint_fast64_t const startIndexComparison = lastState; double reward; // Iterate over states. @@ -47,21 +48,21 @@ namespace storm { // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index). - if(state <= lastState && lastState != (uint_fast64_t)-1) { - LOG4CPLUS_ERROR(logger, "State " << state << " was found but has already been read or skipped previously."); - throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + if (state <= lastState && lastState != startIndexComparison) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."; } if(stateCount <= state) { - LOG4CPLUS_ERROR(logger, "Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states."); - throw storm::exceptions::OutOfRangeException() << "Found reward for a state of an invalid index \"" << state << "\""; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states."); + throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\""; } reward = checked_strtod(buf, &buf); if (reward < 0.0) { - LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\"."); - throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value."; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\"."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State reward file specifies illegal reward value."; } stateRewards[state] = reward; diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index e9d0222ea..4955797ed 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -80,7 +80,7 @@ namespace storm { bool const useGpu = sccIndexIt->first; storm::storage::StateBlock const& scc = sccIndexIt->second; - // Generate a submatrix + // Generate a sub matrix storm::storage::BitVector subMatrixIndices(A.getColumnCount(), scc.cbegin(), scc.cend()); storm::storage::SparseMatrix sccSubmatrix = A.getSubmatrix(true, subMatrixIndices, subMatrixIndices); std::vector sccSubB(sccSubmatrix.getRowCount()); @@ -97,7 +97,7 @@ namespace storm { std::vector sccSubNondeterministicChoiceIndices(sccSubmatrix.getColumnCount() + 1); sccSubNondeterministicChoiceIndices.at(0) = 0; - // Preprocess all dependent states + // Pre-process all dependent states // Remove outgoing transitions and create the ChoiceIndices uint_fast64_t innerIndex = 0; uint_fast64_t outerIndex = 0; @@ -135,8 +135,7 @@ namespace storm { localIterations = 0; if (minimize) { result = basicValueIteration_mvReduce_uint64_double_minimize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); - } - else { + } else { result = basicValueIteration_mvReduce_uint64_double_maximize(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations); } LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU."); @@ -276,13 +275,24 @@ namespace storm { storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]]; tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend()); - for (size_t j = startIndex + 1; j < i; ++j) { - storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; - std::vector::iterator const middleIterator = tempGroups.end(); - tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); - std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); + if (((startIndex + 1) + 80) >= i) { + size_t lastSize = 0; + for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) { + storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; + lastSize = tempGroups.size(); + tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); + std::vector::iterator middleIterator = tempGroups.begin(); + std::advance(middleIterator, lastSize); + std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); + } + } else { + // Use std::sort + for (size_t j = startIndex + 1; j < i; ++j) { + storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; + tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); + } + std::sort(tempGroups.begin(), tempGroups.end()); } - result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend()))); } else { // Only one group, copy construct. @@ -318,13 +328,25 @@ namespace storm { storm::storage::StateBlock const& scc_first = sccDecomposition[topologicalSort[startIndex]]; tempGroups.insert(tempGroups.cend(), scc_first.cbegin(), scc_first.cend()); - for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) { - storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; - std::vector::iterator const middleIterator = tempGroups.end(); - tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); - std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); - } - + // For set counts <= 80, Inplace Merge is faster + if (((startIndex + 1) + 80) >= topologicalSortSize) { + size_t lastSize = 0; + for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) { + storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; + lastSize = tempGroups.size(); + tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); + std::vector::iterator middleIterator = tempGroups.begin(); + std::advance(middleIterator, lastSize); + std::inplace_merge(tempGroups.begin(), middleIterator, tempGroups.end()); + } + } else { + // Use std::sort + for (size_t j = startIndex + 1; j < topologicalSort.size(); ++j) { + storm::storage::StateBlock const& scc = sccDecomposition[topologicalSort[j]]; + tempGroups.insert(tempGroups.cend(), scc.cbegin(), scc.cend()); + } + std::sort(tempGroups.begin(), tempGroups.end()); + } result.push_back(std::make_pair(true, storm::storage::StateBlock(boost::container::ordered_unique_range, tempGroups.cbegin(), tempGroups.cend()))); } else {