Browse Source

Finalized hybrid MDP model checker. It passes its tests now.

Former-commit-id: 47de0b9433
main
dehnert 10 years ago
parent
commit
dd399c5f85
  1. 44
      src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
  2. 1
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  3. 201
      src/storage/dd/CuddAdd.cpp
  4. 86
      src/storage/dd/CuddAdd.h
  5. 190
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  6. 30
      test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  7. 4
      test/functional/storage/CuddDdTest.cpp

44
src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp

@ -70,19 +70,20 @@ namespace storm {
storm::dd::Add<DdType> subvector = submatrix * prob1StatesAsColumn; storm::dd::Add<DdType> subvector = submatrix * prob1StatesAsColumn;
subvector = subvector.sumAbstract(model.getColumnVariables()); subvector = subvector.sumAbstract(model.getColumnVariables());
// Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed // Before cutting the non-maybe columns, we need to compute the sizes of the row groups.
// for solving the equation system (i.e. compute (I-A)). std::vector<uint_fast64_t> rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector<uint_fast64_t>(odd);
// Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Create the solution vector. // Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5)); std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system. // Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
std::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitRepresentation.first);
solver->solveEquationSystem(minimize, x, b); solver->solveEquationSystem(minimize, x, explicitRepresentation.second);
// Return a hybrid check result that stores the numerical values explicitly. // Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, statesWithProbability01.second.toAdd(), maybeStates, odd, x)); return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(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); statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0E(model, transitionMatrix.notZero(), phiStates, psiStates);
} }
storm::dd::Bdd<DdType> maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates(); storm::dd::Bdd<DdType> maybeStates = statesWithProbabilityGreater0 && !psiStates && model.getReachableStates();
// If there are maybe states, we need to perform matrix-vector multiplications. // If there are maybe states, we need to perform matrix-vector multiplications.
if (!maybeStates.isZero()) { if (!maybeStates.isZero()) {
// Create the ODD for the translation between symbolic and explicit storage. // Create the ODD for the translation between symbolic and explicit storage.
@ -156,6 +157,9 @@ namespace storm {
storm::dd::Add<DdType> prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); storm::dd::Add<DdType> prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs());
storm::dd::Add<DdType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); storm::dd::Add<DdType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables());
// Before cutting the non-maybe columns, we need to compute the sizes of the row groups.
std::vector<uint_fast64_t> rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector<uint_fast64_t>(odd);
// Finally cut away all columns targeting non-maybe states. // Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
@ -163,11 +167,10 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>()); std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations. // Translate the symbolic matrix/vector to their explicit representations.
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
std::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitRepresentation.first);
solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); solver->performMatrixVectorMultiplication(minimize, x, &explicitRepresentation.second, stepBound);
// Return a hybrid check result that stores the numerical values explicitly. // Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.toAdd(), maybeStates, odd, x)); return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, psiStates.toAdd(), maybeStates, odd, x));
@ -259,9 +262,9 @@ namespace storm {
storm::dd::Bdd<DdType> infinityStates; storm::dd::Bdd<DdType> infinityStates;
storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero(); storm::dd::Bdd<DdType> transitionMatrixBdd = transitionMatrix.notZero();
if (minimize) { 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 { } 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(); infinityStates = !infinityStates && model.getReachableStates();
storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates();
@ -293,21 +296,22 @@ namespace storm {
subvector += (submatrix * transitionRewardMatrix.get()).sumAbstract(model.getColumnVariables()); subvector += (submatrix * transitionRewardMatrix.get()).sumAbstract(model.getColumnVariables());
} }
// Finally cut away all columns targeting non-maybe states and convert the matrix into the matrix needed // Before cutting the non-maybe columns, we need to compute the sizes of the row groups.
// for solving the equation system (i.e. compute (I-A)). std::vector<uint_fast64_t> rowGroupSizes = submatrix.notZero().existsAbstract(model.getColumnVariables()).toAdd().sumAbstract(model.getNondeterminismVariables()).template toVector<uint_fast64_t>(odd);
// Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Create the solution vector. // Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5)); std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
// Translate the symbolic matrix/vector to their explicit representations. // Translate the symbolic matrix/vector to their explicit representations.
storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
std::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
// Now solve the resulting equation system. // Now solve the resulting equation system.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitRepresentation.first);
solver->solveEquationSystem(minimize, x, b); solver->solveEquationSystem(minimize, x, explicitRepresentation.second);
// Return a hybrid check result that stores the numerical values explicitly. // Return a hybrid check result that stores the numerical values explicitly.
return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()), maybeStates, odd, x)); return std::unique_ptr<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()), maybeStates, odd, x));
} else { } else {

1
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@ -297,6 +297,7 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory.create(submatrix); std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory.create(submatrix);
solver->solveEquationSystem(minimize, x, b); solver->solveEquationSystem(minimize, x, b);
// Set values of resulting vector according to result. // Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x); storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
} }

