From ffe63ea95d63b2bdcbf49573b0217acefcd28ba7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 29 Feb 2016 22:10:30 +0100 Subject: [PATCH] made dfs as exploration order available Former-commit-id: 46ea31af78b5819690fcc0a47ef9c1565c109c2b --- src/builder/ExplicitPrismModelBuilder.cpp | 12 +--- src/parser/PrismParser.cpp | 4 +- src/settings/ArgumentValidators.h | 16 ++++-- src/storage/BitVectorHashMap.cpp | 7 +-- src/storage/BitVectorHashMap.h | 3 +- src/storage/SparseMatrix.cpp | 70 +++++++---------------- src/storage/SparseMatrix.h | 5 -- 7 files changed, 40 insertions(+), 77 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 1aeab458d..1ef7f3ad8 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -231,8 +231,8 @@ namespace storm { } // Now that the program is fixed, we we need to substitute all constants with their concrete value. - this->program = program.substituteConstants(); - + this->program = this->program.substituteConstants(); + // Create the variable information for the transformed program. this->variableInformation = VariableInformation(this->program); @@ -481,13 +481,7 @@ namespace storm { this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices); // Fix (c). - std::unordered_map valueRemapping; - for (StateType index = 0; index < remapping.size(); ++index) { - if (remapping[index] != index) { - valueRemapping.emplace(index, static_cast(remapping[index])); - } - } - this->internalStateInformation.stateStorage.remap(valueRemapping); + this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } ); } return choiceLabels; diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 9040f3cf4..b2a153f99 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -11,7 +11,7 @@ namespace storm { namespace parser { storm::prism::Program PrismParser::parse(std::string const& filename) { // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); + std::ifstream inputFileStream(filename); STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); storm::prism::Program result; @@ -35,7 +35,7 @@ namespace storm { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); - assert(first != last); + STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser."); // Create empty result; storm::prism::Program result; diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h index 235ddd765..6e1b4aa02 100644 --- a/src/settings/ArgumentValidators.h +++ b/src/settings/ArgumentValidators.h @@ -18,6 +18,7 @@ #include "src/exceptions/IllegalArgumentValueException.h" #include "src/exceptions/IllegalFunctionCallException.h" +#include namespace storm { namespace settings { @@ -97,11 +98,16 @@ namespace storm { */ static std::function existingReadableFileValidator() { return [] (std::string const fileName) -> bool { - std::ifstream targetFile(fileName); - bool isFileGood = targetFile.good(); - - STORM_LOG_THROW(isFileGood, storm::exceptions::IllegalArgumentValueException, "The file " << fileName << " does not exist or is not readable."); - return isFileGood; + // First check existence as ifstream::good apparently als returns true for directories. + struct stat info; + stat(fileName.c_str(), &info); + STORM_LOG_THROW(info.st_mode & S_IFREG, storm::exceptions::IllegalArgumentValueException, "Unable to read from non-existing file '" << fileName << "'."); + + // Now that we know it's a file, we can check its readability. + std::ifstream istream(fileName); + STORM_LOG_THROW(istream.good(), storm::exceptions::IllegalArgumentValueException, "Unable to read from file '" << fileName << "'."); + + return true; }; } diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index fd4304eaa..66ff43f96 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -234,12 +234,9 @@ namespace storm { } template - void BitVectorHashMap::remap(std::unordered_map const& remapping) { + void BitVectorHashMap::remap(std::function const& remapping) { for (auto pos : occupied) { - auto it = remapping.find(values[pos]); - if (it != remapping.end()) { - values[pos] = it->second; - } + values[pos] = remapping(values[pos]); } } diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h index 7e8a1dc0e..746467203 100644 --- a/src/storage/BitVectorHashMap.h +++ b/src/storage/BitVectorHashMap.h @@ -3,7 +3,6 @@ #include #include -#include #include "src/storage/BitVector.h" @@ -129,7 +128,7 @@ namespace storm { * * @param remapping The remapping to apply. */ - void remap(std::unordered_map const& remapping); + void remap(std::function const& remapping); private: /*! diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 08138d48c..9d390185f 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -218,68 +218,40 @@ namespace storm { template bool SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { - bool changed = false; + bool matrixChanged = false; - // Sort columns per row. - typename SparseMatrix::index_type endGroups; - typename SparseMatrix::index_type endRows; - for (index_type group = 0; group < rowGroupIndices.size(); ++group) { - endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size(); - for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) { - bool changedRow = false; - endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); - - for (auto it = columnsAndValues.begin() + rowIndications[i], ite = columnsAndValues.begin() + endRows; it != ite; ++it) { - if (it->getColumn() >= offset) { - it->setColumn(replacements[it->getColumn() - offset]); - changedRow = true; - } - // Update highest column in a way that only works if the highest appearing index does not become - // lower during performing the replacement. - highestColumn = std::max(highestColumn, it->getColumn()); - } - - if (changedRow) { - changed = true; - - // Sort the row. - std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() < b.getColumn(); - }); - // Assert no equal elements - STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() <= b.getColumn(); - }), "Must not have different elements with the same column in a row."); + // Walk through all rows. + for (index_type row = 0; row < rowIndications.size(); ++row) { + bool rowChanged = false; + index_type rowEnd = row < rowIndications.size()-1 ? rowIndications[row+1] : columnsAndValues.size(); + + for (auto it = columnsAndValues.begin() + rowIndications[row], ite = columnsAndValues.begin() + rowEnd; it != ite; ++it) { + if (it->getColumn() >= offset && it->getColumn() != replacements[it->getColumn() - offset]) { + it->setColumn(replacements[it->getColumn() - offset]); + rowChanged = true; } + // Update highest column in a way that only works if the highest appearing index does not become + // lower during performing the replacement. + highestColumn = std::max(highestColumn, it->getColumn()); } - } - - return changed; - } - - template - void SparseMatrixBuilder::fixColumns() { - // Sort columns per row. - typename SparseMatrix::index_type endGroups; - typename SparseMatrix::index_type endRows; - for (index_type group = 0; group < rowGroupIndices.size(); ++group) { - endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size(); - for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) { - endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); + + if (rowChanged) { + matrixChanged = true; + // Sort the row. - std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + std::sort(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd, [](MatrixEntry const& a, MatrixEntry const& b) { return a.getColumn() < b.getColumn(); }); // Assert no equal elements - STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd, [](MatrixEntry const& a, MatrixEntry const& b) { return a.getColumn() <= b.getColumn(); }), "Must not have different elements with the same column in a row."); } } + + return matrixChanged; } template diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 4892dbe32..1ecee566f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -288,11 +288,6 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroup; - - /*! - * Fixes the matrix by sorting the columns to gain increasing order again. - */ - void fixColumns(); }; /*!