From dd399c5f85714253e5097781cb526520b36de22e Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 11 Apr 2015 17:55:45 +0200 Subject: [PATCH] Finalized hybrid MDP model checker. It passes its tests now. Former-commit-id: 47de0b9433c3db6b84f84fe848a0d8df7bfb0056 --- .../prctl/HybridMdpPrctlModelChecker.cpp | 44 ++-- .../prctl/SparseMdpPrctlModelChecker.cpp | 1 + src/storage/dd/CuddAdd.cpp | 201 ++++++++++++++++-- src/storage/dd/CuddAdd.h | 86 ++++++-- .../GmmxxHybridMdpPrctlModelCheckerTest.cpp | 190 +++++++++++++++++ .../NativeHybridMdpPrctlModelCheckerTest.cpp | 30 +-- test/functional/storage/CuddDdTest.cpp | 4 +- 7 files changed, 486 insertions(+), 70 deletions(-) create mode 100644 test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index 0893a8ac4..f54bed203 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -70,19 +70,20 @@ namespace storm { storm::dd::Add subvector = submatrix * prob1StatesAsColumn; subvector = subvector.sumAbstract(model.getColumnVariables()); - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). + // Before cutting the non-maybe columns, we need to compute the sizes of the row groups. + std::vector rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector(odd); + + // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); // Translate the symbolic matrix/vector to their explicit representations and solve the equation system. - storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); + std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); - solver->solveEquationSystem(minimize, x, b); + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + solver->solveEquationSystem(minimize, x, explicitRepresentation.second); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x)); @@ -138,7 +139,7 @@ namespace storm { statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates); } storm::dd::Bdd maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates(); - + // If there are maybe states, we need to perform matrix-vector multiplications. if (!maybeStates.isZero()) { // Create the ODD for the translation between symbolic and explicit storage. @@ -156,6 +157,9 @@ namespace storm { storm::dd::Add prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Add subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); + // Before cutting the non-maybe columns, we need to compute the sizes of the row groups. + std::vector rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector(odd); + // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -163,11 +167,10 @@ namespace storm { std::vector x(maybeStates.getNonZeroCount(), storm::utility::zero()); // Translate the symbolic matrix/vector to their explicit representations. - storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); + std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); - solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + solver->performMatrixVectorMultiplication(minimize, x, &explicitRepresentation.second, stepBound); // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.toAdd(), maybeStates, odd, x)); @@ -259,9 +262,9 @@ namespace storm { storm::dd::Bdd infinityStates; storm::dd::Bdd transitionMatrixBdd = transitionMatrix.notZero(); if (minimize) { - infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getManager().getBddZero(), targetStates)); + infinityStates = storm::utility::graph::performProb1A(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0A(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } else { - infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getManager().getBddZero(), targetStates)); + infinityStates = storm::utility::graph::performProb1E(model, transitionMatrixBdd, model.getReachableStates(), targetStates, storm::utility::graph::performProbGreater0E(model, transitionMatrixBdd, model.getReachableStates(), targetStates)); } infinityStates = !infinityStates && model.getReachableStates(); storm::dd::Bdd maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); @@ -293,21 +296,22 @@ namespace storm { subvector += (submatrix * transitionRewardMatrix.get()).sumAbstract(model.getColumnVariables()); } - // Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed - // for solving the equation system (i.e. compute (I-A)). + // Before cutting the non-maybe columns, we need to compute the sizes of the row groups. + std::vector rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector(odd); + + // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); // Create the solution vector. std::vector x(maybeStates.getNonZeroCount(), ValueType(0.5)); // Translate the symbolic matrix/vector to their explicit representations. - storm::storage::SparseMatrix explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); - std::vector b = subvector.template toVector(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices()); + std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); // Now solve the resulting equation system. - std::unique_ptr> solver = linearEquationSolverFactory.create(explicitSubmatrix); - solver->solveEquationSystem(minimize, x, b); - + std::unique_ptr> solver = linearEquationSolverFactory.create(explicitRepresentation.first); + solver->solveEquationSystem(minimize, x, explicitRepresentation.second); + // Return a hybrid check result that stores the numerical values explicitly. return std::unique_ptr(new storm::modelchecker::HybridQuantitativeCheckResult(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity()), maybeStates, odd, x)); } else { diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 0d46f40c9..ca2c19212 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -297,6 +297,7 @@ namespace storm { std::unique_ptr> solver = MinMaxLinearEquationSolverFactory.create(submatrix); solver->solveEquationSystem(minimize, x, b); + // Set values of resulting vector according to result. storm::utility::vector::setVectorValues(result, maybeStates, x); } diff --git a/src/storage/dd/CuddAdd.cpp b/src/storage/dd/CuddAdd.cpp index 1dbf60803..6b7f2067f 100644 --- a/src/storage/dd/CuddAdd.cpp +++ b/src/storage/dd/CuddAdd.cpp @@ -424,7 +424,7 @@ namespace storm { std::vector Add::toVector(Odd const& rowOdd) const { std::vector result(rowOdd.getTotalOffset()); std::vector ddVariableIndices = this->getSortedVariableIndices(); - addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); + addToVector(rowOdd, ddVariableIndices, result); return result; } @@ -577,6 +577,7 @@ namespace storm { } } + // Create the canonical row group sizes and build the matrix. return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); } @@ -585,6 +586,7 @@ namespace storm { std::vector ddColumnVariableIndices; std::vector ddGroupVariableIndices; std::set rowAndColumnMetaVariables; + boost::optional> optionalExplicitVector; for (auto const& variable : rowMetaVariables) { DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); @@ -610,8 +612,6 @@ namespace storm { } std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); - // TODO: assert that the group variables are at the very top of the variable ordering? - // Start by computing the offsets (in terms of rows) for each row group. Add stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables); std::vector rowGroupIndices = stateToNumberOfChoices.toVector(rowOdd); @@ -635,21 +635,22 @@ namespace storm { // Now compute the indices at which the individual rows start. std::vector rowIndications(rowGroupIndices.back() + 1); + std::vector> statesWithGroupEnabled(groups.size()); + storm::dd::Add stateToRowGroupCount = this->getDdManager()->getAddZero(); for (uint_fast64_t i = 0; i < groups.size(); ++i) { auto const& dd = groups[i]; toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables).toAdd(); - addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); } // Since we modified the rowGroupIndices, we need to restore the correct values. - for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { - rowGroupIndices[i] = rowGroupIndices[i - 1]; - } - rowGroupIndices[0] = 0; + std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; + modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. tmp = 0; @@ -667,26 +668,147 @@ namespace storm { toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); - addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices); + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); } // Since we modified the rowGroupIndices, we need to restore the correct values. - for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { - rowGroupIndices[i] = rowGroupIndices[i - 1]; + modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. + for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { + rowIndications[i] = rowIndications[i - 1]; + } + rowIndications[0] = 0; + + return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + } + + std::pair, std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::set rowMetaVariables; + std::set columnMetaVariables; + + for (auto const& variable : this->getContainedMetaVariables()) { + // If the meta variable is a group meta variable, we do not insert it into the set of row/column meta variables. + if (groupMetaVariables.find(variable) != groupMetaVariables.end()) { + continue; + } + + if (variable.getName().size() > 0 && variable.getName().back() == '\'') { + columnMetaVariables.insert(variable); + } else { + rowMetaVariables.insert(variable); + } + } + + // Create the canonical row group sizes and build the matrix. + return toMatrixVector(vector, std::move(rowGroupSizes), rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd); + } + + std::pair,std::vector> Add::toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupIndices, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const { + std::vector ddRowVariableIndices; + std::vector ddColumnVariableIndices; + std::vector ddGroupVariableIndices; + std::set rowAndColumnMetaVariables; + + for (auto const& variable : rowMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddRowVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddRowVariableIndices.begin(), ddRowVariableIndices.end()); + for (auto const& variable : columnMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddColumnVariableIndices.push_back(ddVariable.getIndex()); + } + rowAndColumnMetaVariables.insert(variable); + } + std::sort(ddColumnVariableIndices.begin(), ddColumnVariableIndices.end()); + for (auto const& variable : groupMetaVariables) { + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(variable); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddGroupVariableIndices.push_back(ddVariable.getIndex()); + } + } + std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); + + // Transform the row group sizes to the actual row group indices. + rowGroupIndices.resize(rowGroupIndices.size() + 1); + uint_fast64_t tmp = 0; + uint_fast64_t tmp2 = 0; + for (uint_fast64_t i = 1; i < rowGroupIndices.size(); ++i) { + tmp2 = rowGroupIndices[i]; + rowGroupIndices[i] = rowGroupIndices[i - 1] + tmp; + std::swap(tmp, tmp2); } rowGroupIndices[0] = 0; + // Create the explicit vector we need to fill later. + std::vector explicitVector(rowGroupIndices.back()); + + // Next, we split the matrix into one for each group. This only works if the group variables are at the very + // top. + std::vector, Add>> groups; + splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables, rowMetaVariables); + + // Create the actual storage for the non-zero entries. + std::vector> columnsAndValues(this->getNonZeroCount()); + + // Now compute the indices at which the individual rows start. + std::vector rowIndications(rowGroupIndices.back() + 1); + + std::vector> statesWithGroupEnabled(groups.size()); + storm::dd::Add stateToRowGroupCount = this->getDdManager()->getAddZero(); + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + std::pair, storm::dd::Add> ddPair = groups[i]; + + toMatrixRec(ddPair.first.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false); + toVectorRec(ddPair.second.getCuddDdNode(), explicitVector, rowGroupIndices, rowOdd, 0, ddRowVariableIndices.size(), 0, ddRowVariableIndices); + + statesWithGroupEnabled[i] = (ddPair.first.notZero().existsAbstract(columnMetaVariables) || ddPair.second.notZero()).toAdd(); + stateToRowGroupCount += statesWithGroupEnabled[i]; + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + std::function fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast(b); }; + modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + + // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. + tmp = 0; + tmp2 = 0; + for (uint_fast64_t i = 1; i < rowIndications.size(); ++i) { + tmp2 = rowIndications[i]; + rowIndications[i] = rowIndications[i - 1] + tmp; + std::swap(tmp, tmp2); + } + rowIndications[0] = 0; + + // Now actually fill the entry vector. + for (uint_fast64_t i = 0; i < groups.size(); ++i) { + auto const& dd = groups[i].first; + + toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true); + + statesWithGroupEnabled[i].addToVector(rowOdd, ddRowVariableIndices, rowGroupIndices); + } + + // Since we modified the rowGroupIndices, we need to restore the correct values. + modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct); + // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values. for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) { rowIndications[i] = rowIndications[i - 1]; } rowIndications[0] = 0; - return storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); + return std::make_pair(storm::storage::SparseMatrix(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector)); } template - void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { + void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; @@ -695,7 +817,6 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentRowLevel == maxLevel) { result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); - ++rowGroupOffsets[currentRowOffset]; } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); @@ -774,8 +895,39 @@ namespace storm { } } + void Add::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, Add>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables1, std::set const& remainingMetaVariables2) const { + // For the empty DD, we do not need to create a group. + if (dd1 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager()) && dd2 == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { + return; + } + + if (currentLevel == maxLevel) { + groups.push_back(std::make_pair(Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd1), remainingMetaVariables1), Add(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd2), remainingMetaVariables2))); + } else if (ddGroupVariableIndices[currentLevel] < dd1->index) { + if (ddGroupVariableIndices[currentLevel] < dd2->index) { + splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + splitGroupsRec(dd1, dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + } else { + splitGroupsRec(dd1, Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + splitGroupsRec(dd1, Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + } + } else if (ddGroupVariableIndices[currentLevel] < dd2->index) { + splitGroupsRec(Cudd_T(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + splitGroupsRec(Cudd_E(dd1), dd2, groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + } else { + splitGroupsRec(Cudd_T(dd1), Cudd_T(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + splitGroupsRec(Cudd_E(dd1), Cudd_E(dd2), groups, ddGroupVariableIndices, currentLevel + 1, maxLevel, remainingMetaVariables1, remainingMetaVariables2); + } + } + template - void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const { + std::function fct = [] (ValueType const& a, double const& b) -> ValueType { return a + b; }; + modifyVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, fct); + } + + template + void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const { // For the empty DD, we do not need to add any entries. if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { return; @@ -783,16 +935,16 @@ namespace storm { // If we are at the maximal level, the value to be set is stored as a constant in the DD. if (currentLevel == maxLevel) { - targetVector[currentOffset] += static_cast(Cudd_V(dd)); + targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd)); } else if (ddVariableIndices[currentLevel] < dd->index) { // If we skipped a level, we need to enumerate the explicit entries for the case in which the bit is set // and for the one in which it is not set. - addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); - addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); + modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } else { // Otherwise, we simply recursively call the function for both (different) cases. - addToVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); - addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); + modifyVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function); + modifyVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function); } } @@ -910,11 +1062,14 @@ namespace storm { // Explicitly instantiate some templated functions. template std::vector Add::toVector() const; template std::vector Add::toVector(Odd const& rowOdd) const; - template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; template std::vector Add::toVector(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, std::vector groupOffsets) const; - template void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; + template void Add::toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; template std::vector Add::toVector() const; template std::vector Add::toVector(Odd const& rowOdd) const; - template void Add::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template void Add::addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + template void Add::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; + } } \ No newline at end of file diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index 6b91e514b..01a57b629 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_DD_CUDDADD_H_ #define STORM_STORAGE_DD_CUDDADD_H_ +#include + #include "src/storage/dd/Add.h" #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdForwardIterator.h" @@ -581,20 +583,21 @@ namespace storm { * @return The matrix that is represented by this ADD. */ storm::storage::SparseMatrix toMatrix(std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; - + /*! - * Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to - * determine the correct row and column, respectively, for each entry. Note: this function assumes that - * the meta variables used to distinguish different row groups are at the very top of the ADD. + * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector. + * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each + * entry. Note: this function assumes that the meta variables used to distinguish different row groups are + * at the very top of the ADD. * - * @param rowMetaVariables The meta variables that encode the rows of the matrix. - * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param vector The symbolic vector to convert. + * @param rowGroupSizes A vector specifying the sizes of the row groups. * @param groupMetaVariables The meta variables that are used to distinguish different row groups. * @param rowOdd The ODD used for determining the correct row. * @param columnOdd The ODD used for determining the correct column. * @return The matrix that is represented by this ADD. */ - storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + std::pair, std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; /*! * Exports the DD to the given file in the dot format. @@ -656,6 +659,40 @@ namespace storm { */ Add(std::shared_ptr const> ddManager, ADD cuddAdd, std::set const& containedMetaVariables = std::set()); + /*! + * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also + * translated to an explicit row-grouped vector with the same row-grouping. The given offset-labeled DDs + * are used to determine the correct row and column, respectively, for each entry. Note: this function + * assumes that the meta variables used to distinguish different row groups are at the very top of the ADD. + * + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector + * (if it was given). + */ + storm::storage::SparseMatrix toMatrix(std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + + /*! + * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to an equally row-grouped + * explicit vector. The given offset-labeled DDs are used to determine the correct row and column, + * respectively, for each entry. Note: this function assumes that the meta variables used to distinguish + * different row groups are at the very top of the ADD. + * + * @param vector The vector that is to be transformed to an equally grouped explicit vector. + * @param rowGroupSizes A vector specifying the sizes of the row groups. + * @param rowMetaVariables The meta variables that encode the rows of the matrix. + * @param columnMetaVariables The meta variables that encode the columns of the matrix. + * @param groupMetaVariables The meta variables that are used to distinguish different row groups. + * @param rowOdd The ODD used for determining the correct row. + * @param columnOdd The ODD used for determining the correct column. + * @return The matrix that is represented by this ADD and and a vector corresponding to the symbolic vector + * (if it was given). + */ + std::pair,std::vector> toMatrixVector(storm::dd::Add const& vector, std::vector&& rowGroupSizes, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::set const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd) const; + /*! * Helper function to convert the DD into a (sparse) matrix. * @@ -688,9 +725,7 @@ namespace storm { * * @param dd The DD to convert. * @param result The vector that will hold the values upon successful completion. - * @param rowGroupOffsets The row offsets at which a given row group starts. Note this vector is modified in - * the computation. More concretely, each entry i in the vector will be increased by one iff there was a - * non-zero entry in that row-group. + * @param rowGroupOffsets The row offsets at which a given row group starts. * @param rowOdd The ODD used for the row translation. * @param currentRowLevel The currently considered row level in the DD. * @param maxLevel The number of levels that need to be considered. @@ -698,7 +733,7 @@ namespace storm { * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered. */ template - void toVectorRec(DdNode const* dd, std::vector& result, std::vector& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; + void toVectorRec(DdNode const* dd, std::vector& result, std::vector const& rowGroupOffsets, Odd const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; /*! * Splits the given matrix DD into the groups using the given group variables. @@ -713,7 +748,32 @@ namespace storm { void splitGroupsRec(DdNode* dd, std::vector>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables) const; /*! - * Performs a recursive step to add the given DD-based vector to the given explicit vector. + * Splits the given matrix and vector DDs into the groups using the given group variables. + * + * @param dd1 The matrix DD to split. + * @param dd2 The vector DD to split. + * @param groups A vector that is to be filled with the pairs of matrix/vector DDs for the individual groups. + * @param ddGroupVariableIndices The (sorted) indices of all DD group variables that need to be considered. + * @param currentLevel The currently considered level in the DD. + * @param maxLevel The number of levels that need to be considered. + * @param remainingMetaVariables1 The meta variables that remain in the matrix DD after the groups have been split. + * @param remainingMetaVariables2 The meta variables that remain in the vector DD after the groups have been split. + */ + void splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector, Add>>& groups, std::vector const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set const& remainingMetaVariables1, std::set const& remainingMetaVariables2) const; + + /*! + * Adds the current (DD-based) vector to the given explicit one. + * + * @param odd The ODD used for the translation. + * @param ddVariableIndices The (sorted) indices of all DD variables that need to be considered. + * @param targetVector The vector to which the translated DD-based vector is to be added. + */ + template + void addToVector(Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + + /*! + * Performs a recursive step to perform the given function between the given DD-based vector to the given + * explicit vector. * * @param dd The DD to add to the explicit vector. * @param currentLevel The currently considered level in the DD. @@ -724,7 +784,7 @@ namespace storm { * @param targetVector The vector to which the translated DD-based vector is to be added. */ template - void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector) const; + void modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd const& odd, std::vector const& ddVariableIndices, std::vector& targetVector, std::function const& function) const; /*! * Builds an ADD representing the given vector. diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..3a7cd5402 --- /dev/null +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,190 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/logic/Formulas.h" +#include "src/utility/solver.h" +#include "src/modelchecker/prctl/HybridMdpPrctlModelChecker.h" +#include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/parser/PrismParser.h" +#include "src/builder/DdPrismModelBuilder.h" +#include "src/models/symbolic/Dtmc.h" +#include "src/settings/SettingsManager.h" + +TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "coinflips"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(169, model->getNumberOfStates()); + EXPECT_EQ(436, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("two"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("three"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("four"); + eventuallyFormula = std::make_shared(labelFormula); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("done"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} + +TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm"); + + // Build the die model with its reward model. + typename storm::builder::DdPrismModelBuilder::Options options; + options.buildRewards = true; + options.rewardModelName = "rounds"; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(3172, model->getNumberOfStates()); + EXPECT_EQ(7144, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); + + std::shared_ptr> mdp = model->as>(); + + storm::modelchecker::HybridMdpPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("elected"); + auto eventuallyFormula = std::make_shared(labelFormula); + auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); + + std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto trueFormula = std::make_shared(true); + auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 25); + minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); + + result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); + + result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + labelFormula = std::make_shared("elected"); + auto reachabilityRewardFormula = std::make_shared(labelFormula); + auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); + + result = checker.check(*minRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + + auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); + + result = checker.check(*maxRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); + + EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index ccc9ed7e3..1b1af244d 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -97,8 +97,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult7 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); - EXPECT_NEAR(7.333329499, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); @@ -106,8 +106,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult8 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(7.333329499, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); - EXPECT_NEAR(7.333329499, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { @@ -118,8 +118,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { options.buildRewards = true; options.rewardModelName = "rounds"; std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); - EXPECT_EQ(169, model->getNumberOfStates()); - EXPECT_EQ(436, model->getNumberOfTransitions()); + EXPECT_EQ(3172, model->getNumberOfStates()); + EXPECT_EQ(7144, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); @@ -132,7 +132,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { auto minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, eventuallyFormula); std::unique_ptr result = checker.check(*minProbabilityOperatorFormula); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -140,7 +141,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { auto maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, eventuallyFormula); result = checker.check(*maxProbabilityOperatorFormula); - storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -151,6 +153,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { minProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, boundedUntilFormula); result = checker.check(*minProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -159,6 +162,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { maxProbabilityOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, boundedUntilFormula); result = checker.check(*maxProbabilityOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -169,16 +173,18 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { auto minRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); result = checker.check(*minRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult5 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); - EXPECT_NEAR(4.285689611, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); auto maxRewardOperatorFormula = std::make_shared(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); result = checker.check(*maxRewardOperatorFormula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult6 = result->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(4.285689611, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); - EXPECT_NEAR(4.285689611, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); } diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 6255e912c..f8b149c2d 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -351,7 +351,7 @@ TEST(CuddDd, AddOddTest) { EXPECT_EQ(25, matrix.getNonzeroEntryCount()); dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); - ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd)); + ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); EXPECT_EQ(18, matrix.getRowCount()); EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getColumnCount()); @@ -398,7 +398,7 @@ TEST(CuddDd, BddOddTest) { EXPECT_EQ(25, matrix.getNonzeroEntryCount()); dd = manager->getRange(x.first).toAdd() * manager->getRange(x.second).toAdd() * manager->getEncoding(a.first, 0).toAdd().ite(dd, dd + manager->getConstant(1)); - ASSERT_NO_THROW(matrix = dd.toMatrix({x.first}, {x.second}, {a.first}, rowOdd, columnOdd)); + ASSERT_NO_THROW(matrix = dd.toMatrix({a.first}, rowOdd, columnOdd)); EXPECT_EQ(18, matrix.getRowCount()); EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getColumnCount());