From 6a80348150baa64da092fd0a8b7654237b547c8d Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 8 Sep 2015 15:35:19 +0200 Subject: [PATCH] fixed issue related to row groups in sparse matrix and adapted the affected calling sites Former-commit-id: 96c6fd7e5916277966035ebec1fa802b8da4e7bd --- ...NondeterministicSparseTransitionParser.cpp | 21 +++++----- src/solver/GameSolver.cpp | 33 ++++++++------- src/solver/SymbolicGameSolver.cpp | 8 ++-- src/storage/SparseMatrix.cpp | 32 ++++++++++---- src/storage/prism/Program.cpp | 1 - src/utility/ConstantsComparator.cpp | 4 +- src/utility/constants.cpp | 42 ++++++++++--------- src/utility/solver.cpp | 13 +++--- src/utility/solver.h | 16 ++++++- 9 files changed, 104 insertions(+), 66 deletions(-) diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 3136bc36f..421f3b8cc 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -117,15 +117,21 @@ namespace storm { // If we have switched the source state, we possibly need to insert the rows of the last // source state. if (source != lastSource) { - curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) -(lastChoice + 1); + curRow += ((modelInformation.getRowGroupIndices())[lastSource + 1] - (modelInformation.getRowGroupIndices())[lastSource]) - (lastChoice + 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic - // choices. + // choices and create the row groups. for (uint_fast64_t i = lastSource + 1; i < source; ++i) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[i]); curRow += ((modelInformation.getRowGroupIndices())[i + 1] - (modelInformation.getRowGroupIndices())[i]); } + // If we moved to the next source, we need to open the next row group. + if (source != lastSource) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[source]); + } + // If we advanced to the next state, but skipped some choices, we have to reserve rows // for them if (source != lastSource) { @@ -155,7 +161,7 @@ namespace storm { } } if (source != lastSource) { - // Add create a new rowGroup for the source, if this is the first choice we encounter for this state. + // Create a new rowGroup for the source, if this is the first choice we encounter for this state. matrixBuilder.newRowGroup(curRow); } } @@ -178,13 +184,8 @@ namespace storm { // Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices. if (isRewardFile) { - // We already have rowGroup 0. - for (uint_fast64_t index = 1; index < modelInformation.getRowGroupIndices().size() - 1; index++) { - matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[index]); - } - } else { - for (uint_fast64_t node = lastSource + 1; node <= firstPass.highestStateIndex; node++) { - matrixBuilder.newRowGroup(curRow + 1); + for (uint_fast64_t node = lastSource + 1; node < modelInformation.getRowGroupCount(); node++) { + matrixBuilder.newRowGroup(modelInformation.getRowGroupIndices()[node]); } } diff --git a/src/solver/GameSolver.cpp b/src/solver/GameSolver.cpp index ea87aa10b..752328e11 100644 --- a/src/solver/GameSolver.cpp +++ b/src/solver/GameSolver.cpp @@ -39,26 +39,27 @@ namespace storm { } for (uint_fast64_t pl1State = 0; pl1State < numberOfPlayer1States; ++pl1State) { - uint_fast64_t startRow = player1Matrix.getRowGroupIndices()[pl1State]; - uint_fast64_t endRow = player1Matrix.getRowGroupIndices()[pl1State + 1]; - storm::storage::SparseMatrix::const_rows relevantRows = player1Matrix.getRowGroup(pl1State); - storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); - storm::storage::SparseMatrix::const_iterator ite = relevantRows.end(); + if (relevantRows.getNumberOfEntries() > 0) { + storm::storage::SparseMatrix::const_iterator it = relevantRows.begin(); + storm::storage::SparseMatrix::const_iterator ite = relevantRows.end(); - // Set the first value. - tmpResult[pl1State] = player2Result[it->getColumn()]; - ++it; + // Set the first value. + tmpResult[pl1State] = player2Result[it->getColumn()]; + ++it; - // Now iterate through the different values and pick the extremal one. - if (player1Goal == OptimizationDirection::Minimize) { - for (; it != ite; ++it) { - tmpResult[pl1State] = std::min(tmpResult[pl1State], player2Result[it->getColumn()]); + // Now iterate through the different values and pick the extremal one. + if (player1Goal == OptimizationDirection::Minimize) { + for (; it != ite; ++it) { + tmpResult[pl1State] = std::min(tmpResult[pl1State], player2Result[it->getColumn()]); + } + } else { + for (; it != ite; ++it) { + tmpResult[pl1State] = std::max(tmpResult[pl1State], player2Result[it->getColumn()]); + } } } else { - for (; it != ite; ++it) { - tmpResult[pl1State] = std::max(tmpResult[pl1State], player2Result[it->getColumn()]); - } + tmpResult[pl1State] = storm::utility::zero(); } } @@ -67,7 +68,7 @@ namespace storm { std::swap(x, tmpResult); ++iterations; - } while (!converged); + } while (!converged && iterations < maximalNumberOfIterations); } template class GameSolver; diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp index 4c03732a8..ab439326c 100644 --- a/src/solver/SymbolicGameSolver.cpp +++ b/src/solver/SymbolicGameSolver.cpp @@ -26,7 +26,7 @@ namespace storm { uint_fast64_t iterations = 0; bool converged = false; - while (!converged && iterations < maximalNumberOfIterations) { + do { // Compute tmp = A * x + b storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); storm::dd::Add tmp = this->gameMatrix.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); @@ -34,12 +34,12 @@ namespace storm { // Now abstract from player 2 and player 1 variables. switch (player2Goal) { - case OptimizationDirection::Minimize: tmp.minAbstract(this->player2Variables); break; + case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player2Variables); break; case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break; } switch (player1Goal) { - case OptimizationDirection::Minimize: tmp.minAbstract(this->player1Variables); break; + case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player1Variables); break; case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break; } @@ -52,7 +52,7 @@ namespace storm { } ++iterations; - } + } while (!converged && iterations < maximalNumberOfIterations); return xCopy; } diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 4648950b3..4184109cb 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -1,4 +1,5 @@ #include +#include // To detect whether the usage of TBB is possible, this include is neccessary #include "storm-config.h" @@ -143,9 +144,18 @@ namespace storm { template void SparseMatrixBuilder::newRowGroup(index_type startingRow) { STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping."); - STORM_LOG_THROW(rowGroupIndices.empty() || startingRow >= rowGroupIndices.back(), storm::exceptions::InvalidStateException, "Illegal row group with negative size."); + STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size."); rowGroupIndices.push_back(startingRow); ++currentRowGroup; + + // Close all rows from the most recent one to the starting row. + for (index_type i = lastRow + 1; i <= startingRow; ++i) { + rowIndications.push_back(currentEntryCount); + } + + // Reset the most recently seen row/column to allow for proper insertion of the following elements. + lastRow = startingRow; + lastColumn = 0; } template @@ -156,7 +166,7 @@ namespace storm { rowCount = std::max(rowCount, initialRowCount); } rowCount = std::max(rowCount, overriddenRowCount); - + // If the current row count was overridden, we may need to add empty rows. for (index_type i = lastRow + 1; i < rowCount; ++i) { rowIndications.push_back(currentEntryCount); @@ -196,7 +206,7 @@ namespace storm { rowGroupIndices.push_back(rowCount); } } - + return SparseMatrix(columnCount, std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices), hasCustomRowGrouping); } @@ -1163,16 +1173,16 @@ namespace storm { // Explicitly instantiate the entry, builder and the matrix. // double template class MatrixEntry::index_type, double>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, double> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template std::vector SparseMatrix::getPointwiseProductRowSumVector(storm::storage::SparseMatrix const& otherMatrix) const; template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; - // float + // float template class MatrixEntry::index_type, float>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, float> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); @@ -1181,12 +1191,20 @@ namespace storm { // int template class MatrixEntry::index_type, int>; - template std::ostream& operator<<(std::ostream& out, MatrixEntry const& entry); + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, int> const& entry); template class SparseMatrixBuilder; template class SparseMatrix; template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + // state_type + template class MatrixEntry::index_type, storm::storage::sparse::state_type>; + template std::ostream& operator<<(std::ostream& out, MatrixEntry::index_type, storm::storage::sparse::state_type> const& entry); + template class SparseMatrixBuilder; + template class SparseMatrix; + template std::ostream& operator<<(std::ostream& out, SparseMatrix const& matrix); + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const; + #ifdef STORM_HAVE_CARL // Rat Function template class MatrixEntry::index_type, RationalFunction>; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index e62cfc114..9ac73881e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1011,7 +1011,6 @@ namespace storm { } // Now we are in a position to start the enumeration over all command variables. - uint_fast64_t modelCount = 0; solver->allSat(allCommandVariables, [&] (storm::solver::SmtSolver::ModelReference& modelReference) -> bool { // Now we need to reconstruct the chosen commands from the valuation of the command variables. std::vector>> chosenCommands(possibleCommands.size()); diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index aecfa39fb..5923b5284 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -2,6 +2,7 @@ #include #include +#include #include "src/utility/constants.h" #include "src/settings/SettingsManager.h" @@ -94,7 +95,8 @@ namespace storm { template class ConstantsComparator; template class ConstantsComparator; template class ConstantsComparator; - + template class ConstantsComparator; + #ifdef STORM_HAVE_CARL template class ConstantsComparator; template class ConstantsComparator; diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index f346d2fcc..bba5fd160 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -1,7 +1,7 @@ #include "src/utility/constants.h" -#include "src/storage/SparseMatrix.h" #include "src/storage/sparse/StateType.h" +#include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" @@ -83,27 +83,13 @@ namespace storm { return std::pow(value, exponent); } - template<> - double simplify(double value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - - template<> - float simplify(float value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. + template + ValueType simplify(ValueType value) { + // In the general case, we don't to anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. return value; } - template<> - int simplify(int value) { - // In the general case, we don't to anything here, but merely return the value. If something else is - // supposed to happen here, the templated function can be specialized for this particular type. - return value; - } - #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -201,7 +187,23 @@ namespace storm { template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); - + + template bool isOne(storm::storage::sparse::state_type const& value); + template bool isZero(storm::storage::sparse::state_type const& value); + template bool isConstant(storm::storage::sparse::state_type const& value); + + template storm::storage::sparse::state_type one(); + template storm::storage::sparse::state_type zero(); + template storm::storage::sparse::state_type infinity(); + + template storm::storage::sparse::state_type pow(storm::storage::sparse::state_type const& value, uint_fast64_t exponent); + + template storm::storage::sparse::state_type simplify(storm::storage::sparse::state_type value); + + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry); + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); + template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + #ifdef STORM_HAVE_CARL template bool isOne(RationalFunction const& value); template bool isZero(RationalFunction const& value); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index ef3744ff9..15d8a71ac 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,13 +1,13 @@ #include "src/utility/solver.h" -#include "src/solver/SymbolicGameSolver.h" - #include #include "src/solver/SymbolicLinearEquationSolver.h" #include "src/solver/SymbolicMinMaxLinearEquationSolver.h" +#include "src/solver/SymbolicGameSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" +#include "src/solver/GameSolver.h" #include "src/solver/NativeMinMaxLinearEquationSolver.h" #include "src/solver/GmmxxMinMaxLinearEquationSolver.h" @@ -102,8 +102,7 @@ namespace storm { template void MinMaxLinearEquationSolverFactory::setPreferredTechnique(storm::solver::MinMaxTechniqueSelection preferredTech) { this->prefTech = preferredTech; - } - + } template std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix, bool trackPolicy) const { @@ -133,6 +132,10 @@ namespace storm { } + template + std::unique_ptr> GameSolverFactory::create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const { + return std::unique_ptr>(new storm::solver::GameSolver(player1Matrix, player2Matrix)); + } std::unique_ptr LpSolverFactory::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const { storm::solver::LpSolverType t; @@ -192,7 +195,7 @@ namespace storm { template class GmmxxLinearEquationSolverFactory; template class NativeLinearEquationSolverFactory; template class MinMaxLinearEquationSolverFactory; - + template class GameSolverFactory; } } } \ No newline at end of file diff --git a/src/utility/solver.h b/src/utility/solver.h index 81e2d1d23..ed7528915 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/storage/dd/DdType.h" #include "src/solver/SolverSelectionOptions.h" @@ -13,13 +14,15 @@ namespace storm { template class SymbolicGameSolver; template class SymbolicLinearEquationSolver; template class SymbolicMinMaxLinearEquationSolver; + template class GameSolver; template class LinearEquationSolver; template class MinMaxLinearEquationSolver; class LpSolver; class SmtSolver; template class NativeLinearEquationSolver; - enum class NativeLinearEquationSolverSolutionMethod; + enum class + NativeLinearEquationSolverSolutionMethod; } namespace storage { @@ -93,7 +96,7 @@ namespace storm { public: MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection solverType = storm::solver::EquationSolverTypeSelection::FROMSETTINGS); /*! - * Creates a new nondeterministic linear equation solver instance with the given matrix. + * Creates a new min/max linear equation solver instance with the given matrix. */ virtual std::unique_ptr> create(storm::storage::SparseMatrix const& matrix, bool trackPolicy = false) const; void setSolverType(storm::solver::EquationSolverTypeSelection solverType); @@ -106,6 +109,15 @@ namespace storm { /// Notice that we save the selection enum here, which allows different solvers to use different techniques. storm::solver::MinMaxTechniqueSelection prefTech; }; + + template + class GameSolverFactory { + public: + /*! + * Creates a new game solver instance with the given matrices. + */ + virtual std::unique_ptr> create(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix) const; + }; class LpSolverFactory { public: