diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index ad656a53b..1caae1606 100644 --- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -243,16 +243,21 @@ namespace storm { // Then compute the state reward vector to use in the computation. storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables()); + if (!rewardModel.hasStateActionRewards() && !rewardModel.hasTransitionRewards()) { + // If the reward model neither has state-action nor transition rewards, we need to multiply + // it with the legal nondetermism encodings in each state. + subvector *= transitionMatrixBdd.existsAbstract(model.getColumnVariables()).template toAdd(); + } // Since we are cutting away target and infinity states, we need to account for this by giving // choices the value infinity that have some successor contained in the infinity states. storm::dd::Bdd choicesWithInfinitySuccessor = (maybeStates && transitionMatrixBdd && infinityStates.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables()); subvector = choicesWithInfinitySuccessor.ite(model.getManager().template getInfinity(), subvector); - + // Before cutting the non-maybe columns, we need to compute the sizes of the row groups. - storm::dd::Add stateActionAdd = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd(); + storm::dd::Add stateActionAdd = submatrix.notZero().existsAbstract(model.getColumnVariables()).template toAdd(); std::vector rowGroupSizes = stateActionAdd.sumAbstract(model.getNondeterminismVariables()).toVector(odd); - + // Finally cut away all columns targeting non-maybe states. submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); @@ -261,7 +266,7 @@ namespace storm { // Translate the symbolic matrix/vector to their explicit representations. std::pair, std::vector> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd); - + // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first)); solver->solveEquations(dir, x, explicitRepresentation.second); diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 4db5e15a9..5d84bd9fb 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -88,7 +88,6 @@ namespace storm { storm::utility::vector::selectVectorValues(x, maybeStates, resultHint.get()); } - // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 61aa2636f..2db593ac9 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -330,7 +330,7 @@ namespace storm { } } } - + // Create vector for results for maybe states. std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::zero()); diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index c8dd1f1f3..ac1815d43 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -166,13 +166,13 @@ namespace storm { storm::dd::Add submatrix = transitionMatrix * maybeStatesAdd; // Then compute the state reward vector to use in the computation. - storm::dd::Add subvector = rewardModel.getTotalRewardVector(submatrix, model.getColumnVariables()); + storm::dd::Add subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, 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)). submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; - + // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0), subvector); diff --git a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp index 0d9e86fc5..ef52d6028 100644 --- a/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -106,6 +106,7 @@ namespace storm { if (!this->symbolicStates.isZero()) { if (this->symbolicValues.isZero()) { out << "0"; + first = false; } else { for (auto valuationValuePair : this->symbolicValues) { if (!first) { diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index 7189b1544..f8a8a3ad2 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp @@ -54,15 +54,15 @@ namespace storm { xCopy = tmp; - if (converged) { - STORM_LOG_TRACE("Iterative solver converged in " << iterations << " iterations."); - } else { - STORM_LOG_WARN("Iterative solver did not converge in " << iterations << " iterstions."); - } - ++iterations; } - + + if (converged) { + STORM_LOG_TRACE("Iterative solver converged in " << iterations << " iterations."); + } else { + STORM_LOG_WARN("Iterative solver did not converge in " << iterations << " iterstions."); + } + return xCopy; }