201
src/storage/dd/CuddAdd.cpp

@ -424,7 +424,7 @@ namespace storm {
std::vector<ValueType> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const { std::vector<ValueType> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
std::vector<ValueType> result(rowOdd.getTotalOffset()); std::vector<ValueType> result(rowOdd.getTotalOffset());
std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices(); std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result); addToVector(rowOdd, ddVariableIndices, result);
return 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); return toMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd);
} }
@ -585,6 +586,7 @@ namespace storm {
std::vector<uint_fast64_t> ddColumnVariableIndices; std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices; std::vector<uint_fast64_t> ddGroupVariableIndices;
std::set<storm::expressions::Variable> rowAndColumnMetaVariables; std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
boost::optional<std::vector<double>> optionalExplicitVector;
for (auto const& variable : rowMetaVariables) { for (auto const& variable : rowMetaVariables) {
DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variable); DdMetaVariable<DdType::CUDD> const& metaVariable = this->getDdManager()->getMetaVariable(variable);
@ -610,8 +612,6 @@ namespace storm {
} }
std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end()); 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. // Start by computing the offsets (in terms of rows) for each row group.
Add<DdType::CUDD> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables); Add<DdType::CUDD> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables);
std::vector<uint_fast64_t> rowGroupIndices = stateToNumberOfChoices.toVector<uint_fast64_t>(rowOdd); std::vector<uint_fast64_t> rowGroupIndices = stateToNumberOfChoices.toVector<uint_fast64_t>(rowOdd);
@ -635,21 +635,22 @@ namespace storm {
// Now compute the indices at which the individual rows start. // Now compute the indices at which the individual rows start.
std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1); std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
std::vector<storm::dd::Add<DdType::CUDD>> statesWithGroupEnabled(groups.size()); std::vector<storm::dd::Add<DdType::CUDD>> statesWithGroupEnabled(groups.size());
storm::dd::Add<storm::dd::DdType::CUDD> stateToRowGroupCount = this->getDdManager()->getAddZero();
for (uint_fast64_t i = 0; i < groups.size(); ++i) { for (uint_fast64_t i = 0; i < groups.size(); ++i) {
auto const& dd = groups[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); 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(); 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. // Since we modified the rowGroupIndices, we need to restore the correct values.
for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { std::function<uint_fast64_t (uint_fast64_t const&, double const&)> fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast<uint_fast64_t>(b); };
rowGroupIndices[i] = rowGroupIndices[i - 1]; modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct);
}
rowGroupIndices[0] = 0;
// Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector. // Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
tmp = 0; 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); 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. // Since we modified the rowGroupIndices, we need to restore the correct values.
for (uint_fast64_t i = rowGroupIndices.size() - 1; i > 0; --i) { modifyVectorRec(stateToRowGroupCount.getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices, fct);
rowGroupIndices[i] = rowGroupIndices[i - 1]; // 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<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
}
std::pair<storm::storage::SparseMatrix<double>, std::vector<double>> Add<DdType::CUDD>::toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
std::set<storm::expressions::Variable> rowMetaVariables;
std::set<storm::expressions::Variable> 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<storm::storage::SparseMatrix<double>,std::vector<double>> Add<DdType::CUDD>::toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupIndices, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
std::vector<uint_fast64_t> ddRowVariableIndices;
std::vector<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
for (auto const& variable : rowMetaVariables) {
DdMetaVariable<DdType::CUDD> 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<DdType::CUDD> 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<DdType::CUDD> 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; rowGroupIndices[0] = 0;
// Create the explicit vector we need to fill later.
std::vector<double> 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<std::pair<Add<DdType::CUDD>, Add<DdType::CUDD>>> groups;
splitGroupsRec(this->getCuddDdNode(), vector.getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables, rowMetaVariables);
// Create the actual storage for the non-zero entries.
std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
// Now compute the indices at which the individual rows start.
std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
std::vector<storm::dd::Add<DdType::CUDD>> statesWithGroupEnabled(groups.size());
storm::dd::Add<storm::dd::DdType::CUDD> stateToRowGroupCount = this->getDdManager()->getAddZero();
for (uint_fast64_t i = 0; i < groups.size(); ++i) {
std::pair<storm::dd::Add<DdType::CUDD>, storm::dd::Add<DdType::CUDD>> 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<uint_fast64_t (uint_fast64_t const&, double const&)> fct = [] (uint_fast64_t const& a, double const& b) -> uint_fast64_t { return a - static_cast<uint_fast64_t>(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. // 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) { for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
rowIndications[i] = rowIndications[i - 1]; rowIndications[i] = rowIndications[i - 1];
} }
rowIndications[0] = 0; rowIndications[0] = 0;
return storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)); return std::make_pair(storm::storage::SparseMatrix<double>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), std::move(explicitVector));
} }
template<typename ValueType> template<typename ValueType>
void Add<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t>& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const { void Add<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
// For the empty DD, we do not need to add any entries. // For the empty DD, we do not need to add any entries.
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
return; 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 we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentRowLevel == maxLevel) { if (currentRowLevel == maxLevel) {
result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd); result[rowGroupOffsets[currentRowOffset]] = Cudd_V(dd);
++rowGroupOffsets[currentRowOffset];
} else if (ddRowVariableIndices[currentRowLevel] < dd->index) { } else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); toVectorRec(dd, result, rowGroupOffsets, rowOdd.getElseSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); toVectorRec(dd, result, rowGroupOffsets, rowOdd.getThenSuccessor(), currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
@ -774,8 +895,39 @@ namespace storm {
} }
} }
void Add<DdType::CUDD>::splitGroupsRec(DdNode* dd1, DdNode* dd2, std::vector<std::pair<Add<DdType::CUDD>, Add<DdType::CUDD>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables1, std::set<storm::expressions::Variable> 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<DdType::CUDD>(this->getDdManager(), ADD(this->getDdManager()->getCuddManager(), dd1), remainingMetaVariables1), Add<DdType::CUDD>(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<typename ValueType> template<typename ValueType>
void Add<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const { void Add<DdType::CUDD>::addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
std::function<ValueType (ValueType const&, double const&)> fct = [] (ValueType const& a, double const& b) -> ValueType { return a + b; };
modifyVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, odd, ddVariableIndices, targetVector, fct);
}
template<typename ValueType>
void Add<DdType::CUDD>::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, double const&)> const& function) const {
// For the empty DD, we do not need to add any entries. // For the empty DD, we do not need to add any entries.
if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) { if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
return; 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 we are at the maximal level, the value to be set is stored as a constant in the DD.
if (currentLevel == maxLevel) { if (currentLevel == maxLevel) {
targetVector[currentOffset] += static_cast<ValueType>(Cudd_V(dd)); targetVector[currentOffset] = function(targetVector[currentOffset], Cudd_V(dd));
} else if (ddVariableIndices[currentLevel] < dd->index) { } 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 // 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. // and for the one in which it is not set.
addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
addToVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); modifyVectorRec(dd, currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector, function);
} else { } else {
// Otherwise, we simply recursively call the function for both (different) cases. // Otherwise, we simply recursively call the function for both (different) cases.
addToVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector); modifyVectorRec(Cudd_E(dd), currentLevel + 1, maxLevel, currentOffset, odd.getElseSuccessor(), ddVariableIndices, targetVector, function);
addToVectorRec(Cudd_T(dd), currentLevel + 1, maxLevel, currentOffset + odd.getElseOffset(), odd.getThenSuccessor(), ddVariableIndices, targetVector); 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. // Explicitly instantiate some templated functions.
template std::vector<double> Add<DdType::CUDD>::toVector() const; template std::vector<double> Add<DdType::CUDD>::toVector() const;
template std::vector<double> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const; template std::vector<double> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
template void Add<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double>& targetVector) const; template void Add<DdType::CUDD>::addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double>& targetVector) const;
template void Add<DdType::CUDD>::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<double>& targetVector, std::function<double (double const&, double const&)> const& function) const;
template std::vector<double> Add<DdType::CUDD>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> groupOffsets) const; template std::vector<double> Add<DdType::CUDD>::toVector(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, std::vector<uint_fast64_t> groupOffsets) const;
template void Add<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<double>& result, std::vector<uint_fast64_t>& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const; template void Add<DdType::CUDD>::toVectorRec(DdNode const* dd, std::vector<double>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
template std::vector<uint_fast64_t> Add<DdType::CUDD>::toVector() const; template std::vector<uint_fast64_t> Add<DdType::CUDD>::toVector() const;
template std::vector<uint_fast64_t> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const; template std::vector<uint_fast64_t> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const;
template void Add<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t>& targetVector) const; template void Add<DdType::CUDD>::addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t>& targetVector) const;
template void Add<DdType::CUDD>::modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<uint_fast64_t>& targetVector, std::function<uint_fast64_t (uint_fast64_t const&, double const&)> const& function) const;
} }
} }

