diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index a859ea441..36c1bbe01 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -455,7 +455,7 @@ namespace storm { * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { + static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation& stateInformation, bool deterministicModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, storm::storage::SparseMatrixBuilder& transitionRewardMatrixBuilder) { std::vector nondeterministicChoiceIndices; std::vector> choiceLabels; @@ -480,7 +480,7 @@ namespace storm { // requested and issue an error otherwise. if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - transitionMatrix.addNextValue(currentRow, currentState, storm::utility::constantOne()); + transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne()); ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -528,13 +528,13 @@ namespace storm { choiceLabels.push_back(globalChoice.getChoiceLabels()); for (auto const& stateProbabilityPair : globalChoice) { - transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } } @@ -549,7 +549,7 @@ namespace storm { choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { - transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { @@ -563,7 +563,7 @@ namespace storm { // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } } @@ -576,7 +576,7 @@ namespace storm { choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { - transitionMatrix.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + transitionMatrixBuilder.addNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { @@ -590,7 +590,7 @@ namespace storm { // Add all transition rewards to the matrix and add dummy entry if there is none. if (stateToRewardMap.size() > 0) { for (auto const& stateRewardPair : stateToRewardMap) { - transitionRewardMatrix.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + transitionRewardMatrixBuilder.addNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); } } @@ -631,13 +631,15 @@ namespace storm { bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC; // Build the transition and reward matrices. - std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); + storm::storage::SparseMatrixBuilder transitionMatrixBuilder; + storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; + std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, transitionMatrixBuilder, transitionRewardMatrixBuilder); modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first); modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); // Finalize the resulting matrices. - modelComponents.transitionMatrix.finalize(); - modelComponents.transitionRewardMatrix.finalize(modelComponents.transitionMatrix.getRowCount()); + modelComponents.transitionMatrix = transitionMatrixBuilder.build(); + modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount()); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 26461f665..0ac15408b 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -90,7 +90,6 @@ public: return this->checkBoundedUntil(formula.getLeft().check(*this), formula.getRight().check(*this), formula.getBound(), qualitative); } - /*! * Computes the probability to satisfy phi until psi inside a given bound for each state in the model. * @@ -108,7 +107,7 @@ public: // If we identify the states that have probability 0 of reaching the target states, we can exclude them in the // further analysis. - storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), phiStates, psiStates, true, stepBound); + storm::storage::BitVector statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getBackwardTransitions(), phiStates, psiStates, true, stepBound); LOG4CPLUS_INFO(logger, "Found " << statesWithProbabilityGreater0.getNumberOfSetBits() << " 'maybe' states."); // Check if we already know the result (i.e. probability 0) for all initial states and @@ -264,9 +263,7 @@ public: // We need to identify the states which have to be taken out of the matrix, i.e. // all states that have probability 0 and 1 of satisfying the until-formula. - LOG4CPLUS_INFO(logger, "Running Prob01."); std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), phiStates, psiStates); - LOG4CPLUS_INFO(logger, "Done running Prob01."); storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); @@ -427,7 +424,7 @@ public: // Determine which states have a reward of infinity by definition. storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), trueStates, targetStates); + storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->getModel(), this->getModel().getBackwardTransitions(), trueStates, targetStates); infinityStates.complement(); storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index fa1731f10..b11fef9d4 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -160,7 +160,7 @@ class AbstractModel: public std::enable_shared_from_this> { } // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. - storm::storage::SparseMatrix dependencyGraph(numberOfStates, numberOfStates); + storm::storage::SparseMatrixBuilder dependencyGraphBuilder(numberOfStates, numberOfStates); for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < decomposition.size(); ++currentBlockIndex) { // Get the next block. @@ -181,13 +181,11 @@ class AbstractModel: public std::enable_shared_from_this> { // Now we can just enumerate all the target SCCs and insert the corresponding transitions. for (auto targetBlock : allTargetBlocks) { - dependencyGraph.addNextValue(currentBlockIndex, targetBlock, storm::utility::constantOne()); + dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::constantOne()); } } - // Finalize the matrix and return result. - dependencyGraph.finalize(true); - return dependencyGraph; + return dependencyGraphBuilder.build(); } /*! diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 2637f1be0..e05e1d3dd 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -28,10 +28,10 @@ namespace parser { */ DeterministicModelParserResultContainer parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::storage::SparseMatrix resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser(transitionSystemFile))); uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); + uint_fast64_t rowCount = resultTransitionSystem.getRowCount(); storm::models::AtomicPropositionsLabeling resultLabeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 223f0b218..4645286aa 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -201,7 +201,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st * The number of non-zero elements is computed by firstPass(). */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); - storm::storage::SparseMatrix resultMatrix(maxStateId + 1, maxStateId + 1, nonZeroEntryCount); + storm::storage::SparseMatrixBuilder matrixBuilder(maxStateId + 1, maxStateId + 1, nonZeroEntryCount); int_fast64_t row, lastRow = -1, col; double val; @@ -225,7 +225,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (lastRow != row) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + matrixBuilder.addNextValue(lastRow, lastRow, storm::utility::constantZero()); // LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); } else if (!isRewardMatrix) { // LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -236,7 +236,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (fixDeadlocks && !isRewardMatrix) { - resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + matrixBuilder.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 if (!isRewardMatrix) { @@ -253,20 +253,20 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st } else if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(row, row, storm::utility::constantZero()); + matrixBuilder.addNextValue(row, row, storm::utility::constantZero()); // LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); } else if (!isRewardMatrix) { // LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); } } - resultMatrix.addNextValue(row, col, val); + matrixBuilder.addNextValue(row, col, val); buf = trimWhitespaces(buf); } if (!rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + matrixBuilder.addNextValue(lastRow, lastRow, storm::utility::constantZero()); // LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); } else if (!isRewardMatrix) { // LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); @@ -275,12 +275,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; - /* - * Finalize Matrix. - */ - resultMatrix.finalize(); - - return resultMatrix; + return matrixBuilder.build(); } } // namespace parser diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 46bc05d2f..f2942f730 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -139,6 +139,7 @@ namespace storm { MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) { ResultType result(firstPassResult); + storm::storage::SparseMatrixBuilder matrixBuilder(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -159,7 +160,7 @@ namespace storm { if (fixDeadlocks) { for (uint_fast64_t index = lastsource + 1; index < source; ++index) { result.nondeterministicChoiceIndices[index] = currentChoice; - result.transitionMatrix.addNextValue(currentChoice, index, 1); + matrixBuilder.addNextValue(currentChoice, index, 1); ++currentChoice; } } else { @@ -218,7 +219,7 @@ namespace storm { double val = checked_strtod(buf, &buf); // Record the value as well as the exit rate in case of a Markovian choice. - result.transitionMatrix.addNextValue(currentChoice, target, val); + matrixBuilder.addNextValue(currentChoice, target, val); if (isMarkovianChoice) { result.exitRates[source] += val; } @@ -235,7 +236,7 @@ namespace storm { } // As we have added all entries at this point, we need to finalize the matrix. - result.transitionMatrix.finalize(); + result.transitionMatrix = matrixBuilder.build(); // Put a sentinel element at the end. result.nondeterministicChoiceIndices[firstPassResult.highestStateIndex + 1] = currentChoice; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 94542b64e..683605361 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -39,7 +39,7 @@ namespace storm { */ struct ResultType { - ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(firstPassResult.numberOfChoices, firstPassResult.highestStateIndex + 1, firstPassResult.numberOfNonzeroEntries), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { + ResultType(FirstPassResult const& firstPassResult) : transitionMatrix(), nondeterministicChoiceIndices(firstPassResult.highestStateIndex + 2), markovianChoices(firstPassResult.numberOfChoices), markovianStates(firstPassResult.highestStateIndex + 1), exitRates(firstPassResult.highestStateIndex + 1) { // Intentionally left empty. } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 1a44cffab..02a1e94f1 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -264,7 +264,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP * Those two values, as well as the number of nonzero elements, was been calculated in the first run. */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries."); - storm::storage::SparseMatrix matrix(choices, maxnode + 1, nonzero); + storm::storage::SparseMatrixBuilder matrixBuilder(choices, maxnode + 1, nonzero); /* * Create row mapping. @@ -325,7 +325,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP hadDeadlocks = true; if (fixDeadlocks) { rowMapping.at(node) = curRow; - matrix.addNextValue(curRow, node, 1); + matrixBuilder.addNextValue(curRow, node, 1); ++curRow; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); } else { @@ -343,7 +343,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP // Read target and value and write it to the matrix. target = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); - matrix.addNextValue(curRow, target, val); + matrixBuilder.addNextValue(curRow, target, val); lastsource = source; lastchoice = choice; @@ -379,12 +379,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly."; - /* - * Finalize matrix. - */ - matrix.finalize(); - - return std::make_pair(std::move(matrix), std::move(rowMapping)); + return std::make_pair(matrixBuilder.build(), std::move(rowMapping)); } } // namespace parser diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 6b9601f6f..18db8363c 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -10,6 +10,127 @@ extern log4cplus::Logger logger; namespace storm { namespace storage { + template + SparseMatrixBuilder::SparseMatrixBuilder(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0) { + this->prepareInternalStorage(); + } + + template + void SparseMatrixBuilder::addNextValue(uint_fast64_t row, uint_fast64_t column, T 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."; + } + + // 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 (uint_fast64_t 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 (uint_fast64_t i = lastRow + 1; i <= row; ++i) { + rowIndications.push_back(currentEntryCount); + } + } + 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); + if (!columnCountSet) { + columnCount = column + 1; + } + if (!rowCountSet) { + rowCount = row + 1; + } + } + ++currentEntryCount; + + } + + template + SparseMatrix SparseMatrixBuilder::build(uint_fast64_t overriddenRowCount, uint_fast64_t overriddenColumnCount) { + // 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::finalize: 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 (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { + rowIndications[i] = currentEntryCount; + } + } else { + if (!rowCountSet) { + rowCount = std::max(overriddenRowCount, rowCount); + } + for (uint_fast64_t 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 { + rowIndications.push_back(currentEntryCount); + if (!columnCountSet) { + columnCount = std::max(columnCount, overriddenColumnCount); + } + } + + entryCount = currentEntryCount; + } + + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues)); + } + + template + void SparseMatrixBuilder::prepareInternalStorage() { + // Only allocate the memory if the dimensions of the matrix are already known. + if (storagePreallocated) { + columnsAndValues = std::vector>(entryCount, std::make_pair(0, storm::utility::constantZero())); + rowIndications = std::vector(rowCount + 1, 0); + } else { + rowIndications.push_back(0); + } + } + template SparseMatrix::rows::rows(iterator begin, uint_fast64_t entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. @@ -41,37 +162,30 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t rows, uint_fast64_t columns, uint_fast64_t entries) : rowCountSet(rows != 0), rowCount(rows), columnCountSet(columns != 0), columnCount(columns), entryCount(entries), storagePreallocated(rows != 0 && columns != 0 && entries != 0), columnsAndValues(), rowIndications(), internalStatus(UNINITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { - prepareInternalStorage(); + SparseMatrix::SparseMatrix() : rowCount(0), columnCount(0), entryCount(0), columnsAndValues(), rowIndications() { + // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { + SparseMatrix::SparseMatrix(SparseMatrix const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCountSet(other.rowCountSet), rowCount(other.rowCount), columnCountSet(other.columnCountSet), columnCount(other.columnCount), entryCount(other.entryCount), storagePreallocated(other.storagePreallocated), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)), internalStatus(other.internalStatus), currentEntryCount(other.currentEntryCount), lastRow(other.lastRow), lastColumn(other.lastColumn) { + SparseMatrix::SparseMatrix(SparseMatrix&& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), columnsAndValues(std::move(other.columnsAndValues)), rowIndications(std::move(other.rowIndications)) { // Now update the source matrix - other.rowCountSet = false; other.rowCount = 0; - other.columnCountSet = false; other.columnCount = 0; other.entryCount = 0; - other.storagePreallocated = false; - other.internalStatus = MatrixStatus::UNINITIALIZED; - other.currentEntryCount = 0; - other.lastRow = 0; - other.lastColumn = 0; } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), storagePreallocated(true), columnsAndValues(columnsAndValues), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector> const& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(columnsAndValues), rowIndications(rowIndications) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), storagePreallocated(true), columnsAndValues(), rowIndications(rowIndications), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector const& rowIndications, std::vector const& columnIndications, std::vector const& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), columnsAndValues(), rowIndications(rowIndications) { if (columnIndications.size() != values.size()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::SparseMatrix: value and column vector length mismatch."; } @@ -87,12 +201,12 @@ namespace storm { } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), storagePreallocated(true), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector>&& columnsAndValues) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), columnsAndValues(std::move(columnsAndValues)), rowIndications(std::move(rowIndications)) { // Intentionally left empty. } template - SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector&& columnIndications, std::vector&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), columnsAndValues(), rowIndications(std::move(rowIndications)), internalStatus(INITIALIZED), currentEntryCount(0), lastRow(0), lastColumn(0) { + SparseMatrix::SparseMatrix(uint_fast64_t columnCount, std::vector&& rowIndications, std::vector&& columnIndications, std::vector&& values) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(values.size()), columnsAndValues(), rowIndications(std::move(rowIndications)) { if (columnIndications.size() != values.size()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::SparseMatrix: value and column vector length mismatch."; } @@ -111,19 +225,12 @@ namespace storm { SparseMatrix& SparseMatrix::operator=(SparseMatrix const& other) { // Only perform assignment if source and target are not the same. if (this != &other) { - rowCountSet = other.rowCountSet; rowCount = other.rowCount; - columnCountSet = other.columnCountSet; columnCount = other.columnCount; entryCount = other.entryCount; columnsAndValues = other.columnsAndValues; rowIndications = other.rowIndications; - - internalStatus = other.internalStatus; - currentEntryCount = other.currentEntryCount; - lastRow = other.lastRow; - lastColumn = other.lastColumn; } return *this; @@ -133,19 +240,12 @@ namespace storm { SparseMatrix& SparseMatrix::operator=(SparseMatrix&& other) { // Only perform assignment if source and target are not the same. if (this != &other) { - rowCountSet = other.rowCountSet; rowCount = other.rowCount; - columnCountSet = other.columnCountSet; columnCount = other.columnCount; entryCount = other.entryCount; columnsAndValues = std::move(other.columnsAndValues); rowIndications = std::move(other.rowIndications); - - internalStatus = other.internalStatus; - currentEntryCount = other.currentEntryCount; - lastRow = other.lastRow; - lastColumn = other.lastColumn; } return *this; @@ -157,22 +257,8 @@ namespace storm { return true; } - if (this->isInitialized() != other.isInitialized()) { - return false; - } - bool equalityResult = true; - // If the matrix is initialized, we only care about the contents and not the auxiliary members. - if (!this->isInitialized()) { - equalityResult &= rowCountSet == other.rowCountSet; - equalityResult &= columnCountSet == other.columnCountSet; - equalityResult &= internalStatus == other.internalStatus; - equalityResult &= currentEntryCount == other.currentEntryCount; - equalityResult &= lastRow == other.lastRow; - equalityResult &= lastColumn == other.lastColumn; - } - equalityResult &= rowCount == other.rowCount; equalityResult &= columnCount == other.columnCount; @@ -202,141 +288,23 @@ namespace storm { return equalityResult; } - template - void SparseMatrix::addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value) { - if (this->isInitialized()) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::addNextValue: adding an entry to an already initialized matrix."; - } - - // 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 SparseMatrix::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 SparseMatrix::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 SparseMatrix::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 SparseMatrix::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 SparseMatrix::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row."; - } - - // 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 (uint_fast64_t 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 (uint_fast64_t i = lastRow + 1; i <= row; ++i) { - rowIndications.push_back(currentEntryCount); - } - } - 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); - if (!columnCountSet) { - columnCount = column + 1; - } - if (!rowCountSet) { - rowCount = row + 1; - } - } - ++currentEntryCount; - } - - template - void SparseMatrix::finalize(uint_fast64_t overriddenRowCount, uint_fast64_t overridenColumnCount) { - // Check whether it's safe to finalize the matrix and throw error otherwise. - if (this->isInitialized()) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::finalize: matrix has already been initialized."; - } else if (storagePreallocated && currentEntryCount != entryCount) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::finalize: 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 (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) { - rowIndications[i] = currentEntryCount; - } - } else { - if (!rowCountSet) { - rowCount = std::max(overriddenRowCount, rowCount); - } - for (uint_fast64_t 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 { - rowIndications.push_back(currentEntryCount); - if (!columnCountSet) { - columnCount = std::max(columnCount, overridenColumnCount); - } - } - - entryCount = currentEntryCount; - internalStatus = INITIALIZED; - } - } - template uint_fast64_t SparseMatrix::getRowCount() const { - checkReady("getRowCount"); return rowCount; } template uint_fast64_t SparseMatrix::getColumnCount() const { - checkReady("getColumnCount"); return columnCount; } - template - bool SparseMatrix::isInitialized() const { - return internalStatus == INITIALIZED; - } - template uint_fast64_t SparseMatrix::getEntryCount() const { - checkReady("getEntryCount"); return entryCount; } template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { - checkReady("makeRowsAbsorbing"); for (auto row : rows) { makeRowAbsorbing(row, row); } @@ -344,7 +312,6 @@ namespace storm { template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices) { - checkReady("makeRowsAbsorbing"); for (auto rowGroup : rowGroupConstraint) { for (uint_fast64_t row = rowGroupIndices[rowGroup]; row < rowGroupIndices[rowGroup + 1]; ++row) { makeRowAbsorbing(row, rowGroup); @@ -354,7 +321,6 @@ namespace storm { template void SparseMatrix::makeRowAbsorbing(uint_fast64_t row, uint_fast64_t column) { - checkReady("makeRowAbsorbing"); if (row > rowCount) { throw storm::exceptions::OutOfRangeException() << "Illegal call to SparseMatrix::makeRowAbsorbing: access to row " << row << " is out of bounds."; } @@ -381,7 +347,6 @@ namespace storm { template T SparseMatrix::getConstrainedRowSum(uint_fast64_t row, storm::storage::BitVector const& constraint) const { - checkReady("getConstrainedRowSum"); T result(0); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { if (constraint.get(it->first)) { @@ -393,7 +358,6 @@ namespace storm { template std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint) const { - checkReady("getConstrainedRowSumVector"); std::vector result(rowConstraint.getNumberOfSetBits()); uint_fast64_t currentRowCount = 0; for (auto row : rowConstraint) { @@ -404,7 +368,6 @@ namespace storm { template std::vector SparseMatrix::getConstrainedRowSumVector(storm::storage::BitVector const& rowGroupConstraint, std::vector const& rowGroupIndices, storm::storage::BitVector const& columnConstraint) const { - checkReady("getConstrainedRowSumVector"); std::vector result; result.reserve(rowGroupConstraint.getNumberOfSetBits()); for (auto rowGroup : rowGroupConstraint) { @@ -433,7 +396,6 @@ namespace storm { template SparseMatrix SparseMatrix::getSubmatrix(storm::storage::BitVector const& rowGroupConstraint, storm::storage::BitVector const& columnConstraint, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { - checkReady("getSubmatrix"); // First, we need to determine the number of entries and the number of rows of the submatrix. uint_fast64_t subEntries = 0; uint_fast64_t subRows = 0; @@ -460,7 +422,7 @@ namespace storm { } // Create and initialize resulting matrix. - SparseMatrix result(subRows, columnConstraint.getNumberOfSetBits(), subEntries); + SparseMatrixBuilder matrixBuilder(subRows, columnConstraint.getNumberOfSetBits(), subEntries); // 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. @@ -496,27 +458,25 @@ namespace storm { if (index == it->first) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->first > index) { - result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); insertedDiagonalElement = true; } - result.addNextValue(rowCount, bitsSetBeforeIndex[it->first], it->second); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[it->first], it->second); } } if (insertDiagonalEntries && !insertedDiagonalElement) { - result.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); + matrixBuilder.addNextValue(rowCount, bitsSetBeforeIndex[index], storm::utility::constantZero()); } ++rowCount; } } - result.finalize(); - return result; + return matrixBuilder.build(); } template SparseMatrix SparseMatrix::getSubmatrix(std::vector const& rowGroupToRowIndexMapping, std::vector const& rowGroupIndices, bool insertDiagonalEntries) const { - checkReady("getSubmatrix"); // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for // diagonal entries if requested. uint_fast64_t subEntries = 0; @@ -538,7 +498,7 @@ namespace storm { } // Now create the matrix to be returned with the appropriate size. - SparseMatrix submatrix(rowGroupIndices.size() - 1, columnCount, subEntries); + SparseMatrixBuilder matrixBuilder(rowGroupIndices.size() - 1, columnCount, subEntries); // Copy over the selected lines from the source matrix. for (uint_fast64_t rowGroupIndex = 0, rowGroupIndexEnd = rowGroupToRowIndexMapping.size(); rowGroupIndex < rowGroupIndexEnd; ++rowGroupIndex) { @@ -552,25 +512,22 @@ namespace storm { if (it->first == rowGroupIndex) { insertedDiagonalElement = true; } else if (insertDiagonalEntries && !insertedDiagonalElement && it->first > rowGroupIndex) { - submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); + matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); insertedDiagonalElement = true; } - submatrix.addNextValue(rowGroupIndex, it->first, it->second); + matrixBuilder.addNextValue(rowGroupIndex, it->first, it->second); } if (insertDiagonalEntries && !insertedDiagonalElement) { - submatrix.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); + matrixBuilder.addNextValue(rowGroupIndex, rowGroupIndex, storm::utility::constantZero()); } } // Finalize created matrix and return result. - submatrix.finalize(); - return submatrix; + return matrixBuilder.build(); } template SparseMatrix SparseMatrix::transpose() const { - checkReady("transpose"); - uint_fast64_t rowCount = this->columnCount; uint_fast64_t columnCount = this->rowCount; uint_fast64_t entryCount = this->entryCount; @@ -620,8 +577,6 @@ namespace storm { template void SparseMatrix::invertDiagonal() { - checkReady("invertDiagonal"); - // Check if the matrix is square, because only then it makes sense to perform this // transformation. if (this->getRowCount() != this->getColumnCount()) { @@ -649,8 +604,6 @@ namespace storm { template void SparseMatrix::negateAllNonDiagonalEntries() { - checkReady("negateAllNonDiagonalEntries"); - // Check if the matrix is square, because only then it makes sense to perform this transformation. if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; @@ -668,8 +621,6 @@ namespace storm { template void SparseMatrix::deleteDiagonalEntries() { - checkReady("deleteDiagonalEntries"); - // Check if the matrix is square, because only then it makes sense to perform this transformation. if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::deleteDiagonalEntries: matrix is non-square."; @@ -687,15 +638,13 @@ namespace storm { template typename std::pair, storm::storage::SparseMatrix> SparseMatrix::getJacobiDecomposition() const { - checkReady("getJacobiDecomposition"); - if (rowCount != columnCount) { throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrix::invertDiagonal: matrix is non-square."; } storm::storage::SparseMatrix resultLU(*this); resultLU.deleteDiagonalEntries(); - storm::storage::SparseMatrix resultDinv(rowCount, columnCount, rowCount); + SparseMatrixBuilder dInvBuilder(rowCount, columnCount, rowCount); // Copy entries to the appropriate matrices. for (uint_fast64_t rowNumber = 0; rowNumber < rowCount; ++rowNumber) { @@ -710,17 +659,14 @@ namespace storm { break; } } - resultDinv.addNextValue(rowNumber, rowNumber, storm::utility::constantOne() / diagonalValue); + dInvBuilder.addNextValue(rowNumber, rowNumber, storm::utility::constantOne() / diagonalValue); } - resultDinv.finalize(); - return std::make_pair(std::move(resultLU), std::move(resultDinv)); + return std::make_pair(std::move(resultLU), dInvBuilder.build()); } template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const { - checkReady("getPointwiseProductRowSumVector"); - std::vector result(rowCount, storm::utility::constantZero()); // Iterate over all elements of the current matrix and either continue with the next element in case the @@ -746,7 +692,6 @@ namespace storm { template void SparseMatrix::multiplyWithVector(std::vector const& vector, std::vector& result) const { - checkReady("multiplyWithVector"); #ifdef STORM_HAVE_INTELTBB tbb::parallel_for(tbb::blocked_range(0, result.size()), tbbHelper_MatrixRowVectorScalarProduct, std::vector, T>(this, &vector, &result)); #else @@ -769,8 +714,6 @@ namespace storm { template uint_fast64_t SparseMatrix::getSizeInMemory() const { - checkReady("getSizeInMemory"); - uint_fast64_t size = sizeof(*this); // Add size of columns and values. @@ -784,67 +727,56 @@ namespace storm { template typename SparseMatrix::const_rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) const { - checkReady("getRows"); - return const_rows(this->columnsAndValues.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); + return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } template typename SparseMatrix::rows SparseMatrix::getRows(uint_fast64_t startRow, uint_fast64_t endRow) { - checkReady("getRows"); - return rows(this->columnsAndValues.data() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); + return rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow + 1] - this->rowIndications[startRow]); } template typename SparseMatrix::const_rows SparseMatrix::getRow(uint_fast64_t row) const { - checkReady("getRow"); return getRows(row, row); } template typename SparseMatrix::rows SparseMatrix::getRow(uint_fast64_t row) { - checkReady("getRow"); return getRows(row, row); } template typename SparseMatrix::const_iterator SparseMatrix::begin(uint_fast64_t row) const { - checkReady("begin"); - return this->columnsAndValues.data() + this->rowIndications[row]; + return this->columnsAndValues.begin() + this->rowIndications[row]; } template typename SparseMatrix::iterator SparseMatrix::begin(uint_fast64_t row) { - checkReady("begin"); - return this->columnsAndValues.data() + this->rowIndications[row]; + return this->columnsAndValues.begin() + this->rowIndications[row]; } template typename SparseMatrix::const_iterator SparseMatrix::end(uint_fast64_t row) const { - checkReady("end"); - return this->columnsAndValues.data() + this->rowIndications[row + 1]; + return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } template typename SparseMatrix::iterator SparseMatrix::end(uint_fast64_t row) { - checkReady("end"); - return this->columnsAndValues.data() + this->rowIndications[row + 1]; + return this->columnsAndValues.begin() + this->rowIndications[row + 1]; } template typename SparseMatrix::const_iterator SparseMatrix::end() const { - checkReady("end"); - return this->columnsAndValues.data() + this->rowIndications[rowCount]; + return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } template typename SparseMatrix::iterator SparseMatrix::end() { - checkReady("end"); - return this->columnsAndValues.data() + this->rowIndications[rowCount]; + return this->columnsAndValues.begin() + this->rowIndications[rowCount]; } template T SparseMatrix::getRowSum(uint_fast64_t row) const { - checkReady("getRowSum"); T sum = storm::utility::constantZero(); for (const_iterator it = this->begin(row), ite = this->end(row); it != ite; ++it) { sum += it->second; @@ -854,8 +786,6 @@ namespace storm { template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { - checkReady("isSubmatrixOf"); - // Check for matching sizes. if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; @@ -877,8 +807,6 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix) { - matrix.checkReady("operator<<"); - // Print column numbers in header. out << "\t\t"; for (uint_fast64_t i = 0; i < matrix.columnCount; ++i) { @@ -922,34 +850,17 @@ namespace storm { boost::hash_combine(result, rowCount); boost::hash_combine(result, columnCount); boost::hash_combine(result, entryCount); - boost::hash_combine(result, internalStatus); boost::hash_combine(result, boost::hash_range(columnsAndValues.begin(), columnsAndValues.end())); boost::hash_combine(result, boost::hash_range(rowIndications.begin(), rowIndications.end())); return result; } - template - void SparseMatrix::prepareInternalStorage() { - // Only allocate the memory if the dimensions of the matrix are already known. - if (storagePreallocated) { - columnsAndValues = std::vector>(entryCount, std::make_pair(0, storm::utility::constantZero())); - rowIndications = std::vector(rowCount + 1, 0); - } else { - rowIndications.push_back(0); - } - } - - template - void SparseMatrix::checkReady(std::string const& methodName) const { - if (!this->isInitialized()) { - throw storm::exceptions::InvalidStateException() << "Invalid call to SparseMatrix::" << methodName << ": matrix used for operation has not been initialized properly."; - } - } - - // Explicitly instantiate the matrix and the nested classes. + // Explicitly instantiate the builder and the matrix. + template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 5d5d66fa6..d4f481e04 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -40,6 +40,103 @@ namespace storm { class tbbHelper_MatrixRowVectorScalarProduct; #endif + // Forward declare matrix class. + template class SparseMatrix; + + /*! + * A class that can be used to build a sparse matrix by adding value by value. + */ + template + class SparseMatrixBuilder { + public: + /*! + * Constructs a sparse matrix builder producing a matrix with the given number of rows, columns and entries. + * + * @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. + */ + SparseMatrixBuilder(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0); + + /*! + * Sets the matrix entry at the given row and column to the given value. After all entries have been added, + * a call to finalize(false) is mandatory. + * + * Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and + * column by column. As multiple entries per column are admitted, consecutive calls to this method are + * admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are + * treated as empty. If these constraints are not met, an exception is thrown. + * + * @param row The row in which the matrix entry is to be set. + * @param column The column in which the matrix entry is to be set. + * @param value The value that is to be set at the specified row and column. + */ + void addNextValue(uint_fast64_t row, uint_fast64_t column, T const& value); + + /* + * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix + * may now be used. This must be called after all entries have been added to the matrix via addNextValue. + * + * @param overriddenRowCount If this is set to a value that is greater than the current number of rows, + * this will cause the finalize method to add empty rows at the end of the matrix until the given row count + * has been matched. Note that this will *not* override the row count that has been given upon construction + * (if any), but will only take effect if the matrix has been created without the number of rows given. + * @param overriddenColumnCount If this is set to a value that is greater than the current number of columns, + * this will cause the finalize method to set the number of columns to the given value. Note that this will + * *not* override the column count that has been given upon construction (if any), but will only take effect + * if the matrix has been created without the number of columns given. By construction, the matrix will have + * no entries in the columns that have been added this way. + */ + SparseMatrix build(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 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; + + // The number of rows of the matrix. + uint_fast64_t rowCount; + + // A flag indicating whether the number of columns was set upon construction. + bool columnCountSet; + + // The number of columns of the matrix. + uint_fast64_t columnCount; + + // The number of entries in the matrix. + uint_fast64_t entryCount; + + // 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; + + // A vector containing the indices at which each given row begins. This index is to be interpreted as an + // index in the valueStorage and the columnIndications vectors. Put differently, the values of the entries + // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last + // entry is not included anymore. + std::vector rowIndications; + + // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix + // with preallocated storage. + uint_fast64_t currentEntryCount; + + // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a + // matrix. + uint_fast64_t lastRow; + + // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an + // entry into a matrix. + uint_fast64_t lastColumn; + }; + /*! * A class that holds a possibly non-square matrix in the compressed row storage format. That is, it is supposed * to store non-zero entries only, but zeros may be explicitly stored if necessary for certain operations. @@ -68,8 +165,8 @@ namespace storm { friend class tbbHelper_MatrixRowVectorScalarProduct; #endif - typedef std::pair* iterator; - typedef std::pair const* const_iterator; + typedef typename std::vector>::iterator iterator; + typedef typename std::vector const>::const_iterator const_iterator; /*! * This class represents a number of consecutive rows of the matrix. @@ -151,14 +248,10 @@ namespace storm { enum MatrixStatus { UNINITIALIZED, INITIALIZED }; /*! - * Constructs a sparse matrix object with the given number of rows, columns and number of entries. - * - * @param rows The number of rows of the matrix. - * @param columns The number of columns of the matrix. - * @param entries The number of entries of the matrix. + * Constructs an empty sparse matrix. */ - SparseMatrix(uint_fast64_t rows = 0, uint_fast64_t columns = 0, uint_fast64_t entries = 0); - + SparseMatrix(); + /*! * Constructs a sparse matrix by performing a deep-copy of the given matrix. * @@ -233,37 +326,6 @@ namespace storm { */ bool operator==(SparseMatrix const& other) const; - /*! - * Sets the matrix entry at the given row and column to the given value. After all entries have been added, - * a call to finalize(false) is mandatory. - * - * Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and - * column by column. As multiple entries per column are admitted, consecutive calls to this method are - * admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are - * treated as empty. If these constraints are not met, an exception is thrown. - * - * @param row The row in which the matrix entry is to be set. - * @param column The column in which the matrix entry is to be set. - * @param value The value that is to be set at the specified row and column. - */ - void addNextValue(uint_fast64_t row, uint_fast64_t column,T const& value); - - /* - * Finalizes the sparse matrix to indicate that initialization process has been completed and the matrix - * may now be used. This must be called after all entries have been added to the matrix via addNextValue. - * - * @param overriddenRowCount If this is set to a value that is greater than the current number of rows, - * this will cause the finalize method to add empty rows at the end of the matrix until the given row count - * has been matched. Note that this will *not* override the row count that has been given upon construction - * (if any), but will only take effect if the matrix has been created without the number of rows given. - * @param overriddenColumnCount If this is set to a value that is greater than the current number of columns, - * this will cause the finalize method to set the number of columns to the given value. Note that this will - * *not* override the column count that has been given upon construction (if any), but will only take effect - * if the matrix has been created without the number of columns given. By construction, the matrix will have - * no entries in the columns that have been added this way. - */ - void finalize(uint_fast64_t overriddenRowCount = 0, uint_fast64_t overriddenColumnCount = 0); - /*! * Returns the number of rows of the matrix. * @@ -285,13 +347,6 @@ namespace storm { */ uint_fast64_t getEntryCount() const; - /*! - * Checks whether the matrix was initialized properly and is ready for further use. - * - * @return True iff the matrix was initialized properly and is ready for further use. - */ - bool isInitialized() const; - /*! * This function makes the given rows absorbing. * @@ -566,36 +621,15 @@ namespace storm { std::size_t hash() const; private: - /*! - * Prepares the internal storage of the matrix. 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 matrix - * will cause occasional reallocations. - */ - void prepareInternalStorage(); - - /*! - * Checks whether the matrix is properly initialized and throws an exception otherwise. - */ - void checkReady(std::string const& methodName) const; - - // A flag indicating whether the number of rows was set upon construction. - bool rowCountSet; - // The number of rows of the matrix. uint_fast64_t rowCount; - // A flag indicating whether the number of columns was set upon construction. - bool columnCountSet; - // The number of columns of the matrix. uint_fast64_t columnCount; // The number of entries in the matrix. uint_fast64_t entryCount; - // 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; @@ -604,22 +638,6 @@ namespace storm { // in row i are valueStorage[rowIndications[i]] to valueStorage[rowIndications[i + 1]] where the last // entry is not included anymore. std::vector rowIndications; - - // The internal status of the matrix. - MatrixStatus internalStatus; - - // Stores the current number of entries in the matrix. This is used for inserting an entry into a matrix - // with preallocated storage. - uint_fast64_t currentEntryCount; - - // Stores the row of the last entry in the matrix. This is used for correctly inserting an entry into a - // matrix. - uint_fast64_t lastRow; - - // Stores the column of the currently last entry in the matrix. This is used for correctly inserting an - // entry into a matrix. - uint_fast64_t lastColumn; - }; #ifdef STORM_HAVE_INTELTBB diff --git a/src/utility/graph.h b/src/utility/graph.h index c83e38c5e..fc9f02298 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -45,13 +45,10 @@ namespace storm { * @return A bit vector with all indices of states that have a probability greater than 0. */ template - storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { + storm::storage::BitVector performProbGreater0(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) { // Prepare the resulting bit vector. storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); - // Get the backwards transition relation from the model to ease the search. - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - // Add all psi states as the already satisfy the condition. statesWithProbabilityGreater0 |= psiStates; @@ -82,7 +79,7 @@ namespace storm { } for (typename storm::storage::SparseMatrix::const_iterator entryIt = backwardTransitions.begin(currentState), entryIte = backwardTransitions.end(currentState); entryIt != entryIte; ++entryIt) { - if (phiStates.get(entryIt->first) && (!statesWithProbabilityGreater0.get(entryIt->first) || (useStepBound && remainingSteps[entryIt->first] < currentStepBound - 1))) { + if (phiStates[entryIt->first] && (!statesWithProbabilityGreater0.get(entryIt->first) || (useStepBound && remainingSteps[entryIt->first] < currentStepBound - 1))) { // If we don't have a bound on the number of steps to take, just add the state to the stack. if (!useStepBound) { statesWithProbabilityGreater0.set(entryIt->first, true); @@ -117,8 +114,8 @@ namespace storm { * @return A bit vector with all indices of states that have a probability greater than 1. */ template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0); + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0) { + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~statesWithProbabilityGreater0); statesWithProbability1.complement(); return statesWithProbability1; } @@ -136,9 +133,9 @@ namespace storm { * @return A bit vector with all indices of states that have a probability greater than 1. */ template - storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { - storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, phiStates, psiStates); - storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, ~psiStates, ~(statesWithProbabilityGreater0)); + storm::storage::BitVector performProb1(storm::models::AbstractDeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::storage::BitVector statesWithProbabilityGreater0 = performProbGreater0(model, backwardTransitions, phiStates, psiStates); + storm::storage::BitVector statesWithProbability1 = performProbGreater0(model, backwardTransitions, ~psiStates, ~(statesWithProbabilityGreater0)); statesWithProbability1.complement(); return statesWithProbability1; } @@ -156,8 +153,9 @@ namespace storm { template static std::pair performProb01(storm::models::AbstractDeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { std::pair result; - result.first = performProbGreater0(model, phiStates, psiStates); - result.second = performProb1(model, phiStates, psiStates, result.first); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + result.first = performProbGreater0(model, backwardTransitions, phiStates, psiStates); + result.second = performProb1(model, backwardTransitions, phiStates, psiStates, result.first); result.first.complement(); return result; } diff --git a/src/utility/matrix.h b/src/utility/matrix.h index 21bbe2fe9..93a15b43e 100644 --- a/src/utility/matrix.h +++ b/src/utility/matrix.h @@ -20,7 +20,7 @@ namespace storm { */ template storm::storage::SparseMatrix applyScheduler(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::Scheduler const& scheduler) { - storm::storage::SparseMatrix result(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); + storm::storage::SparseMatrixBuilder matrixBuilder(nondeterministicChoiceIndices.size() - 1, transitionMatrix.getColumnCount()); for (uint_fast64_t state = 0; state < nondeterministicChoiceIndices.size() - 1; ++state) { if (scheduler.isChoiceDefined(state)) { @@ -33,17 +33,15 @@ namespace storm { // If a valid choice for this state is defined, we copy over the corresponding entries. typename storm::storage::SparseMatrix::const_rows selectedRow = transitionMatrix.getRow(choice); for (auto const& entry : selectedRow) { - result.addNextValue(state, entry.first, entry.second); + matrixBuilder.addNextValue(state, entry.first, entry.second); } } else { // If no valid choice for the state is defined, we insert a self-loop. - result.addNextValue(state, state, storm::utility::constantOne()); + matrixBuilder.addNextValue(state, state, storm::utility::constantOne()); } } - // Finalize the matrix creation and return result. - result.finalize(); - return result; + return matrixBuilder.build(); } } } diff --git a/test/functional/storage/SparseMatrixTest.cpp b/test/functional/storage/SparseMatrixTest.cpp index 8e48b1c7b..ad7e134d8 100644 --- a/test/functional/storage/SparseMatrixTest.cpp +++ b/test/functional/storage/SparseMatrixTest.cpp @@ -3,218 +3,228 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" -TEST(SparseMatrix, SimpleCreation) { - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix); - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(3)); - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(3, 4)); - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(3, 4, 5)); -} - -TEST(SparseMatrix, CreationWithMovingContents) { - ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2})); - storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2}); - ASSERT_EQ(3, matrix.getRowCount()); - ASSERT_EQ(4, matrix.getColumnCount()); - ASSERT_EQ(5, matrix.getEntryCount()); -} - -TEST(SparseMatrix, CreationWithDimensions) { - storm::storage::SparseMatrix matrix(3, 4, 5); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); +TEST(SparseMatrixBuilder, CreationWithDimensions) { + storm::storage::SparseMatrixBuilder matrixBuilder(3, 4, 5); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); } -TEST(SparseMatrix, CreationWithoutNumberOfEntries) { - storm::storage::SparseMatrix matrix(3, 4); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); - +TEST(SparseMatrixBuilder, CreationWithoutNumberOfEntries) { + storm::storage::SparseMatrixBuilder matrixBuilder(3, 4); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); } -TEST(SparseMatrix, CreationWithNumberOfRows) { - storm::storage::SparseMatrix matrix(3); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); - +TEST(SparseMatrixBuilder, CreationWithNumberOfRows) { + storm::storage::SparseMatrixBuilder matrixBuilder(3); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + ASSERT_EQ(3, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); } -TEST(SparseMatrix, CreationWithoutDimensions) { +TEST(SparseMatrixBuilder, CreationWithoutDimensions) { + storm::storage::SparseMatrixBuilder matrixBuilder; + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); - + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + ASSERT_EQ(2, matrix.getRowCount()); ASSERT_EQ(4, matrix.getColumnCount()); ASSERT_EQ(5, matrix.getEntryCount()); } -TEST(SparseMatrix, CopyConstruct) { - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); - - ASSERT_NO_THROW(storm::storage::SparseMatrix copy(matrix)); - storm::storage::SparseMatrix copy(matrix); - ASSERT_TRUE(matrix == copy); +TEST(SparseMatrixBuilder, AddNextValue) { + storm::storage::SparseMatrixBuilder matrixBuilder1(3, 4, 5); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 2, 1.2)); + ASSERT_THROW(matrixBuilder1.addNextValue(0, 4, 0.5), storm::exceptions::OutOfRangeException); + ASSERT_THROW(matrixBuilder1.addNextValue(3, 1, 0.5), storm::exceptions::OutOfRangeException); + + storm::storage::SparseMatrixBuilder matrixBuilder2(3, 4); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_THROW(matrixBuilder2.addNextValue(0, 4, 0.5), storm::exceptions::OutOfRangeException); + ASSERT_THROW(matrixBuilder2.addNextValue(3, 1, 0.5), storm::exceptions::OutOfRangeException); + + storm::storage::SparseMatrixBuilder matrixBuilder3(3); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(2, 4, 0.5)); + ASSERT_THROW(matrixBuilder3.addNextValue(3, 1, 0.2), storm::exceptions::OutOfRangeException); + + storm::storage::SparseMatrixBuilder matrixBuilder4; + ASSERT_NO_THROW(matrixBuilder4.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(1, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(2, 4, 0.5)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(3, 1, 0.2)); } -TEST(SparseMatrix, CopyAssign) { - storm::storage::SparseMatrix matrix; - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); - - ASSERT_NO_THROW(storm::storage::SparseMatrix copy = matrix); - storm::storage::SparseMatrix copy = matrix; - ASSERT_TRUE(matrix == copy); -} - -TEST(SparseMatrix, AddNextValue) { - storm::storage::SparseMatrix matrix(3, 4, 5); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_THROW(matrix.addNextValue(0, 4, 0.5), storm::exceptions::OutOfRangeException); - ASSERT_THROW(matrix.addNextValue(3, 1, 0.5), storm::exceptions::OutOfRangeException); - - storm::storage::SparseMatrix matrix2(3, 4); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_THROW(matrix2.addNextValue(0, 4, 0.5), storm::exceptions::OutOfRangeException); - ASSERT_THROW(matrix.addNextValue(3, 1, 0.5), storm::exceptions::OutOfRangeException); - - storm::storage::SparseMatrix matrix3(3); - ASSERT_NO_THROW(matrix3.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 2, 1.2)); - ASSERT_NO_THROW(matrix3.addNextValue(2, 4, 0.5)); - ASSERT_THROW(matrix3.addNextValue(3, 1, 0.2), storm::exceptions::OutOfRangeException); - - storm::storage::SparseMatrix matrix4; - ASSERT_NO_THROW(matrix4.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix4.addNextValue(1, 2, 1.2)); - ASSERT_NO_THROW(matrix4.addNextValue(2, 4, 0.5)); - ASSERT_NO_THROW(matrix4.addNextValue(3, 1, 0.2)); -} - -TEST(SparseMatrix, Finalize) { - storm::storage::SparseMatrix matrix(3, 4, 5); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_FALSE(matrix.isInitialized()); - ASSERT_NO_THROW(matrix.finalize()); - ASSERT_TRUE(matrix.isInitialized()); - - storm::storage::SparseMatrix matrix2(3, 4, 5); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_THROW(matrix2.finalize(), storm::exceptions::InvalidStateException); - +TEST(SparseMatrix, Build) { + storm::storage::SparseMatrixBuilder matrixBuilder1(3, 4, 5); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder1.addNextValue(1, 3, 0.2)); + ASSERT_NO_THROW(matrixBuilder1.build()); + + storm::storage::SparseMatrixBuilder matrixBuilder2(3, 4, 5); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_THROW(matrixBuilder2.build(), storm::exceptions::InvalidStateException); + + storm::storage::SparseMatrixBuilder matrixBuilder3; + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 3, 0.2)); storm::storage::SparseMatrix matrix3; - ASSERT_NO_THROW(matrix3.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix3.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix3.finalize()); + ASSERT_NO_THROW(matrix3 = matrixBuilder3.build()); ASSERT_EQ(2, matrix3.getRowCount()); ASSERT_EQ(4, matrix3.getColumnCount()); ASSERT_EQ(5, matrix3.getEntryCount()); + storm::storage::SparseMatrixBuilder matrixBuilder4; + ASSERT_NO_THROW(matrixBuilder4.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder4.addNextValue(1, 3, 0.2)); storm::storage::SparseMatrix matrix4; - ASSERT_NO_THROW(matrix4.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix4.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix4.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix4.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix4.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix4.finalize(4)); + ASSERT_NO_THROW(matrix4 = matrixBuilder4.build(4)); ASSERT_EQ(4, matrix4.getRowCount()); ASSERT_EQ(4, matrix4.getColumnCount()); ASSERT_EQ(5, matrix4.getEntryCount()); + storm::storage::SparseMatrixBuilder matrixBuilder5; + ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(1, 3, 0.2)); storm::storage::SparseMatrix matrix5; - ASSERT_NO_THROW(matrix5.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix5.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix5.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix5.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix5.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix5.finalize(0, 6)); + ASSERT_NO_THROW(matrix5 = matrixBuilder5.build(0, 6)); ASSERT_EQ(2, matrix5.getRowCount()); ASSERT_EQ(6, matrix5.getColumnCount()); ASSERT_EQ(5, matrix5.getEntryCount()); } -TEST(SparseMatrix, MakeAbsorbing) { - storm::storage::SparseMatrix matrix(3, 4, 5); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.2)); - ASSERT_NO_THROW(matrix.finalize()); +TEST(SparseMatrix, CreationWithMovingContents) { + ASSERT_NO_THROW(storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2})); + storm::storage::SparseMatrix matrix(4, {0, 2, 5, 5}, {1, 2, 0, 1, 3}, {1.0, 1.2, 0.5, 0.7, 0.2}); + ASSERT_EQ(3, matrix.getRowCount()); + ASSERT_EQ(4, matrix.getColumnCount()); + ASSERT_EQ(5, matrix.getEntryCount()); +} + +TEST(SparseMatrix, CopyConstruct) { + storm::storage::SparseMatrixBuilder matrixBuilder; + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + + ASSERT_NO_THROW(storm::storage::SparseMatrix copy(matrix)); + storm::storage::SparseMatrix copy(matrix); + ASSERT_TRUE(matrix == copy); +} + +TEST(SparseMatrix, CopyAssign) { + storm::storage::SparseMatrixBuilder matrixBuilder; + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + ASSERT_NO_THROW(storm::storage::SparseMatrix copy = matrix); + storm::storage::SparseMatrix copy = matrix; + ASSERT_TRUE(matrix == copy); +} + +TEST(SparseMatrix, MakeAbsorbing) { + storm::storage::SparseMatrixBuilder matrixBuilder(3, 4, 5); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.2)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + storm::storage::BitVector absorbingRows(3); absorbingRows.set(1); ASSERT_NO_THROW(matrix.makeRowsAbsorbing(absorbingRows)); - storm::storage::SparseMatrix matrix2(3, 4, 3); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 1)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder2(3, 4, 3); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 1)); + + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_TRUE(matrix == matrix2); } TEST(SparseMatrix, MakeRowGroupAbsorbing) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); std::vector rowGroupIndices = {0, 2, 4, 5}; @@ -223,33 +233,35 @@ TEST(SparseMatrix, MakeRowGroupAbsorbing) { ASSERT_NO_THROW(matrix.makeRowsAbsorbing(absorbingRowGroups, rowGroupIndices)); + storm::storage::SparseMatrixBuilder matrixBuilder2; + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 1, 1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 1, 1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 3, 0.3)); storm::storage::SparseMatrix matrix2; - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 1, 1)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 1, 1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix2.finalize()); + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_TRUE(matrix == matrix2); } TEST(SparseMatrix, ConstrainedRowSumVector) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); storm::storage::BitVector columnConstraint(4); columnConstraint.set(1); @@ -259,17 +271,18 @@ 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::SparseMatrix matrix2(5, 4, 9); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 3, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 3, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); std::vector rowGroupIndices = {0, 2, 4, 5}; @@ -286,17 +299,18 @@ TEST(SparseMatrix, ConstrainedRowSumVector) { } TEST(SparseMatrix, Submatrix) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); std::vector rowGroupIndices = {0, 1, 2, 4, 5}; @@ -311,11 +325,12 @@ TEST(SparseMatrix, Submatrix) { ASSERT_NO_THROW(storm::storage::SparseMatrix matrix2 = matrix.getSubmatrix(rowGroupConstraint, columnConstraint, rowGroupIndices, false)); storm::storage::SparseMatrix matrix2 = matrix.getSubmatrix(rowGroupConstraint, columnConstraint, rowGroupIndices, false); - storm::storage::SparseMatrix matrix3(3, 2, 3); - ASSERT_NO_THROW(matrix3.addNextValue(0, 0, 0.5)); - ASSERT_NO_THROW(matrix3.addNextValue(2, 0, 0.1)); - ASSERT_NO_THROW(matrix3.addNextValue(2, 1, 0.3)); - ASSERT_NO_THROW(matrix3.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder3(3, 2, 3); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(2, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(2, 1, 0.3)); + storm::storage::SparseMatrix matrix3; + ASSERT_NO_THROW(matrix3 = matrixBuilder3.build()); ASSERT_TRUE(matrix2 == matrix3); @@ -324,132 +339,142 @@ TEST(SparseMatrix, Submatrix) { ASSERT_NO_THROW(storm::storage::SparseMatrix matrix4 = matrix.getSubmatrix(rowGroupToIndexMapping, rowGroupIndices)); storm::storage::SparseMatrix matrix4 = matrix.getSubmatrix(rowGroupToIndexMapping, rowGroupIndices); - storm::storage::SparseMatrix matrix5(4, 4, 8); - ASSERT_NO_THROW(matrix5.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix5.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix5.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix5.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix5.addNextValue(2, 2, 1.1)); - ASSERT_NO_THROW(matrix5.addNextValue(3, 0, 0.1)); - ASSERT_NO_THROW(matrix5.addNextValue(3, 1, 0.2)); - ASSERT_NO_THROW(matrix5.addNextValue(3, 3, 0.3)); - ASSERT_NO_THROW(matrix5.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder5(4, 4, 8); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(2, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(3, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(3, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder5.addNextValue(3, 3, 0.3)); + storm::storage::SparseMatrix matrix5; + ASSERT_NO_THROW(matrix5 = matrixBuilder5.build()); ASSERT_TRUE(matrix4 == matrix5); } TEST(SparseMatrix, Transpose) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); ASSERT_NO_THROW(storm::storage::SparseMatrix transposeResult = matrix.transpose()); storm::storage::SparseMatrix transposeResult = matrix.transpose(); - storm::storage::SparseMatrix matrix2(4, 5, 9); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 4, 0.1)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 4, 0.2)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 0, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 3, 1.1)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 4, 0.3)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder2(4, 5, 9); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 4, 0.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 4, 0.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 0, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 3, 1.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 4, 0.3)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_TRUE(transposeResult == matrix2); } TEST(SparseMatrix, EquationSystem) { - storm::storage::SparseMatrix matrix(4, 4, 7); - ASSERT_NO_THROW(matrix.addNextValue(0, 0, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(2, 2, 0.99)); - ASSERT_NO_THROW(matrix.addNextValue(3, 3, 0.11)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(4, 4, 7); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.99)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 3, 0.11)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); ASSERT_NO_THROW(matrix.convertToEquationSystem()); - storm::storage::SparseMatrix matrix2(4, 4, 7); - ASSERT_NO_THROW(matrix2.addNextValue(0, 0, 1 - 1.1)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, -1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 1 - 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 3, -0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 0, -0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 2, 1 - 0.99)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 3, 1 - 0.11)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder2(4, 4, 7); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 0, 1 - 1.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, -1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 1 - 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 3, -0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 0, -0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 2, 1 - 0.99)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 3, 1 - 0.11)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_TRUE(matrix == matrix2); } TEST(SparseMatrix, JacobiDecomposition) { - storm::storage::SparseMatrix matrix(4, 4, 7); - ASSERT_NO_THROW(matrix.addNextValue(0, 0, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 3, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(2, 2, 0.99)); - ASSERT_NO_THROW(matrix.addNextValue(3, 3, 0.11)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(4, 4, 7); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 0, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 3, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, 0.99)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 3, 0.11)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); ASSERT_NO_THROW(matrix.getJacobiDecomposition()); std::pair, storm::storage::SparseMatrix> jacobiDecomposition = matrix.getJacobiDecomposition(); - storm::storage::SparseMatrix LU(4, 4, 3); - ASSERT_NO_THROW(LU.addNextValue(0, 1, 1.2)); - ASSERT_NO_THROW(LU.addNextValue(1, 3, 0.7)); - ASSERT_NO_THROW(LU.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(LU.finalize()); - - storm::storage::SparseMatrix Dinv(4, 4, 4); - ASSERT_NO_THROW(Dinv.addNextValue(0, 0, 1 / 1.1)); - ASSERT_NO_THROW(Dinv.addNextValue(1, 1, 1 / 0.5)); - ASSERT_NO_THROW(Dinv.addNextValue(2, 2, 1 / 0.99)); - ASSERT_NO_THROW(Dinv.addNextValue(3, 3, 1 / 0.11)); - ASSERT_NO_THROW(Dinv.finalize()); - - ASSERT_TRUE(LU == jacobiDecomposition.first); - ASSERT_TRUE(Dinv == jacobiDecomposition.second); + storm::storage::SparseMatrixBuilder luBuilder(4, 4, 3); + ASSERT_NO_THROW(luBuilder.addNextValue(0, 1, 1.2)); + ASSERT_NO_THROW(luBuilder.addNextValue(1, 3, 0.7)); + ASSERT_NO_THROW(luBuilder.addNextValue(2, 0, 0.5)); + storm::storage::SparseMatrix lu; + ASSERT_NO_THROW(lu = luBuilder.build()); + + storm::storage::SparseMatrixBuilder dinvBuilder(4, 4, 4); + ASSERT_NO_THROW(dinvBuilder.addNextValue(0, 0, 1 / 1.1)); + ASSERT_NO_THROW(dinvBuilder.addNextValue(1, 1, 1 / 0.5)); + ASSERT_NO_THROW(dinvBuilder.addNextValue(2, 2, 1 / 0.99)); + ASSERT_NO_THROW(dinvBuilder.addNextValue(3, 3, 1 / 0.11)); + storm::storage::SparseMatrix dinv; + ASSERT_NO_THROW(dinv = dinvBuilder.build()); + + ASSERT_TRUE(lu == jacobiDecomposition.first); + ASSERT_TRUE(dinv == jacobiDecomposition.second); } TEST(SparseMatrix, PointwiseMultiplicationVector) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); - - storm::storage::SparseMatrix matrix2(5, 4, 9); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + + storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_NO_THROW(std::vector pointwiseProductRowSums = matrix.getPointwiseProductRowSumVector(matrix2)); std::vector pointwiseProductRowSums = matrix.getPointwiseProductRowSumVector(matrix2); @@ -459,17 +484,18 @@ TEST(SparseMatrix, PointwiseMultiplicationVector) { } TEST(SparseMatrix, MatrixVectorMultiply) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); std::vector x = {1, 0.3, 1.4, 7.1}; std::vector result(matrix.getRowCount()); @@ -481,17 +507,18 @@ TEST(SparseMatrix, MatrixVectorMultiply) { } TEST(SparseMatrix, Iteration) { - storm::storage::SparseMatrix matrix(5, 4, 9); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(2, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 9); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); for (auto const& entry : matrix.getRow(4)) { if (entry.first == 0) { @@ -519,50 +546,54 @@ TEST(SparseMatrix, Iteration) { } TEST(SparseMatrix, RowSum) { - storm::storage::SparseMatrix matrix(5, 4, 8); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 8); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); ASSERT_EQ(0, matrix.getRowSum(2)); ASSERT_EQ(0.1+0.2+0.3, matrix.getRowSum(4)); } TEST(SparseMatrix, IsSubmatrix) { - storm::storage::SparseMatrix matrix(5, 4, 8); - ASSERT_NO_THROW(matrix.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix.addNextValue(0, 2, 1.2)); - ASSERT_NO_THROW(matrix.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix.addNextValue(3, 2, 1.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix.addNextValue(4, 3, 0.3)); - ASSERT_NO_THROW(matrix.finalize()); - - storm::storage::SparseMatrix matrix2(5, 4, 5); - ASSERT_NO_THROW(matrix2.addNextValue(0, 1, 1.0)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix2.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix2.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix2.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder(5, 4, 8); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 1.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 1, 0.2)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(4, 3, 0.3)); + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); + + storm::storage::SparseMatrixBuilder matrixBuilder2(5, 4, 5); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(0, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder2.addNextValue(4, 1, 0.2)); + storm::storage::SparseMatrix matrix2; + ASSERT_NO_THROW(matrix2 = matrixBuilder2.build()); ASSERT_TRUE(matrix2.isSubmatrixOf(matrix)); - storm::storage::SparseMatrix matrix3(5, 4, 5); - ASSERT_NO_THROW(matrix3.addNextValue(0, 3, 1.0)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 0, 0.5)); - ASSERT_NO_THROW(matrix3.addNextValue(1, 1, 0.7)); - ASSERT_NO_THROW(matrix3.addNextValue(4, 0, 0.1)); - ASSERT_NO_THROW(matrix3.addNextValue(4, 1, 0.2)); - ASSERT_NO_THROW(matrix3.finalize()); + storm::storage::SparseMatrixBuilder matrixBuilder3(5, 4, 5); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(0, 3, 1.0)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 0, 0.5)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(1, 1, 0.7)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(4, 0, 0.1)); + ASSERT_NO_THROW(matrixBuilder3.addNextValue(4, 1, 0.2)); + storm::storage::SparseMatrix matrix3; + ASSERT_NO_THROW(matrix3 = matrixBuilder3.build()); ASSERT_FALSE(matrix3.isSubmatrixOf(matrix)); ASSERT_FALSE(matrix3.isSubmatrixOf(matrix2)); diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 5bff9383a..6bc0042b5 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -12,6 +12,7 @@ TEST(GraphTest, PerformProb01) { storm::storage::BitVector trueStates(dtmc->getNumberOfStates(), true); LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); + std::pair prob01(storm::utility::graph::performProb01(*dtmc, trueStates, storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1")))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414ull); diff --git a/test/performance/storage/SparseMatrixTest.cpp b/test/performance/storage/SparseMatrixTest.cpp index 794d942ec..40a510e36 100644 --- a/test/performance/storage/SparseMatrixTest.cpp +++ b/test/performance/storage/SparseMatrixTest.cpp @@ -2,13 +2,15 @@ #include "src/storage/SparseMatrix.h" TEST(SparseMatrix, Iteration) { - storm::storage::SparseMatrix matrix; + storm::storage::SparseMatrixBuilder matrixBuilder; for (uint_fast64_t row = 0; row < 10000; ++row) { for (uint_fast64_t column = 0; column < row; ++column) { - ASSERT_NO_THROW(matrix.addNextValue(row, column, row+column)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, row+column)); } } - ASSERT_NO_THROW(matrix.finalize()); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); for (uint_fast64_t row = 0; row < matrix.getRowCount(); ++row) { for (auto const& entry : matrix.getRow(row)) { @@ -21,13 +23,15 @@ TEST(SparseMatrix, Iteration) { } TEST(SparseMatrix, Multiplication) { - storm::storage::SparseMatrix matrix; + storm::storage::SparseMatrixBuilder matrixBuilder; for (uint_fast64_t row = 0; row < 2000; ++row) { for (uint_fast64_t column = 0; column < row; ++column) { - ASSERT_NO_THROW(matrix.addNextValue(row, column, row+column)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(row, column, row+column)); } } - ASSERT_NO_THROW(matrix.finalize()); + + storm::storage::SparseMatrix matrix; + ASSERT_NO_THROW(matrix = matrixBuilder.build()); std::vector x(matrix.getColumnCount(), 1.0); std::vector result(matrix.getRowCount());