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<DdType> 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<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());
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
// 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::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
+ std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
- std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix);
- solver->solveEquationSystem(minimize, x, b);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<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);
}
storm::dd::Bdd<DdType> 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<DdType> prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs());
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.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
@@ -163,11 +167,10 @@ namespace storm {
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations.
- storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd);
- std::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
+ std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
- std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix);
- solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound);
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<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> 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<DdType> 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<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());
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5));
// Translate the symbolic matrix/vector to their explicit representations.
- storm::storage::SparseMatrix<ValueType> explicitSubmatrix = submatrix.toMatrix(model.getNondeterminismVariables(), odd, odd);
- std::vector<ValueType> b = subvector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitSubmatrix.getRowGroupIndices());
+ std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
// Now solve the resulting equation system.
- std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitSubmatrix);
- solver->solveEquationSystem(minimize, x, b);
-
+ std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> 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<CheckResult>(new storm::modelchecker::HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getReachableStates() && !maybeStates, infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()), 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<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = MinMaxLinearEquationSolverFactory.create(submatrix);
solver->solveEquationSystem(minimize, x, b);
+
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(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<ValueType> Add<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
std::vector<ValueType> result(rowOdd.getTotalOffset());
std::vector<uint_fast64_t> 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<uint_fast64_t> ddColumnVariableIndices;
std::vector<uint_fast64_t> ddGroupVariableIndices;
std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
+ boost::optional<std::vector<double>> optionalExplicitVector;
for (auto const& variable : rowMetaVariables) {
DdMetaVariable<DdType::CUDD> 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<DdType::CUDD> stateToNumberOfChoices = this->notZero().existsAbstract(columnMetaVariables).toAdd().sumAbstract(groupMetaVariables);
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.
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) {
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<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;
@@ -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<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;
+ // 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.
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));
+ 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>
- 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.
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<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>
- 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.
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<ValueType>(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<double> Add<DdType::CUDD>::toVector() 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 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(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;
+
}
}
\ 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 <boost/optional.hpp>
+
#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<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
- * 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<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.
@@ -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>());
+ /*!
+ * 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.
*
@@ -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<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.
@@ -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;
/*!
- * 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 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<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.
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<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());
+}
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<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.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::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()));
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.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<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());
+ 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::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
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.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);
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.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -151,6 +153,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
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());
@@ -159,6 +162,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
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());
@@ -169,16 +173,18 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
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.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::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.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());