86
src/storage/dd/CuddAdd.h

@ -1,6 +1,8 @@
#ifndef STORM_STORAGE_DD_CUDDADD_H_ #ifndef STORM_STORAGE_DD_CUDDADD_H_
#define STORM_STORAGE_DD_CUDDADD_H_ #define STORM_STORAGE_DD_CUDDADD_H_
#include <boost/optional.hpp>
#include "src/storage/dd/Add.h" #include "src/storage/dd/Add.h"
#include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDd.h"
#include "src/storage/dd/CuddDdForwardIterator.h" #include "src/storage/dd/CuddDdForwardIterator.h"
@ -581,20 +583,21 @@ namespace storm {
* @return The matrix that is represented by this ADD. * @return The matrix that is represented by this ADD.
*/ */
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const;
/*! /*!
* Converts the ADD to a row-grouped (sparse) double matrix. The given offset-labeled DDs are used to * Converts the ADD to a row-grouped (sparse) double matrix and the given vector to a row-grouped vector.
* determine the correct row and column, respectively, for each entry. Note: this function assumes that * The given offset-labeled DDs are used to determine the correct row and column, respectively, for each
* the meta variables used to distinguish different row groups are at the very top of the ADD. * 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 vector The symbolic vector to convert.
* @param columnMetaVariables The meta variables that encode the columns of the matrix. * @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 groupMetaVariables The meta variables that are used to distinguish different row groups.
* @param rowOdd The ODD used for determining the correct row. * @param rowOdd The ODD used for determining the correct row.
* @param columnOdd The ODD used for determining the correct column. * @param columnOdd The ODD used for determining the correct column.
* @return The matrix that is represented by this ADD. * @return The matrix that is represented by this ADD.
*/ */
storm::storage::SparseMatrix<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const; std::pair<storm::storage::SparseMatrix<double>, std::vector<double>> toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const;
/*! /*!
* Exports the DD to the given file in the dot format. * Exports the DD to the given file in the dot format.
@ -656,6 +659,40 @@ namespace storm {
*/ */
Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>()); Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
/*!
* 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<double> toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> 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<storm::storage::SparseMatrix<double>,std::vector<double>> toMatrixVector(storm::dd::Add<storm::dd::DdType::CUDD> const& vector, std::vector<uint_fast64_t>&& rowGroupSizes, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const;
/*! /*!
* Helper function to convert the DD into a (sparse) matrix. * Helper function to convert the DD into a (sparse) matrix.
* *
@ -688,9 +725,7 @@ namespace storm {
* *
* @param dd The DD to convert. * @param dd The DD to convert.
* @param result The vector that will hold the values upon successful completion. * @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 * @param rowGroupOffsets The row offsets at which a given row group starts.
* 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 rowOdd The ODD used for the row translation. * @param rowOdd The ODD used for the row translation.
* @param currentRowLevel The currently considered row level in the DD. * @param currentRowLevel The currently considered row level in the DD.
* @param maxLevel The number of levels that need to be considered. * @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. * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
*/ */
template<typename ValueType> template<typename ValueType>
void toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t>& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const; void toVectorRec(DdNode const* dd, std::vector<ValueType>& result, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
/*! /*!
* Splits the given matrix DD into the groups using the given group variables. * 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<Add<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const; void splitGroupsRec(DdNode* dd, std::vector<Add<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> 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<std::pair<Add<DdType::CUDD>, Add<DdType::CUDD>>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables1, std::set<storm::expressions::Variable> 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<typename ValueType>
void addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& 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 dd The DD to add to the explicit vector.
* @param currentLevel The currently considered level in the DD. * @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. * @param targetVector The vector to which the translated DD-based vector is to be added.
*/ */
template<typename ValueType> template<typename ValueType>
void addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const; void modifyVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector, std::function<ValueType (ValueType const&, double const&)> const& function) const;
/*! /*!
* Builds an ADD representing the given vector. * Builds an ADD representing the given vector.

190
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<storm::dd::DdType::CUDD>::Options options;
options.buildRewards = true;
options.rewardModelName = "coinflips";
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169, model->getNumberOfStates());
EXPECT_EQ(436, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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<storm::dd::DdType::CUDD>::Options options;
options.buildRewards = true;
options.rewardModelName = "rounds";
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(3172, model->getNumberOfStates());
EXPECT_EQ(7144, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
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::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}

30
test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp

@ -97,8 +97,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(7.333329499, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.333329499, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
@ -106,8 +106,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult8 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(7.333329499, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.333329499, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(7.3333283960819244, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
} }
TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
@ -118,8 +118,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
options.buildRewards = true; options.buildRewards = true;
options.rewardModelName = "rounds"; options.rewardModelName = "rounds";
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options); std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(169, model->getNumberOfStates()); EXPECT_EQ(3172, model->getNumberOfStates());
EXPECT_EQ(436, model->getNumberOfTransitions()); EXPECT_EQ(7144, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
@ -132,7 +132,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula); auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), 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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula); auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula); result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), 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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula); minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula); result = checker.check(*minProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
@ -159,6 +162,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula); maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula); result = checker.check(*maxProbabilityOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult4 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
@ -169,16 +173,18 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula); auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula); result = checker.check(*minRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(4.285689611, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.285689611, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856925589077264, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula); auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula); result = checker.check(*maxRewardOperatorFormula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult6 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(4.285689611, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.285689611, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(4.2856953906798676, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
} }

4
test/functional/storage/CuddDdTest.cpp

@ -351,7 +351,7 @@ TEST(CuddDd, AddOddTest) {
EXPECT_EQ(25, matrix.getNonzeroEntryCount()); 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)); 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(18, matrix.getRowCount());
EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getRowGroupCount());
EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(9, matrix.getColumnCount());
@ -398,7 +398,7 @@ TEST(CuddDd, BddOddTest) {
EXPECT_EQ(25, matrix.getNonzeroEntryCount()); 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)); 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(18, matrix.getRowCount());
EXPECT_EQ(9, matrix.getRowGroupCount()); EXPECT_EQ(9, matrix.getRowGroupCount());
EXPECT_EQ(9, matrix.getColumnCount()); EXPECT_EQ(9, matrix.getColumnCount());

|||||||
100:0
Loading…
Cancel
Save