sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

bugfix for symbolic reachability reward computation 

Former-commit-id: c197203539
tempestpy_adaptions
dehnert 9 years ago
parent
fd3b8adc00
commit
f3701f66fb
5 changed files with 40 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  2. 17
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  3. 5
      src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  4. 13
      src/storage/dd/DdManager.cpp
  5. 8
      src/storage/dd/DdManager.h

7
src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -242,6 +242,11 @@ namespace storm {
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
// 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<DdType> choicesWithInfinitySuccessor = (maybeStates && transitionMatrixBdd && infinityStates.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables());
subvector = choicesWithInfinitySuccessor.ite(model.getManager().template getInfinity<ValueType>(), subvector);
// Before cutting the non-maybe columns, we need to compute the sizes of the row groups.
storm::dd::Add<DdType, uint_fast64_t> stateActionAdd = (submatrix.notZero().existsAbstract(model.getColumnVariables()) || subvector.notZero()).template toAdd<uint_fast64_t>();
std::vector<uint_fast64_t> rowGroupSizes = stateActionAdd.sumAbstract(model.getNondeterminismVariables()).toVector(odd);
@ -254,7 +259,7 @@ namespace storm {
// Translate the symbolic matrix/vector to their explicit representations.
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(explicitRepresentation.first);
solver->solveEquationSystem(dir, x, explicitRepresentation.second);

17
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -275,15 +275,15 @@ namespace storm {
template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeReachabilityRewardsHelper(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::function<std::vector<ValueType>(uint_fast64_t, storm::storage::SparseMatrix<ValueType> const&, storm::storage::BitVector const&)> const& totalStateRewardVectorGetter, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
std::vector<uint_fast64_t> nondeterminsticChoiceIndices = transitionMatrix.getRowGroupIndices();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
// Determine which states have a reward of infinity by definition.
storm::storage::BitVector infinityStates;
storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true);
if (dir == OptimizationDirection::Minimize) {
infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
infinityStates = storm::utility::graph::performProb1E(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
} else {
infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterminsticChoiceIndices, backwardTransitions, trueStates, targetStates);
infinityStates = storm::utility::graph::performProb1A(transitionMatrix, nondeterministicChoiceIndices, backwardTransitions, trueStates, targetStates);
}
infinityStates.complement();
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
@ -310,13 +310,12 @@ namespace storm {
// Prepare the right-hand side of the equation system.
std::vector<ValueType> b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates);
// This also means that -- when minimizing -- we have to set the entries to infinity that have
// any successor that is an "infinity state". This prevents the action from "being taken" and
// forces the choice that leads to a reward less than infinity.
// 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.
uint_fast64_t currentRow = 0;
for (auto state : maybeStates) {
for (uint_fast64_t row = nondeterminsticChoiceIndices[state]; row < nondeterminsticChoiceIndices[state + 1]; ++row, ++currentRow) {
for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row, ++currentRow) {
for (auto const& element : transitionMatrix.getRow(row)) {
if (infinityStates.get(element.getColumn())) {
b[currentRow] = storm::utility::infinity<ValueType>();
@ -327,7 +326,7 @@ namespace storm {
}
// Create vector for results for maybe states.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
// Solve the corresponding system of equations.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(submatrix);

5
src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -192,6 +192,11 @@ namespace storm {
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> subvector = rewardModel.getTotalRewardVector(maybeStatesAdd, submatrix, model.getColumnVariables());
// 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<DdType> choicesWithInfinitySuccessor = (maybeStates && transitionMatrixBdd && infinityStates.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables());
subvector = choicesWithInfinitySuccessor.ite(model.getManager().template getInfinity<ValueType>(), subvector);
// Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());

13
src/storage/dd/DdManager.cpp
View File

@ -3,6 +3,7 @@
#include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
#include "src/utility/constants.h"
#include "src/exceptions/InvalidArgumentException.h"
namespace storm {
@ -34,6 +35,12 @@ namespace storm {
return Add<LibraryType, ValueType>(*this, internalDdManager.template getAddZero<ValueType>());
}
template<DdType LibraryType>
template<typename ValueType>
Add<LibraryType, ValueType> DdManager<LibraryType>::getInfinity() const {
return getConstant(storm::utility::infinity<ValueType>());
}
template<DdType LibraryType>
template<typename ValueType>
Add<LibraryType, ValueType> DdManager<LibraryType>::getConstant(ValueType const& value) const {
@ -315,6 +322,9 @@ namespace storm {
template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getAddOne() const;
template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getAddOne() const;
template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getInfinity<double>() const;
template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getInfinity<uint_fast64_t>() const;
template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getConstant(double const& value) const;
template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
@ -330,6 +340,9 @@ namespace storm {
template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getAddOne() const;
template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getAddOne() const;
template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getInfinity<double>() const;
template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getInfinity<uint_fast64_t>() const;
template Add<DdType::Sylvan, double> DdManager<DdType::Sylvan>::getConstant(double const& value) const;
template Add<DdType::Sylvan, uint_fast64_t> DdManager<DdType::Sylvan>::getConstant(uint_fast64_t const& value) const;

8
src/storage/dd/DdManager.h
View File

@ -69,6 +69,14 @@ namespace storm {
*/
template<typename ValueType>
Add<LibraryType, ValueType> getAddZero() const;
/*!
* Retrieves an ADD representing the constant infinity function.
*
* @return An ADD representing the constant infinity function.
*/
template<typename ValueType>
Add<LibraryType, ValueType> getInfinity() const;
/*!
* Retrieves an ADD representing the constant function with the given value.

Write Preview
Loading…
Cancel
Save