From f767cfe844a5010675add7c6c8ae95ca830e68c0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 5 Sep 2014 15:56:54 +0200 Subject: [PATCH 01/11] Started to modify the matrix builder to be a bit smarter about preallocation. Former-commit-id: 50be5c8af109981ed4ba11d34c7de57584b9c7f9 --- src/storage/SparseMatrix.cpp | 150 +++++++++++------------------------ src/storage/SparseMatrix.h | 2 + 2 files changed, 47 insertions(+), 105 deletions(-) diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index f4ad62d66..363f5413a 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -59,31 +59,11 @@ namespace storm { template void SparseMatrixBuilder::addNextValue(index_type row, index_type column, ValueType const& value) { - // Depending on whether the internal data storage was preallocated or not, adding the value is done somewhat - // differently. - if (storagePreallocated) { - // Check whether the given row and column positions are valid and throw error otherwise. - if (row >= rowCount || column >= columnCount) { - throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds position (" << row << ", " << column << ") in matrix of size (" << rowCount << ", " << columnCount << ")."; - } - } else { - if (rowCountSet) { - if (row >= rowCount) { - throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds row " << row << " in matrix with " << rowCount << " rows."; - } - } - if (columnCountSet) { - if (column >= columnCount) { - throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding entry at out-of-bounds column " << column << " in matrix with " << columnCount << " columns."; - } - } - } - // Check that we did not move backwards wrt. the row. if (row < lastRow) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added."; } - + // Check that we did not move backwards wrt. to column. if (row == lastRow && column < lastColumn) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row."; @@ -91,23 +71,14 @@ namespace storm { // If we switched to another row, we have to adjust the missing entries in the row indices vector. if (row != lastRow) { - if (storagePreallocated) { - // If the storage was preallocated, we can access the elements in the vectors with the subscript - // operator. - for (index_type i = lastRow + 1; i <= row; ++i) { - rowIndications[i] = currentEntryCount; - } - } else { - // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations. - for (index_type i = lastRow + 1; i <= row; ++i) { - rowIndications.push_back(currentEntryCount); - } + // Otherwise, we need to push the correct values to the vectors, which might trigger reallocations. + for (index_type i = lastRow + 1; i <= row; ++i) { + rowIndications.push_back(currentEntryCount); } if (!hasCustomRowGrouping) { for (index_type i = lastRow + 1; i <= row; ++i) { rowGroupIndices.push_back(i); - ++currentRowGroup; } } @@ -121,12 +92,8 @@ namespace storm { columnsAndValues[currentEntryCount] = std::make_pair(column, value); } else { columnsAndValues.emplace_back(column, value); - if (!columnCountSet) { - columnCount = std::max(columnCount, column + 1); - } - if (!rowCountSet) { - rowCount = row + 1; - } + columnCount = std::max(columnCount, column + 1); + rowCount = row + 1; } ++currentEntryCount; } @@ -138,88 +105,61 @@ namespace storm { } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) { throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size."; } - if (rowGroupCountSet) { - rowGroupIndices[currentRowGroup] = startingRow; - ++currentRowGroup; - } else { - rowGroupIndices.push_back(startingRow); - } + + rowGroupIndices.push_back(startingRow); } template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { - // Check whether it's safe to finalize the matrix and throw error otherwise. - if (storagePreallocated && currentEntryCount != entryCount) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::build: expected " << entryCount << " entries, but got " << currentEntryCount << " instead."; - } else { - // Fill in the missing entries in the row indices array, as there may be empty rows at the end. - if (storagePreallocated) { - for (index_type i = lastRow + 1; i < rowCount; ++i) { - rowIndications[i] = currentEntryCount; - } - } else { - if (!rowCountSet) { - rowCount = std::max(overriddenRowCount, rowCount); - } - for (index_type i = lastRow + 1; i < rowCount; ++i) { - rowIndications.push_back(currentEntryCount); - } - } - - // We put a sentinel element at the last position of the row indices array. This eases iteration work, - // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for - // the first and last row. - if (storagePreallocated) { - rowIndications[rowCount] = currentEntryCount; - } else { + // If the current row count was overridden, we may need to add empty rows. + if (overriddenRowCount > rowCount) { + for (index_type i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); - if (!columnCountSet) { - columnCount = std::max(columnCount, overriddenColumnCount); - } } - - entryCount = currentEntryCount; - - if (hasCustomRowGrouping && rowGroupCountSet) { - rowGroupIndices[rowGroupCount] = rowCount; - } else { - if (!hasCustomRowGrouping) { - for (index_type i = currentRowGroup; i < rowCount; ++i) { - rowGroupIndices.push_back(i + 1); - } - } else { - overriddenRowGroupCount = std::max(overriddenRowGroupCount, currentRowGroup + 1); - for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) { - rowGroupIndices.push_back(rowCount); - } + } + + // We put a sentinel element at the last position of the row indices array. This eases iteration work, + // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for + // the first and last row. + rowIndications.push_back(currentEntryCount); + + // Check whether the column count has been overridden. + if (overriddenColumnCount > columnCount) { + columnCount = overriddenColumnCount; + } + + entryCount = currentEntryCount; + + // Check whether row groups are missing some entries. + if (!hasCustomRowGrouping) { + for (index_type i = currentRowGroup; i < rowCount; ++i) { + rowGroupIndices.push_back(i + 1); + } + } else { + // Check if the row group count has been overridden. + if (overriddenRowGroupCount > currentRowGroup + 1) { + for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) { + rowGroupIndices.push_back(rowCount); } } } - + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } template void SparseMatrixBuilder::prepareInternalStorage() { - // Only allocate the memory for the matrix contents if the dimensions of the matrix are already known. - if (storagePreallocated) { - columnsAndValues = std::vector>(entryCount, MatrixEntry(0, storm::utility::constantZero())); - rowIndications = std::vector(rowCount + 1, 0); - } else { - rowIndications.push_back(0); + if (rowCount > 0) { + rowIndications.reserve(rowCount + 1); } - - // Only allocate the memory for the row grouping of the matrix contents if the number of groups is already - // known. - if (hasCustomRowGrouping && rowGroupCountSet) { - rowGroupIndices = std::vector(rowGroupCount + 1, 0); - } else { - if (hasCustomRowGrouping) { - // Nothing to do in this case - } else { - rowGroupIndices.push_back(0); - } + if (entryCount > 0) { + columnsAndValues.reserve(entryCount); + } + if (rowGroupCount > 0) { + rowGroupIndices.reserve(rowGroupCount + 1); } + rowIndications.push_back(0); + rowGroupIndices.push_back(0); } template diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index e87f215af..a5964d220 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -122,6 +122,8 @@ namespace storm { /*! * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. + * The number of rows, columns and entries is reserved upon creation. If more rows/columns or entries are + * added, this will possibly lead to a reallocation. * * @param rows The number of rows of the resulting matrix. * @param columns The number of columns of the resulting matrix. From fff4e61fc3f7690a0284f932a4e783f0ad7857ea Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 6 Sep 2014 00:55:03 +0200 Subject: [PATCH 02/11] Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space. Former-commit-id: e36d05398e30811a4061a4453ac2cdec27967525 --- src/adapters/ExplicitModelAdapter.h | 4 +- .../SparseMarkovAutomatonCslModelChecker.h | 2 +- src/models/MarkovAutomaton.h | 2 +- src/models/Mdp.h | 2 +- ...NondeterministicSparseTransitionParser.cpp | 6 +- src/storage/SparseMatrix.cpp | 109 +++++++++--------- src/storage/SparseMatrix.h | 45 ++++---- ...ndeterministicLinearEquationSolverTest.cpp | 4 +- ...ndeterministicLinearEquationSolverTest.cpp | 4 +- test/functional/storage/SparseMatrixTest.cpp | 10 +- 10 files changed, 96 insertions(+), 92 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 25804b58a..211a3aecf 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -662,8 +662,8 @@ namespace storm { bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC; // Build the transition and reward matrices. - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0); - storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, !deterministicModel, 0); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); + storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); // Finalize the resulting matrices. diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 56b36ac37..493f286bf 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -347,7 +347,7 @@ namespace storm { // Finally, we are ready to create the SSP matrix and right-hand side of the SSP. std::vector b; - typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size()); + typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). uint_fast64_t currentChoice = 0; diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 8f5825d6d..ef73c26ea 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -126,7 +126,7 @@ namespace storm { //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. - storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates()); + storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, false, true, this->getNumberOfStates()); // Now copy over all choices that need to be kept. uint_fast64_t currentChoice = 0; diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 5dd1c8c0e..0a0c2e06e 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -139,7 +139,7 @@ public: std::vector> const& choiceLabeling = this->getChoiceLabeling(); - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true); std::vector> newChoiceLabeling; // Check for each choice of each state, whether the choice labels are fully contained in the given label set. diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 32557dbb2..5923f7778 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -92,9 +92,9 @@ namespace storm { LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex+1) << " with " << firstPass.numberOfNonzeroEntries << " entries."); storm::storage::SparseMatrixBuilder matrixBuilder; if(!isRewardFile) { - matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, firstPass.highestStateIndex + 1); + matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, firstPass.highestStateIndex + 1); } else { - matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, modelInformation.getRowGroupCount()); + matrixBuilder = storm::storage::SparseMatrixBuilder(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, modelInformation.getRowGroupCount()); } // Initialize variables for the parsing run. @@ -179,7 +179,7 @@ namespace storm { // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices. if(isRewardFile) { // We already have rowGroup 0. - for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size(); index++) { + for(uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) { matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]); } } else { diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 363f5413a..0b5846acc 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -9,6 +9,7 @@ #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidStateException.h" +#include "src/exceptions/ExceptionMacros.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -53,8 +54,18 @@ namespace storm { } template - SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool hasCustomRowGrouping, index_type rowGroups) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), hasCustomRowGrouping(hasCustomRowGrouping), rowGroupCountSet(rowGroups != 0), rowGroupCount(rowGroups), rowGroupIndices(), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), currentRowGroup(0) { - this->prepareInternalStorage(); + SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) { + // Prepare the internal storage. + if (initialRowCountSet > 0) { + rowIndications.reserve(initialRowCount + 1); + } + if (initialEntryCountSet > 0) { + columnsAndValues.reserve(initialEntryCount); + } + if (initialRowGroupCountSet > 0) { + rowGroupIndices.reserve(initialRowGroupCount + 1); + } + rowIndications.push_back(0); } template @@ -76,46 +87,44 @@ namespace storm { rowIndications.push_back(currentEntryCount); } - if (!hasCustomRowGrouping) { - for (index_type i = lastRow + 1; i <= row; ++i) { - rowGroupIndices.push_back(i); - } - } - lastRow = row; } lastColumn = column; // Finally, set the element and increase the current size. - if (storagePreallocated) { - columnsAndValues[currentEntryCount] = std::make_pair(column, value); - } else { - columnsAndValues.emplace_back(column, value); - columnCount = std::max(columnCount, column + 1); - rowCount = row + 1; - } + columnsAndValues.emplace_back(column, value); + highestColumn = std::max(highestColumn, column); ++currentEntryCount; + + // In case we did not expect this value, we throw an exception. + if (forceInitialDimensions) { + LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << "."); + LOG_THROW(!initialColumnCountSet || lastColumn < initialColumnCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal column " << lastColumn << "."); + LOG_THROW(!initialEntryCountSet || currentEntryCount <= initialEntryCount, storm::exceptions::OutOfRangeException, "Too many entries in matrix, expected only " << initialEntryCount << "."); + } } template void SparseMatrixBuilder::newRowGroup(index_type startingRow) { - if (!hasCustomRowGrouping) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping."; - } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size."; - } - + LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); + LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size."); rowGroupIndices.push_back(startingRow); + ++currentRowGroup; } template SparseMatrix SparseMatrixBuilder::build(index_type overriddenRowCount, index_type overriddenColumnCount, index_type overriddenRowGroupCount) { + uint_fast64_t rowCount = lastRow + 1; + if (initialRowCountSet && forceInitialDimensions) { + LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); + rowCount = std::max(rowCount, initialRowCount); + } + rowCount = std::max(rowCount, overriddenRowCount); + // If the current row count was overridden, we may need to add empty rows. - if (overriddenRowCount > rowCount) { - for (index_type i = lastRow + 1; i < rowCount; ++i) { - rowIndications.push_back(currentEntryCount); - } + for (index_type i = lastRow + 1; i < rowCount; ++i) { + rowIndications.push_back(currentEntryCount); } // We put a sentinel element at the last position of the row indices array. This eases iteration work, @@ -123,45 +132,39 @@ namespace storm { // the first and last row. rowIndications.push_back(currentEntryCount); - // Check whether the column count has been overridden. - if (overriddenColumnCount > columnCount) { - columnCount = overriddenColumnCount; + uint_fast64_t columnCount = highestColumn + 1; + if (initialColumnCountSet && forceInitialDimensions) { + LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << "."); + columnCount = std::max(columnCount, initialColumnCount); + } + columnCount = std::max(columnCount, overriddenColumnCount); + + uint_fast64_t entryCount = currentEntryCount; + if (initialEntryCountSet && forceInitialDimensions) { + LOG_THROW(entryCount == initialEntryCount, storm::exceptions::InvalidStateException, "Expected " << initialEntryCount << " entries, but got " << entryCount << "."); } - - entryCount = currentEntryCount; // Check whether row groups are missing some entries. if (!hasCustomRowGrouping) { - for (index_type i = currentRowGroup; i < rowCount; ++i) { - rowGroupIndices.push_back(i + 1); + for (index_type i = 0; i <= rowCount; ++i) { + rowGroupIndices.push_back(i); } } else { - // Check if the row group count has been overridden. - if (overriddenRowGroupCount > currentRowGroup + 1) { - for (index_type i = currentRowGroup; i < overriddenRowGroupCount; ++i) { - rowGroupIndices.push_back(rowCount); - } + uint_fast64_t rowGroupCount = currentRowGroup; + if (initialRowGroupCountSet && forceInitialDimensions) { + LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << "."); + rowGroupCount = std::max(rowGroupCount, initialRowGroupCount); + } + rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount); + + for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) { + rowGroupIndices.push_back(rowCount); } } return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); } - template - void SparseMatrixBuilder::prepareInternalStorage() { - if (rowCount > 0) { - rowIndications.reserve(rowCount + 1); - } - if (entryCount > 0) { - columnsAndValues.reserve(entryCount); - } - if (rowGroupCount > 0) { - rowGroupIndices.reserve(rowGroupCount + 1); - } - rowIndications.push_back(0); - rowGroupIndices.push_back(0); - } - template SparseMatrix::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. @@ -471,7 +474,7 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true); + SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries, true, true); // Create a temporary vector that stores for each index whose bit is set to true the number of bits that // were set before that particular index. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index a5964d220..b419ca841 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -128,12 +128,14 @@ namespace storm { * @param rows The number of rows of the resulting matrix. * @param columns The number of columns of the resulting matrix. * @param entries The number of entries of the resulting matrix. + * @param forceDimensions If this flag is set, the matrix is expected to have exactly the given number of + * rows, columns and entries for all of these entities that are set to a nonzero value. * @param hasCustomRowGrouping A flag indicating whether the builder is used to create a non-canonical * grouping of rows for this matrix. * @param rowGroups The number of row groups of the resulting matrix. This is only relevant if the matrix * has a custom row grouping. */ - SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool hasCustomRowGrouping = false, index_type rowGroups = 0); + SparseMatrixBuilder(index_type rows = 0, index_type columns = 0, index_type entries = 0, bool forceDimensions = true, bool hasCustomRowGrouping = false, index_type rowGroups = 0); /*! * Sets the matrix entry at the given row and column to the given value. After all entries have been added, @@ -180,42 +182,38 @@ namespace storm { SparseMatrix build(index_type overriddenRowCount = 0, index_type overriddenColumnCount = 0, index_type overriddenRowGroupCount = 0); private: - /*! - * Prepares the internal storage of the builder. This relies on the number of entries and the number of rows - * being set correctly. They may, however, be zero, in which case the insertion of elements in the builder - * will cause occasional reallocations. - */ - void prepareInternalStorage(); - - // A flag indicating whether the number of rows was set upon construction. - bool rowCountSet; + // A flag indicating whether a row count was set upon construction. + bool initialRowCountSet; - // The number of rows of the matrix. - index_type rowCount; + // The row count that was initially set (if any). + index_type initialRowCount; - // A flag indicating whether the number of columns was set upon construction. - bool columnCountSet; + // A flag indicating whether a column count was set upon construction. + bool initialColumnCountSet; + + // The column count that was initially set (if any). + index_type initialColumnCount; - // The number of columns of the matrix. - index_type columnCount; + // A flag indicating whether an entry count was set upon construction. + bool initialEntryCountSet; // The number of entries in the matrix. - index_type entryCount; + index_type initialEntryCount; + + // A flag indicating whether the initially given dimensions are to be enforced on the resulting matrix. + bool forceInitialDimensions; // A flag indicating whether the builder is to construct a custom row grouping for the matrix. bool hasCustomRowGrouping; // A flag indicating whether the number of row groups was set upon construction. - bool rowGroupCountSet; + bool initialRowGroupCountSet; // The number of row groups in the matrix. - index_type rowGroupCount; + index_type initialRowGroupCount; std::vector rowGroupIndices; - // Stores whether the storage of the matrix was preallocated or not. - bool storagePreallocated; - // The storage for the columns and values of all entries in the matrix. std::vector> columnsAndValues; @@ -237,6 +235,9 @@ namespace storm { // entry into a matrix. index_type lastColumn; + // Stores the highest column at which an entry was inserted into the matrix. + index_type highestColumn; + // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroup; diff --git a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp index ae9542bbb..04f0b4036 100644 --- a/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxNondeterministicLinearEquationSolverTest.cpp @@ -5,7 +5,7 @@ #include "src/settings/Settings.h" TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { - storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -24,7 +24,7 @@ TEST(GmmxxNondeterministicLinearEquationSolver, SolveWithStandardOptions) { } TEST(GmmxxNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { - storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099)); diff --git a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp index 0ccdafd84..4c7f76337 100644 --- a/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeNondeterministicLinearEquationSolverTest.cpp @@ -5,7 +5,7 @@ #include "src/settings/Settings.h" TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { - storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); @@ -24,7 +24,7 @@ TEST(NativeNondeterministicLinearEquationSolver, SolveWithStandardOptions) { } TEST(NativeNondeterministicLinearEquationSolver, MatrixVectorMultiplication) { - storm::storage::SparseMatrixBuilder builder(0, 0, 0, true); + storm::storage::SparseMatrixBuilder builder(0, 0, 0, false, true); ASSERT_NO_THROW(builder.newRowGroup(0)); ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.9)); ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.099)); diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 52746ef97..b677f6f3c 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -221,7 +221,7 @@ TEST(SparseMatrix, MakeAbsorbing) { } TEST(SparseMatrix, MakeRowGroupAbsorbing) { - storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9, true); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9, true, true); ASSERT_NO_THROW(matrixBuilder.newRowGroup(0)); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); @@ -242,7 +242,7 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) { ASSERT_NO_THROW(matrix.makeRowGroupsAbsorbing(absorbingRowGroups)); - storm::storage::SparseMatrixBuilder matrixBuilder2(0, 0, 0, true); + storm::storage::SparseMatrixBuilder matrixBuilder2(0, 0, 0, false, true); ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0)); ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); @@ -283,7 +283,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) { std::vector constrainedRowSum = matrix.getConstrainedRowSumVector(storm::storage::BitVector(5, true), columnConstraint); ASSERT_TRUE(constrainedRowSum == std::vector({1.0, 0.7, 0, 0, 0.5})); - storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 9, true); + storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 9, true, true); ASSERT_NO_THROW(matrixBuilder2.newRowGroup(0)); ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); @@ -312,7 +312,7 @@ TEST(SparseMatrix, ConstrainedRowSumVector) { } TEST(SparseMatrix, Submatrix) { - storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9, true); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9, true, true); ASSERT_NO_THROW(matrixBuilder.newRowGroup(0)); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); @@ -342,7 +342,7 @@ TEST(SparseMatrix, Submatrix) { ASSERT_NO_THROW(storm::storage::SparseMatrix matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false)); storm::storage::SparseMatrix matrix2 = matrix.getSubmatrix(true, rowGroupConstraint, columnConstraint, false); - storm::storage::SparseMatrixBuilder matrixBuilder3(3, 2, 3, true); + storm::storage::SparseMatrixBuilder matrixBuilder3(3, 2, 3, true, true); ASSERT_NO_THROW(matrixBuilder3.newRowGroup(0)); ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 0, 0.5)); ASSERT_NO_THROW(matrixBuilder3.newRowGroup(2)); From 6fde42850dcf348e9bedadf46a239fbc95486196 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 10 Sep 2014 14:57:22 +0200 Subject: [PATCH 03/11] fix for gcc 4.9 Former-commit-id: d6f8d87a63c56b61e0e7899ecb832b873f840990 --- src/models/AbstractModel.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 05296c584..67d495408 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -309,7 +309,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if this model has a state reward model. */ bool hasStateRewards() const { - return stateRewardVector; + return static_cast(stateRewardVector); } /*! @@ -317,7 +317,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if this model has a transition reward model. */ bool hasTransitionRewards() const { - return transitionRewardMatrix; + return static_cast(transitionRewardMatrix); } /*! @@ -325,7 +325,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @return True if this model has a labeling. */ bool hasChoiceLabeling() const { - return choiceLabeling; + return static_cast(choiceLabeling); } /*! From 2c231a794d490d483250c455b990165ac91f20e8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 10 Sep 2014 20:15:50 +0200 Subject: [PATCH 04/11] SCC decomposition now correctly ignores zero-entries in the matrix. Former-commit-id: 351c0ac6ade95a54f533a1318532632ac7266d78 --- src/storage/StronglyConnectedComponentDecomposition.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp index 46990e7eb..784e99ab0 100644 --- a/src/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storage/StronglyConnectedComponentDecomposition.cpp @@ -161,7 +161,7 @@ namespace storm { bool recursionStepIn = false; for (; successorIt != model.getRows(currentState).end(); ++successorIt) { - if (subsystem.get(successorIt->getColumn())) { + if (subsystem.get(successorIt->getColumn()) && successorIt->getValue() != storm::utility::constantZero()) { if (currentState == successorIt->getColumn()) { statesWithSelfLoop.set(currentState); } From b3810dc75b82d6bddb97151e53466d6b83afe4fe Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 11 Sep 2014 14:44:51 +0200 Subject: [PATCH 05/11] factored out code parts from storm.cpp Former-commit-id: 91cd8e52ad3b38b5be6a56f9b564514e78377514 --- src/counterexamples/GenerateCounterexample.h | 132 ++++++++++++++++ src/utility/CLI.h | 151 +++++++++++++++++++ src/utility/Initialize.h | 22 +++ src/utility/InitializeLogging.h | 37 +++++ 4 files changed, 342 insertions(+) create mode 100644 src/counterexamples/GenerateCounterexample.h create mode 100644 src/utility/CLI.h create mode 100644 src/utility/Initialize.h create mode 100644 src/utility/InitializeLogging.h diff --git a/src/counterexamples/GenerateCounterexample.h b/src/counterexamples/GenerateCounterexample.h new file mode 100644 index 000000000..e59df9ba5 --- /dev/null +++ b/src/counterexamples/GenerateCounterexample.h @@ -0,0 +1,132 @@ + +#ifndef STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_ +#define STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_ + + + +/*! + * Handles the counterexample generation control. + * + * @param parser An AutoParser to get the model from. + */ + void generateCounterExample(std::shared_ptr> model) { + LOG4CPLUS_INFO(logger, "Starting counterexample generation."); + LOG4CPLUS_INFO(logger, "Testing inputs..."); + + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + + // First test output directory. + std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); + if(outPath.back() != '/' && outPath.back() != '\\') { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + std::ofstream testFile(outPath + "test.dot"); + if(testFile.fail()) { + LOG4CPLUS_ERROR(logger, "The output path is not valid."); + return; + } + testFile.close(); + std::remove((outPath + "test.dot").c_str()); + + // Differentiate between model types. + if(model->getType() != storm::models::DTMC) { + LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); + return; + } + + // Get the Dtmc back from the AbstractModel + // Note that the ownership of the object referenced by dtmc lies at the main function. + // Thus, it must not be deleted. + storm::models::Dtmc dtmc = *(model->as>()); + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + + // Get specified PRCTL formulas. + if(!s->isSet("prctl")) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); + std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); + + // Test for each formula if a counterexample can be generated for it. + if(formulaList.size() == 0) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula found."); + return; + } + + // Get prctl file name without the filetype + uint_fast64_t first = 0; + if(chosenPrctlFile.find('/') != std::string::npos) { + first = chosenPrctlFile.find_last_of('/') + 1; + } else if(chosenPrctlFile.find('\\') != std::string::npos) { + first = chosenPrctlFile.find_last_of('\\') + 1; + } + + uint_fast64_t length; + if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) { + length = chosenPrctlFile.find_last_of('.') - first; + } else { + length = chosenPrctlFile.length() - first; + } + + std::string outFileName = chosenPrctlFile.substr(first, length); + + // Test formulas and do generation + uint_fast64_t fIndex = 0; + for (auto formula : formulaList) { + + // First check if it is a formula type for which a counterexample can be generated. + if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { + LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); + continue; + } + + std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); + + // Do some output + std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; + LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": "); + std::cout << "\t" << formula->toString() << "\n" << std::endl; + LOG4CPLUS_INFO(logger, formula->toString()); + + // Now check if the model does not satisfy the formula. + // That is if there is at least one initial state of the model that does not. + + // Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them) + // Lower it again after the model check. + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); + storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc)); + logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); + + if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) { + std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; + LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample."); + continue; + } + + // Generate counterexample + storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(dtmc, stateForm); + + LOG4CPLUS_INFO(logger, "Found counterexample."); + + // Output counterexample + // Do standard output + std::cout << "Found counterexample with following properties: " << std::endl; + counterExample.printModelInformationToStream(std::cout); + std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl; + + // Write the .dot file + std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot"); + if(outFile.good()) { + counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true); + outFile.close(); + } + + fIndex++; + } + } + +#endif \ No newline at end of file diff --git a/src/utility/CLI.h b/src/utility/CLI.h new file mode 100644 index 000000000..7d650b37c --- /dev/null +++ b/src/utility/CLI.h @@ -0,0 +1,151 @@ +#ifndef STORM_UTILITY_CLI_H_ +#define STORM_UTILITY_CLI_H_ + +#include +#include +#include +#include + + +#include "src/utility/OsDetection.h" + +/*! +* Gives the current working directory +* +* @return std::string The path of the current working directory +*/ +std::string getCurrentWorkingDirectory() { + char temp[512]; + return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); +} + + +void printUsage() { +#ifndef WINDOWS + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + + std::cout << "===== Statistics ==============================" << std::endl; + std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; + std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "===============================================" << std::endl; +#else + HANDLE hProcess = GetCurrentProcess (); + FILETIME ftCreation, ftExit, ftUser, ftKernel; + PROCESS_MEMORY_COUNTERS pmc; + if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { + std::cout << "Memory Usage: " << std::endl; + std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; + std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; + std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; + std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; + std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; + std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; + std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; + std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; + std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; + } + + GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); + + ULARGE_INTEGER uLargeInteger; + uLargeInteger.LowPart = ftKernel.dwLowDateTime; + uLargeInteger.HighPart = ftKernel.dwHighDateTime; + double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds + uLargeInteger.LowPart = ftUser.dwLowDateTime; + uLargeInteger.HighPart = ftUser.dwHighDateTime; + double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; + + std::cout << "CPU Time: " << std::endl; + std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; + std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; +#endif +} + + + +/*! + * Prints the header. + */ +void printHeader(const int argc, const char* argv[]) { + std::cout << "StoRM" << std::endl; + std::cout << "-----" << std::endl << std::endl; + + std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; + if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { + std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; + } + std::cout << " build from revision " << STORM_CPP_VERSION_HASH; + if (STORM_CPP_VERSION_DIRTY == 1) { + std::cout << " (DIRTY)"; + } + std::cout << "." << std::endl; + +#ifdef STORM_HAVE_INTELTBB + std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; +#endif +#ifdef STORM_HAVE_GLPK + std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; +#endif +#ifdef STORM_HAVE_GUROBI + std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; +#endif +#ifdef STORM_HAVE_Z3 + unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; + Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); + std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; +#endif + + // "Compute" the command line argument string with which STORM was invoked. + std::stringstream commandStream; + for (int i = 0; i < argc; ++i) { + commandStream << argv[i] << " "; + } + std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; + std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; +} + +/*! + * Parses the given command line arguments. + * + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(const int argc, const char* argv[]) { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + try { + storm::settings::Settings::parse(argc, argv); + } catch (storm::exceptions::OptionParserException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << s->getHelpText(); + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::Settings::getInstance()->getHelpText(); + return false; + } + + if (s->isSet("verbose")) { + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); + } + if (s->isSet("debug")) { + logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); + } + if (s->isSet("trace")) { + logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); + } + if (s->isSet("logfile")) { + setUpFileLogging(); + } + return true; +} + + +#endif \ No newline at end of file diff --git a/src/utility/Initialize.h b/src/utility/Initialize.h new file mode 100644 index 000000000..cf2facda5 --- /dev/null +++ b/src/utility/Initialize.h @@ -0,0 +1,22 @@ +#ifndef STORM_UTILITY_INITIALIZE_H_ +#define STORM_UTILITY_INITIALIZE_H_ + +#include "InitializeLogging.h" + +/*! + * Performs some necessary initializations. + */ +void setUp() { + // Increase the precision of output. + std::cout.precision(10); +} + +/*! + * Performs some necessary clean-up. + */ +void cleanUp() { + // Intentionally left empty. +} + + +#endif \ No newline at end of file diff --git a/src/utility/InitializeLogging.h b/src/utility/InitializeLogging.h new file mode 100644 index 000000000..f818f0f95 --- /dev/null +++ b/src/utility/InitializeLogging.h @@ -0,0 +1,37 @@ +#ifndef STORM_UTILITY_INITIALIZELOGGING_H_ +#define STORM_UTILITY_INITIALIZELOGGING_H_ + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" + + +log4cplus::Logger logger; + +/*! + * Initializes the logging framework and sets up logging to console. + */ +void initializeLogger() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); + consoleLogAppender->setName("mainConsoleAppender"); + consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); + consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); + logger.addAppender(consoleLogAppender); +} + +/*! + * Sets up the logging to file. + */ +void setUpFileLogging() { + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString())); + fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); + logger.addAppender(fileLogAppender); +} + + +#endif \ No newline at end of file From daca9d5294393c9a496db85a5dfeb900c60d10ce Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 11 Sep 2014 15:18:37 +0200 Subject: [PATCH 06/11] refactored main.cpp Former-commit-id: a0648b4e1f8338afa1b2141e82a9be49b2e9d116 --- src/counterexamples/GenerateCounterexample.h | 14 + .../prctl/CreatePrctlModelChecker.h | 43 ++ src/storm.cpp | 368 +----------------- src/utility/CLI.h | 17 + src/utility/InitializeLogging.h | 1 + 5 files changed, 84 insertions(+), 359 deletions(-) create mode 100644 src/modelchecker/prctl/CreatePrctlModelChecker.h diff --git a/src/counterexamples/GenerateCounterexample.h b/src/counterexamples/GenerateCounterexample.h index e59df9ba5..12d0f1da5 100644 --- a/src/counterexamples/GenerateCounterexample.h +++ b/src/counterexamples/GenerateCounterexample.h @@ -3,6 +3,20 @@ #define STORM_COUNTEREXAMPLES_GENERATECOUNTEREXAMPLE_H_ +#include "src/models/Dtmc.h" +#include "src/models/AtomicPropositionsLabeling.h" +#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "src/counterexamples/SMTMinimalCommandSetGenerator.h" +#include "src/counterexamples/PathBasedSubsystemGenerator.h" +#include "src/parser/PrctlParser.h" +#include "src/properties/Prctl.h" +#include "src/modelchecker/prctl/CreatePrctlModelChecker.h" + + +#include "src/parser/PrctlFileParser.h" + +#include "src/exceptions/InvalidSettingsException.h" + /*! * Handles the counterexample generation control. diff --git a/src/modelchecker/prctl/CreatePrctlModelChecker.h b/src/modelchecker/prctl/CreatePrctlModelChecker.h new file mode 100644 index 000000000..bd1b35c7e --- /dev/null +++ b/src/modelchecker/prctl/CreatePrctlModelChecker.h @@ -0,0 +1,43 @@ +#ifndef STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ +#define STORM_MODELCHECKER_PRCTL_CREATEPRCTLMODELCHECKER_H_ + +#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/NativeLinearEquationSolver.h" +#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" +#include "src/solver/GurobiLpSolver.h" +/*! + * Creates a model checker for the given DTMC that complies with the given options. + * + * @param dtmc A reference to the DTMC for which the model checker is to be created. + * @return A pointer to the resulting model checker. + */ +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc const & dtmc) { + // Create the appropriate model checker. + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString(); + if (linsolver == "gmm++") { + return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::GmmxxLinearEquationSolver()); + } else if (linsolver == "native") { + return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::NativeLinearEquationSolver()); + } + + // The control flow should never reach this point, as there is a default setting for matrixlib. + std::string message = "No matrix library suitable for DTMC model checking has been set."; + throw storm::exceptions::InvalidSettingsException() << message; + return nullptr; +} + +/*! + * Creates a model checker for the given MDP that complies with the given options. + * + * @param mdp The Dtmc that the model checker will check + * @return + */ +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const & mdp) { + // Create the appropriate model checker. + return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); +} + +#endif \ No newline at end of file diff --git a/src/storm.cpp b/src/storm.cpp index a3328ae92..940e75ed8 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -13,14 +13,18 @@ * Description: Central part of the application containing the main() Method */ -#include "src/utility/OsDetection.h" -#include +#include "src/utility/Initialize.h" #include #include #include #include #include #include +#include +#include + + + #include "storm-config.h" #include "storm-version.h" @@ -30,12 +34,14 @@ #include "src/storage/MaximalEndComponentDecomposition.h" #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "src/models/AtomicPropositionsLabeling.h" +#include "src/modelchecker/prctl/CreatePrctlModelChecker.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/solver/GurobiLpSolver.h" +#include "src/counterexamples/GenerateCounterexample.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h" #include "src/counterexamples/PathBasedSubsystemGenerator.h" @@ -45,251 +51,20 @@ #include "src/utility/ErrorHandling.h" #include "src/properties/Prctl.h" #include "src/utility/vector.h" -#include "src/utility/OsDetection.h" +#include "src/utility/CLI.h" -#include "src/settings/Settings.h" -// Registers all standard options -#include "src/utility/StormOptions.h" #include "src/parser/PrctlFileParser.h" #include "src/parser/LtlFileParser.h" -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" -log4cplus::Logger logger; - #include "src/parser/PrismParser.h" #include "src/adapters/ExplicitModelAdapter.h" // #include "src/adapters/SymbolicModelAdapter.h" #include "src/exceptions/InvalidSettingsException.h" -// Includes for the linked libraries and versions header -#ifdef STORM_HAVE_INTELTBB -# include "tbb/tbb_stddef.h" -#endif -#ifdef STORM_HAVE_GLPK -# include "glpk.h" -#endif -#ifdef STORM_HAVE_GUROBI -# include "gurobi_c.h" -#endif -#ifdef STORM_HAVE_Z3 -# include "z3.h" -#endif - -#include -#include -#include - -void printUsage() { -#ifndef WINDOWS - struct rusage ru; - getrusage(RUSAGE_SELF, &ru); - - std::cout << "===== Statistics ==============================" << std::endl; - std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; - std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; - std::cout << "===============================================" << std::endl; -#else - HANDLE hProcess = GetCurrentProcess (); - FILETIME ftCreation, ftExit, ftUser, ftKernel; - PROCESS_MEMORY_COUNTERS pmc; - if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { - std::cout << "Memory Usage: " << std::endl; - std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; - std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; - std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; - std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; - std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; - std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; - std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; - std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; - std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; - } - - GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); - - ULARGE_INTEGER uLargeInteger; - uLargeInteger.LowPart = ftKernel.dwLowDateTime; - uLargeInteger.HighPart = ftKernel.dwHighDateTime; - double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds - uLargeInteger.LowPart = ftUser.dwLowDateTime; - uLargeInteger.HighPart = ftUser.dwHighDateTime; - double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; - - std::cout << "CPU Time: " << std::endl; - std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; - std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl; -#endif -} - -/*! - * Initializes the logging framework and sets up logging to console. - */ -void initializeLogger() { - logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); - log4cplus::SharedAppenderPtr consoleLogAppender(new log4cplus::ConsoleAppender()); - consoleLogAppender->setName("mainConsoleAppender"); - consoleLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); - consoleLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %b:%L: %m%n"))); - logger.addAppender(consoleLogAppender); -} - -/*! - * Sets up the logging to file. - */ -void setUpFileLogging() { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender(s->getOptionByLongName("logfile").getArgument(0).getValueAsString())); - fileLogAppender->setName("mainFileAppender"); - fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M:%S} (%r ms) - %F:%L: %m%n"))); - logger.addAppender(fileLogAppender); -} - -/*! -* Gives the current working directory -* -* @return std::string The path of the current working directory -*/ -std::string getCurrentWorkingDirectory() { - char temp[512]; - return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); -} - -/*! - * Prints the header. - */ -void printHeader(const int argc, const char* argv[]) { - std::cout << "StoRM" << std::endl; - std::cout << "-----" << std::endl << std::endl; - - std::cout << "Version: " << STORM_CPP_VERSION_MAJOR << "." << STORM_CPP_VERSION_MINOR << "." << STORM_CPP_VERSION_PATCH; - if (STORM_CPP_VERSION_COMMITS_AHEAD != 0) { - std::cout << " (+" << STORM_CPP_VERSION_COMMITS_AHEAD << " commits)"; - } - std::cout << " build from revision " << STORM_CPP_VERSION_HASH; - if (STORM_CPP_VERSION_DIRTY == 1) { - std::cout << " (DIRTY)"; - } - std::cout << "." << std::endl; - -#ifdef STORM_HAVE_INTELTBB - std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; -#endif -#ifdef STORM_HAVE_GLPK - std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl; -#endif -#ifdef STORM_HAVE_GUROBI - std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; -#endif -#ifdef STORM_HAVE_Z3 - unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; - Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber); - std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl; -#endif - - // "Compute" the command line argument string with which STORM was invoked. - std::stringstream commandStream; - for (int i = 0; i < argc; ++i) { - commandStream << argv[i] << " "; - } - std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; - std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; -} - -/*! - * Parses the given command line arguments. - * - * @param argc The argc argument of main(). - * @param argv The argv argument of main(). - * @return True iff the program should continue to run after parsing the options. - */ -bool parseOptions(const int argc, const char* argv[]) { - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - try { - storm::settings::Settings::parse(argc, argv); - } catch (storm::exceptions::OptionParserException& e) { - std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << s->getHelpText(); - return false; - } - - if (s->isSet("help")) { - std::cout << storm::settings::Settings::getInstance()->getHelpText(); - return false; - } - - if (s->isSet("verbose")) { - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled verbose mode, log output gets printed to console."); - } - if (s->isSet("debug")) { - logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled very verbose mode, log output gets printed to console."); - } - if (s->isSet("trace")) { - logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); - logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); - LOG4CPLUS_INFO(logger, "Enabled trace mode, log output gets printed to console."); - } - if (s->isSet("logfile")) { - setUpFileLogging(); - } - return true; -} - -/*! - * Performs some necessary initializations. - */ -void setUp() { - // Increase the precision of output. - std::cout.precision(10); -} - -/*! - * Performs some necessary clean-up. - */ -void cleanUp() { - // Intentionally left empty. -} -/*! - * Creates a model checker for the given DTMC that complies with the given options. - * - * @param dtmc A reference to the DTMC for which the model checker is to be created. - * @return A pointer to the resulting model checker. - */ -storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc const & dtmc) { - // Create the appropriate model checker. - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - std::string const& linsolver = s->getOptionByLongName("linsolver").getArgument(0).getValueAsString(); - if (linsolver == "gmm++") { - return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::GmmxxLinearEquationSolver()); - } else if (linsolver == "native") { - return new storm::modelchecker::prctl::SparseDtmcPrctlModelChecker(dtmc, new storm::solver::NativeLinearEquationSolver()); - } - - // The control flow should never reach this point, as there is a default setting for matrixlib. - std::string message = "No matrix library suitable for DTMC model checking has been set."; - throw storm::exceptions::InvalidSettingsException() << message; - return nullptr; -} -/*! - * Creates a model checker for the given MDP that complies with the given options. - * - * @param mdp The Dtmc that the model checker will check - * @return - */ -storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const & mdp) { - // Create the appropriate model checker. - return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); -} /*! * Checks the PRCTL formulae provided on the command line on the given model checker. @@ -312,131 +87,6 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker } } -/*! - * Handles the counterexample generation control. - * - * @param parser An AutoParser to get the model from. - */ - void generateCounterExample(std::shared_ptr> model) { - LOG4CPLUS_INFO(logger, "Starting counterexample generation."); - LOG4CPLUS_INFO(logger, "Testing inputs..."); - - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - - // First test output directory. - std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString(); - if(outPath.back() != '/' && outPath.back() != '\\') { - LOG4CPLUS_ERROR(logger, "The output path is not valid."); - return; - } - std::ofstream testFile(outPath + "test.dot"); - if(testFile.fail()) { - LOG4CPLUS_ERROR(logger, "The output path is not valid."); - return; - } - testFile.close(); - std::remove((outPath + "test.dot").c_str()); - - // Differentiate between model types. - if(model->getType() != storm::models::DTMC) { - LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); - return; - } - - // Get the Dtmc back from the AbstractModel - // Note that the ownership of the object referenced by dtmc lies at the main function. - // Thus, it must not be deleted. - storm::models::Dtmc dtmc = *(model->as>()); - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - - // Get specified PRCTL formulas. - if(!s->isSet("prctl")) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); - return; - } - - std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); - LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile); - - // Test for each formula if a counterexample can be generated for it. - if(formulaList.size() == 0) { - LOG4CPLUS_ERROR(logger, "No PRCTL formula found."); - return; - } - - // Get prctl file name without the filetype - uint_fast64_t first = 0; - if(chosenPrctlFile.find('/') != std::string::npos) { - first = chosenPrctlFile.find_last_of('/') + 1; - } else if(chosenPrctlFile.find('\\') != std::string::npos) { - first = chosenPrctlFile.find_last_of('\\') + 1; - } - - uint_fast64_t length; - if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) { - length = chosenPrctlFile.find_last_of('.') - first; - } else { - length = chosenPrctlFile.length() - first; - } - - std::string outFileName = chosenPrctlFile.substr(first, length); - - // Test formulas and do generation - uint_fast64_t fIndex = 0; - for (auto formula : formulaList) { - - // First check if it is a formula type for which a counterexample can be generated. - if (std::dynamic_pointer_cast>(formula->getChild()).get() == nullptr) { - LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); - continue; - } - - std::shared_ptr> stateForm = std::static_pointer_cast>(formula->getChild()); - - // Do some output - std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl; - LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": "); - std::cout << "\t" << formula->toString() << "\n" << std::endl; - LOG4CPLUS_INFO(logger, formula->toString()); - - // Now check if the model does not satisfy the formula. - // That is if there is at least one initial state of the model that does not. - - // Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them) - // Lower it again after the model check. - logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL); - storm::storage::BitVector result = stateForm->check(*createPrctlModelChecker(dtmc)); - logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); - - if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) { - std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl; - LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample."); - continue; - } - - // Generate counterexample - storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(dtmc, stateForm); - - LOG4CPLUS_INFO(logger, "Found counterexample."); - - // Output counterexample - // Do standard output - std::cout << "Found counterexample with following properties: " << std::endl; - counterExample.printModelInformationToStream(std::cout); - std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl; - - // Write the .dot file - std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot"); - if(outFile.good()) { - counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true); - outFile.close(); - } - - fIndex++; - } - } - /*! * Main entry point. */ diff --git a/src/utility/CLI.h b/src/utility/CLI.h index 7d650b37c..858fdd8ff 100644 --- a/src/utility/CLI.h +++ b/src/utility/CLI.h @@ -8,6 +8,23 @@ #include "src/utility/OsDetection.h" +// Registers all standard options +#include "src/utility/StormOptions.h" + + +// Includes for the linked libraries and versions header +#ifdef STORM_HAVE_INTELTBB +# include "tbb/tbb_stddef.h" +#endif +#ifdef STORM_HAVE_GLPK +# include "glpk.h" +#endif +#ifdef STORM_HAVE_GUROBI +# include "gurobi_c.h" +#endif +#ifdef STORM_HAVE_Z3 +# include "z3.h" +#endif /*! * Gives the current working directory diff --git a/src/utility/InitializeLogging.h b/src/utility/InitializeLogging.h index f818f0f95..af45f21c3 100644 --- a/src/utility/InitializeLogging.h +++ b/src/utility/InitializeLogging.h @@ -6,6 +6,7 @@ #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" +#include "src/settings/Settings.h" log4cplus::Logger logger; From 418ce8b6257d31f2120d34a3b07f70c2931c8dfc Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Sep 2014 16:31:31 +0200 Subject: [PATCH 07/11] Fixed some problems related to the memory-mapped file. Former-commit-id: 68225d80063def05d6e7d8802638b1f42d5719e0 --- src/adapters/ExplicitModelAdapter.h | 2 +- .../AtomicPropositionLabelingParser.cpp | 2 +- src/parser/AutoParser.cpp | 30 ++++++++++------- src/parser/AutoParser.h | 2 ++ .../DeterministicSparseTransitionParser.cpp | 32 +++++++++++++++++-- .../DeterministicSparseTransitionParser.h | 2 +- src/parser/MappedFile.cpp | 16 ++++++---- src/parser/MappedFile.h | 10 ++++-- .../MarkovAutomatonSparseTransitionParser.cpp | 6 ++-- .../MarkovAutomatonSparseTransitionParser.h | 4 +-- ...NondeterministicSparseTransitionParser.cpp | 4 +-- .../NondeterministicSparseTransitionParser.h | 2 +- src/parser/SparseStateRewardParser.cpp | 2 +- src/utility/cstring.cpp | 18 +++++------ src/utility/cstring.h | 12 +++---- 15 files changed, 94 insertions(+), 50 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 211a3aecf..a5150c05a 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -668,7 +668,7 @@ namespace storm { // Finalize the resulting matrices. modelComponents.transitionMatrix = transitionMatrixBuilder.build(); - modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount()); + modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index dffdd030a..58ee0abbd 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -34,7 +34,7 @@ namespace storm { } MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // First pass: Count the number of propositions. bool foundDecl = false, foundEnd = false; diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 808d36f0b..b4e72c4cf 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -12,6 +12,7 @@ #include "src/parser/DeterministicModelParser.h" #include "src/parser/NondeterministicModelParser.h" #include "src/parser/MarkovAutomatonParser.h" +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/WrongFormatException.h" #include "src/utility/cstring.h" @@ -74,25 +75,30 @@ namespace storm { // Open the file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + + LOG_THROW(file.getDataSize() >= hintLength, storm::exceptions::WrongFormatException, "File too short to be readable."); + char const* fileData = file.getData(); + + char filehintBuffer[hintLength + 1]; + memcpy(filehintBuffer, fileData, hintLength); + filehintBuffer[hintLength] = 0; // Find and read in the hint. - char hint[65]; - // %60s => The input hint can be AT MOST 60 chars long. + std::string formatString = "%" + std::to_string(hintLength) + "s"; + char hint[5]; #ifdef WINDOWS - sscanf_s(buf, "%60s", hint, sizeof(hint)); + sscanf_s(filehintBuffer, formatString.c_str(), hint, hintLength + 1); #else - sscanf(buf, "%60s", hint); + int ret = sscanf(filehintBuffer, formatString.c_str(), hint); #endif - for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); - + // Check if the hint value is known and store the appropriate enum value. - if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; - else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; - else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; - else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; - else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; + if (strcmp(hint, "DTMC") == 0) hintType = storm::models::DTMC; + else if (strcmp(hint, "CTMC") == 0) hintType = storm::models::CTMC; + else if (strcmp(hint, "MDP") == 0) hintType = storm::models::MDP; + else if (strcmp(hint, "CTMDP") == 0) hintType = storm::models::CTMDP; + else if (strcmp(hint, "MA") == 0) hintType = storm::models::MA; return hintType; } diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 993cbe6bb..c3bab16e6 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -47,6 +47,8 @@ namespace storm { std::string const & transitionRewardFilename = ""); private: + // Define the maximal length of a hint in the file. + static constexpr uint_fast64_t hintLength = 10; /*! * Opens the given file and parses the file format hint. diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 67e31484f..8f81685b6 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -53,7 +53,7 @@ namespace storm { // Open file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Perform first pass, i.e. count entries that are not zero. bool insertDiagonalEntriesIfMissing = !isRewardFile; @@ -115,6 +115,23 @@ namespace storm { buf = trimWhitespaces(buf); } } else { + // Read first row and add self-loops if necessary. + char const* tmp; + row = checked_strtol(buf, &tmp); + + if (row > 0) { + for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { + hadDeadlocks = true; + if (fixDeadlocks) { + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); + // Before throwing the appropriate exception we will give notice of all deadlock states. + } + } + } + while (buf[0] != '\0') { // Read next transition. @@ -139,7 +156,6 @@ namespace storm { hadDeadlocks = true; if (fixDeadlocks) { resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); - rowHadDiagonalEntry = true; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); @@ -193,7 +209,7 @@ namespace storm { return result; } - DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, bool insertDiagonalEntriesIfMissing) { + DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) { DeterministicSparseTransitionParser::FirstPassResult result; @@ -207,6 +223,16 @@ namespace storm { // Check all transitions for non-zero diagonal entries and deadlock states. uint_fast64_t row, col, lastRow = 0, lastCol = -1; bool rowHadDiagonalEntry = false; + + // Read first row and reserve space for self-loops if necessary. + char const* tmp; + row = checked_strtol(buf, &tmp); + if (row > 0) { + for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } + } + while (buf[0] != '\0') { // Read the transition. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index e31ef2291..ede2e37ba 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -67,7 +67,7 @@ namespace storm { * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true); /* * The main parsing routine. diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp index 2b7e13a05..7abf526cf 100644 --- a/src/parser/MappedFile.cpp +++ b/src/parser/MappedFile.cpp @@ -42,15 +42,15 @@ namespace storm { LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file."); throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file."; } - - this->data = reinterpret_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); - if (this->data == reinterpret_cast(-1)) { + + this->data = static_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); + if (this->data == MAP_FAILED) { close(this->file); LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno)); throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno); } this->dataEnd = this->data + this->st.st_size; - #elif defined WINDOWS + #elif defined WINDOWS // Do file mapping for windows. // _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile() @@ -100,13 +100,17 @@ namespace storm { return fin.good(); } - char* MappedFile::getData() { + char const* MappedFile::getData() const { return data; } - char* MappedFile::getDataEnd() { + char const* MappedFile::getDataEnd() const { return dataEnd; } + + std::size_t MappedFile::getDataSize() const { + return this->getDataEnd() - this->getData(); + } } // namespace parser } // namespace storm diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h index 6de9877d4..4273d1c55 100644 --- a/src/parser/MappedFile.h +++ b/src/parser/MappedFile.h @@ -8,6 +8,7 @@ #ifndef STORM_PARSER_MAPPEDFILE_H_ #define STORM_PARSER_MAPPEDFILE_H_ +#include #include #include "src/utility/OsDetection.h" @@ -61,15 +62,20 @@ namespace storm { * * @return A pointer to the first character of the mapped file data. */ - char* getData(); + char const* getData() const; /*! * Returns a pointer to the end of the mapped file data. * * @return A pointer to the first position after the last character of the mapped file data. */ - char* getDataEnd(); + char const* getDataEnd() const; + /*! + * Returns the size of the mapped file data. + */ + std::size_t getDataSize() const; + private: //! A pointer to the mapped file content. diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 6e02df99d..fbfa9a1b2 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -12,7 +12,7 @@ namespace storm { using namespace storm::utility::cstring; - MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) { + MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -154,7 +154,7 @@ namespace storm { return result; } - MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) { + MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -271,7 +271,7 @@ namespace storm { // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); return secondPass(buf, firstPass(buf)); } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 798a9e0e3..1e1ebd1f0 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -85,7 +85,7 @@ namespace storm { * @param buffer The buffer that cointains the input. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer); + static FirstPassResult firstPass(char const* buffer); /*! * Performs the second pass on the input pointed to by the given buffer with the information of the first pass. @@ -94,7 +94,7 @@ namespace storm { * @param firstPassResult The result of the first pass performed on the same input. * @return A structure representing the result of the second pass. */ - static Result secondPass(char* buffer, FirstPassResult const& firstPassResult); + static Result secondPass(char const* buffer, FirstPassResult const& firstPassResult); }; } // namespace parser diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 5923f7778..116364856 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -50,7 +50,7 @@ namespace storm { // Open file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Perform first pass, i.e. obtain number of columns, rows and non-zero elements. NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation); @@ -200,7 +200,7 @@ namespace storm { return resultMatrix; } - NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { + NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char const* buf, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { // Check file header and extract number of transitions. diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index f75babbb7..85a5aac4f 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -74,7 +74,7 @@ namespace storm { * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); + static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); /*! * The main parsing routine. diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index e707dbe3b..364c364b0 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -29,7 +29,7 @@ namespace storm { } MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Create state reward vector with given state count. std::vector stateRewards(stateCount); diff --git a/src/utility/cstring.cpp b/src/utility/cstring.cpp index 2267fdf62..71bcbe69a 100644 --- a/src/utility/cstring.cpp +++ b/src/utility/cstring.cpp @@ -22,8 +22,8 @@ namespace cstring { * @param end New pointer will be written there * @return Result of strtol() */ -uint_fast64_t checked_strtol(const char* str, char** end) { - uint_fast64_t res = strtol(str, end, 10); +uint_fast64_t checked_strtol(char const* str, char const** end) { + uint_fast64_t res = strtol(str, const_cast(end), 10); if (str == *end) { LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number."); LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); @@ -40,8 +40,8 @@ uint_fast64_t checked_strtol(const char* str, char** end) { * @param end New pointer will be written there * @return Result of strtod() */ -double checked_strtod(const char* str, char** end) { - double res = strtod(str, end); +double checked_strtod(char const* str, char const** end) { + double res = strtod(str, const_cast(end)); if (str == *end) { LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number."); LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); @@ -56,7 +56,7 @@ double checked_strtod(const char* str, char** end) { * @param buf The string buffer to operate on. * @return A pointer to the first whitespace character. */ -char* skipWord(char* buf){ +char const* skipWord(char const* buf){ while(!isspace(*buf) && *buf != '\0') buf++; return buf; } @@ -67,7 +67,7 @@ char* skipWord(char* buf){ * @param buf The string buffer to operate on. * @return A pointer to the first non-whitespace character. */ -char* trimWhitespaces(char* buf) { +char const* trimWhitespaces(char const* buf) { while (isspace(*buf)) buf++; return buf; } @@ -75,15 +75,15 @@ char* trimWhitespaces(char* buf) { /*! * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). */ -char* forwardToLineEnd(char* buffer) { +char const* forwardToLineEnd(char const* buffer) { return buffer + strcspn(buffer, "\n\r\0"); } /*! * @brief Encapsulates the usage of function @strchr to forward to the next line */ -char* forwardToNextLine(char* buffer) { - char* lineEnd = forwardToLineEnd(buffer); +char const* forwardToNextLine(char const* buffer) { + char const* lineEnd = forwardToLineEnd(buffer); while((*lineEnd == '\n') || (*lineEnd == '\r')) lineEnd++; return lineEnd; } diff --git a/src/utility/cstring.h b/src/utility/cstring.h index ebe153f3b..65168e525 100644 --- a/src/utility/cstring.h +++ b/src/utility/cstring.h @@ -17,34 +17,34 @@ namespace storm { /*! * @brief Parses integer and checks, if something has been parsed. */ - uint_fast64_t checked_strtol(const char* str, char** end); + uint_fast64_t checked_strtol(const char* str, char const** end); /*! * @brief Parses floating point and checks, if something has been parsed. */ - double checked_strtod(const char* str, char** end); + double checked_strtod(const char* str, char const** end); /*! * @brief Skips all non whitespace characters until the next whitespace. */ - char* skipWord(char* buf); + char const* skipWord(char const* buf); /*! * @brief Skips common whitespaces in a string. */ - char* trimWhitespaces(char* buf); + char const* trimWhitespaces(char const* buf); /*! * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). */ - char* forwardToLineEnd(char* buffer); + char const* forwardToLineEnd(char const* buffer); /*! * @brief Encapsulates the usage of function @strchr to forward to the next line * * Note: All lines after the current, which do not contain any characters are skipped. */ - char* forwardToNextLine(char* buffer); + char const* forwardToNextLine(char const* buffer); } // namespace cstring } // namespace utility From 59dbc5a71e2f73010690f8c0de251b74e1569b4c Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Sep 2014 16:39:06 +0200 Subject: [PATCH 08/11] Fixed tests to comply with new requirement for hint in tra-file (needs to be at the very beginning, no prior white spaces). Former-commit-id: 60bfb720b8d4ad7422a439256bcb6f5ceea8b9ba --- test/functional/parser/MappedFileTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/functional/parser/MappedFileTest.cpp b/test/functional/parser/MappedFileTest.cpp index 8b4d7bfba..26ea73672 100644 --- a/test/functional/parser/MappedFileTest.cpp +++ b/test/functional/parser/MappedFileTest.cpp @@ -23,8 +23,8 @@ TEST(MappedFileTest, BasicFunctionality) { // Open a file and test if the content is loaded as expected. storm::parser::MappedFile file(STORM_CPP_TESTS_BASE_PATH "/functional/parser/testStringFile.txt"); std::string testString = "This is a test string."; - char * dataPtr = file.getData(); - for(char const * testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) { + char const* dataPtr = file.getData(); + for(char const* testStringPtr = testString.c_str(); testStringPtr - testString.c_str() < 22; testStringPtr++) { ASSERT_EQ(*testStringPtr, *dataPtr); dataPtr++; } From 552b3eaab7243e94771e4fabdadb8bd541f1e39a Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Sep 2014 17:20:38 +0200 Subject: [PATCH 09/11] Fixed SCC performance tests. Former-commit-id: a6b46e2fc5420fdd2514f011b13da557f9a409c3 --- .../storage/StronglyConnectedComponentDecompositionTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp index 83bc77de6..24c173265 100644 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -15,7 +15,7 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) { ASSERT_EQ(1290297ull, sccDecomposition.size()); ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); - ASSERT_EQ(1290297, sccDecomposition.size()); + ASSERT_EQ(437690, sccDecomposition.size()); ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); ASSERT_EQ(425040, sccDecomposition.size()); @@ -33,7 +33,7 @@ TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { ASSERT_EQ(2611835, sccDecomposition.size()); ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); - ASSERT_EQ(2611835, sccDecomposition.size()); + ASSERT_EQ(2, sccDecomposition.size()); ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); ASSERT_EQ(1, sccDecomposition.size()); From 2757dd31e2211b34a22639d32a35b28cb6e39eb1 Mon Sep 17 00:00:00 2001 From: PBerger Date: Fri, 12 Sep 2014 01:56:36 +0200 Subject: [PATCH 10/11] Removed illegal typename keywords in SparseMatrix.cpp. Refactored the constexpr in the AutoParser. @CDehnert: SparseMatrix Lines 59 to 65 - that cant be right. Former-commit-id: 21c458604c207a5c8f4d9da196d57b1094a496ea --- src/parser/AutoParser.cpp | 12 ++++++------ src/parser/AutoParser.h | 4 +++- src/storage/SparseMatrix.cpp | 10 +++++----- 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index b4e72c4cf..4c2a91fde 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -76,18 +76,18 @@ namespace storm { // Open the file. MappedFile file(filename.c_str()); - LOG_THROW(file.getDataSize() >= hintLength, storm::exceptions::WrongFormatException, "File too short to be readable."); + LOG_THROW(file.getDataSize() >= STORM_PARSER_AUTOPARSER_HINT_LENGTH, storm::exceptions::WrongFormatException, "File too short to be readable."); char const* fileData = file.getData(); - char filehintBuffer[hintLength + 1]; - memcpy(filehintBuffer, fileData, hintLength); - filehintBuffer[hintLength] = 0; + char filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1]; + memcpy(filehintBuffer, fileData, STORM_PARSER_AUTOPARSER_HINT_LENGTH); + filehintBuffer[STORM_PARSER_AUTOPARSER_HINT_LENGTH] = 0; // Find and read in the hint. - std::string formatString = "%" + std::to_string(hintLength) + "s"; + std::string formatString = "%" + std::to_string(STORM_PARSER_AUTOPARSER_HINT_LENGTH) + "s"; char hint[5]; #ifdef WINDOWS - sscanf_s(filehintBuffer, formatString.c_str(), hint, hintLength + 1); + sscanf_s(filehintBuffer, formatString.c_str(), hint, STORM_PARSER_AUTOPARSER_HINT_LENGTH + 1); #else int ret = sscanf(filehintBuffer, formatString.c_str(), hint); #endif diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index c3bab16e6..5041e2f3c 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -5,6 +5,8 @@ #include +#define STORM_PARSER_AUTOPARSER_HINT_LENGTH (10ull) + namespace storm { /*! @@ -48,7 +50,7 @@ namespace storm { private: // Define the maximal length of a hint in the file. - static constexpr uint_fast64_t hintLength = 10; + static uint_fast64_t hintLength; /*! * Opens the given file and parses the file format hint. diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 0b5846acc..f310c61ad 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -749,9 +749,9 @@ namespace storm { void SparseMatrix::multiplyWithVectorSequential(std::vector const& vector, std::vector& result) const { const_iterator it = this->begin(); const_iterator ite; - typename std::vector::const_iterator rowIterator = rowIndications.begin(); - typename std::vector::iterator resultIterator = result.begin(); - typename std::vector::iterator resultIteratorEnd = result.end(); + std::vector::const_iterator rowIterator = rowIndications.begin(); + std::vector::iterator resultIterator = result.begin(); + std::vector::iterator resultIteratorEnd = result.end(); for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero(); @@ -773,8 +773,8 @@ namespace storm { const_iterator ite; std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; - typename std::vector::iterator resultIterator = result.begin() + startRow; - typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + std::vector::iterator resultIterator = result.begin() + startRow; + std::vector::iterator resultIteratorEnd = result.begin() + endRow; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero(); From a0a8bf704a3db0fdf7aef2acaa57771e6015c8f8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Sep 2014 03:04:39 +0200 Subject: [PATCH 11/11] Fixed some minor issues in the sparse matrix. Former-commit-id: c7690b5a1395ea2b35fb50df32de286611cff610 --- src/storage/SparseMatrix.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index f310c61ad..010cc36bf 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -56,13 +56,13 @@ namespace storm { template SparseMatrixBuilder::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) { // Prepare the internal storage. - if (initialRowCountSet > 0) { + if (initialRowCountSet) { rowIndications.reserve(initialRowCount + 1); } - if (initialEntryCountSet > 0) { + if (initialEntryCountSet) { columnsAndValues.reserve(initialEntryCount); } - if (initialRowGroupCountSet > 0) { + if (initialRowGroupCountSet) { rowGroupIndices.reserve(initialRowGroupCount + 1); } rowIndications.push_back(0); @@ -750,8 +750,8 @@ namespace storm { const_iterator it = this->begin(); const_iterator ite; std::vector::const_iterator rowIterator = rowIndications.begin(); - std::vector::iterator resultIterator = result.begin(); - std::vector::iterator resultIteratorEnd = result.end(); + typename std::vector::iterator resultIterator = result.begin(); + typename std::vector::iterator resultIteratorEnd = result.end(); for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero(); @@ -773,8 +773,8 @@ namespace storm { const_iterator ite; std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; - std::vector::iterator resultIterator = result.begin() + startRow; - std::vector::iterator resultIteratorEnd = result.begin() + endRow; + typename std::vector::iterator resultIterator = result.begin() + startRow; + typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero();