Browse Source
more work on reward model that turned out to be refactoring in disguise
more work on reward model that turned out to be refactoring in disguise
Former-commit-id: 31a7fa4801
main
dehnert
10 years ago
36 changed files with 1387 additions and 1173 deletions
-
8CMakeLists.txt
-
18src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
-
39src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
-
15src/modelchecker/csl/SparseCtmcCslModelChecker.h
-
0src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
-
25src/modelchecker/csl/helper/SparseCtmcCslHelper.h
-
0src/modelchecker/csl/helper/SymbolicCtmcCslHelper.cpp
-
0src/modelchecker/csl/helper/SymbolicCtmcCslHelper.h
-
6src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
-
254src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
-
14src/modelchecker/prctl/HybridMdpPrctlModelChecker.h
-
226src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
-
19src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
399src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
-
22src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
211src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp
-
19src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h
-
0src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
-
0src/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h
-
248src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
-
34src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h
-
196src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
-
39src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
-
407src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
-
45src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
-
195src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
-
35src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h
-
0src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
-
0src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h
-
3src/modelchecker/propositional/SparsePropositionalModelChecker.h
-
3src/models/sparse/Ctmc.h
-
2src/settings/ArgumentBuilder.h
-
29src/storage/MaximalEndComponentDecomposition.cpp
-
13src/storage/MaximalEndComponentDecomposition.h
-
12src/storage/StronglyConnectedComponentDecomposition.cpp
-
24src/storage/StronglyConnectedComponentDecomposition.h
@ -0,0 +1,25 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include <vector> |
|||
|
|||
#include "src/models/sparse/StandardRewardModel.h" |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class SparseCtmcCslHelper { |
|||
public: |
|||
|
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ */ |
|||
@ -0,0 +1,248 @@ |
|||
#include "src/modelchecker/prctl/helper/HybridMdpPrctlHelper.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
|
|||
// probability 0 and 1 of satisfying the until-formula.
|
|||
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01; |
|||
if (minimize) { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Min(model, phiStates, psiStates); |
|||
} else { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Max(model, phiStates, psiStates); |
|||
} |
|||
storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); |
|||
|
|||
// Perform some logging.
|
|||
STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states."); |
|||
STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
|
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5))); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
storm::dd::Add<DdType> prob1StatesAsColumn = statesWithProbability01.second.toAdd(); |
|||
prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> subvector = submatrix * prob1StatesAsColumn; |
|||
subvector = subvector.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()); |
|||
|
|||
// 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.
|
|||
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(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)); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), statesWithProbability01.second.toAdd())); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> HybridMdpPrctlModelChecker<DdType, ValueType>::computeNextProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) { |
|||
storm::dd::Add<DdType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); |
|||
return result.sumAbstract(model.getColumnVariables()); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeBoundedUntilProbabilitiesHelper(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
|
|||
// probability 0 or 1 of satisfying the until-formula.
|
|||
storm::dd::Bdd<DdType> statesWithProbabilityGreater0; |
|||
if (minimize) { |
|||
statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0A(model, transitionMatrix.notZero(), phiStates, psiStates); |
|||
} else { |
|||
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.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
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()); |
|||
|
|||
// Create the solution vector.
|
|||
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
// 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); |
|||
|
|||
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)); |
|||
} else { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), psiStates.toAdd())); |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeInstantaneousRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(model.getReachableStates()); |
|||
|
|||
// Translate the symbolic matrix to its explicit representations.
|
|||
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); |
|||
|
|||
// Create the solution vector (and initialize it to the state rewards of the model).
|
|||
std::vector<ValueType> x = model.getStateRewardVector().template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitMatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, x, nullptr, stepBound); |
|||
|
|||
// Return a hybrid check result that stores the numerical values explicitly.
|
|||
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeCumulativeRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Compute the reward vector to add in each step based on the available reward models.
|
|||
storm::dd::Add<DdType> totalRewardVector = model.hasStateRewards() ? model.getStateRewardVector() : model.getManager().getAddZero(); |
|||
if (model.hasTransitionRewards()) { |
|||
totalRewardVector += (transitionMatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables()); |
|||
} |
|||
|
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(model.getReachableStates()); |
|||
|
|||
// Create the solution vector.
|
|||
std::vector<ValueType> x(model.getNumberOfStates(), storm::utility::zero<ValueType>()); |
|||
|
|||
// Translate the symbolic matrix/vector to their explicit representations.
|
|||
storm::storage::SparseMatrix<ValueType> explicitMatrix = transitionMatrix.toMatrix(model.getNondeterminismVariables(), odd, odd); |
|||
std::vector<ValueType> b = totalRewardVector.template toVector<ValueType>(model.getNondeterminismVariables(), odd, explicitMatrix.getRowGroupIndices()); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(explicitMatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, x, &b, stepBound); |
|||
|
|||
// Return a hybrid check result that stores the numerical values explicitly.
|
|||
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().getAddZero(), model.getReachableStates(), odd, x)); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<DdType, ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, bool qualitative) { |
|||
|
|||
// Only compute the result if there is at least one reward model.
|
|||
STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
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.getReachableStates(), targetStates)); |
|||
} else { |
|||
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(); |
|||
STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states."); |
|||
STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// Check whether we need to compute exact rewards for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values
|
|||
// are neither 0 nor infinity.
|
|||
return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.toAdd() * model.getManager().getConstant(storm::utility::one<ValueType>()))); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the state reward vector to use in the computation.
|
|||
storm::dd::Add<DdType> subvector = stateRewardVector ? maybeStatesAdd * stateRewardVector.get() : model.getManager().getAddZero(); |
|||
if (transitionRewardMatrix) { |
|||
subvector += (submatrix * transitionRewardMatrix.get()).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()); |
|||
|
|||
// Create the solution vector.
|
|||
std::vector<ValueType> x(maybeStates.getNonZeroCount(), ValueType(0.5)); |
|||
|
|||
// 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(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 { |
|||
return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType>(model.getReachableStates(), infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()))); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,34 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include "src/models/symbolic/Model.h" |
|||
|
|||
#include "src/storage/dd/Add.h" |
|||
#include "src/storage/dd/Bdd.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
class HybridMdpPrctlHelper { |
|||
public: |
|||
static std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static storm::dd::Add<DdType> computeNextProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates); |
|||
|
|||
static std::unique_ptr<CheckResult> computeUntilProbabilities(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeCumulativeRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeInstantaneousRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::unique_ptr<CheckResult> computeReachabilityRewards(bool minimize, storm::models::symbolic::NondeterministicModel<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ */ |
|||
@ -0,0 +1,196 @@ |
|||
#include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/vector.h"
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
|
|||
storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, stepBound); |
|||
maybeStates &= ~psiStates; |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
if (!maybeStates.empty()) { |
|||
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); |
|||
|
|||
// Create the vector of one-step probabilities to go to target states.
|
|||
std::vector<ValueType> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates); |
|||
|
|||
// Create the vector with which to multiply.
|
|||
std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(submatrix); |
|||
solver->performMatrixVectorMultiplication(subresult, &b, stepBound); |
|||
|
|||
// Set the values of the resulting vector accordingly.
|
|||
storm::utility::vector::setVectorValues(result, maybeStates, subresult); |
|||
} |
|||
storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e.
|
|||
// all states that have probability 0 and 1 of satisfying the until-formula.
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiStates, psiStates); |
|||
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); |
|||
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); |
|||
|
|||
// Perform some logging.
|
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
|||
STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(transitionMatrix.getRowCount()); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5)); |
|||
} else { |
|||
if (!maybeStates.empty()) { |
|||
// In this case we have have to compute the probabilities.
|
|||
|
|||
// We can eliminate the rows and columns from the original transition probability matrix.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); |
|||
|
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation
|
|||
// system. That is, we go from x = A*x + b to (I-A)x = b.
|
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 0.5 for each element. This is the initial guess for
|
|||
// the iterative solvers. It should be safe as for all 'maybe' states we know that the
|
|||
// probability is strictly larger than 0.
|
|||
std::vector<ValueType> x(maybeStates.getNumberOfSetBits(), ValueType(0.5)); |
|||
|
|||
// 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<ValueType> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Now solve the created system of linear equations.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(submatrix); |
|||
solver->solveEquationSystem(x, b); |
|||
|
|||
// Set values of resulting vector according to result.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x); |
|||
} |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>()); |
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// Create the vector with which to multiply and initialize it correctly.
|
|||
std::vector<ValueType> result(transitionMatrix.getRowCount()); |
|||
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>()); |
|||
|
|||
// Perform one single matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(result); |
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// Compute the reward vector to add in each step based on the available reward models.
|
|||
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); |
|||
|
|||
// Initialize result to either the state rewards of the model or the null vector.
|
|||
std::vector<ValueType> result = rewardModel.getTotalStateActionRewardVector(transitionMatrix.getRowCount(), transitionMatrix.getRowGroupIndices()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(result, &totalRewardVector, stepBound); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has a state-based reward this->getModel().
|
|||
STORM_LOG_THROW(rewardModel.hasStateRewards() || rewardModel.hasStateActionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Initialize result to state rewards of the model.
|
|||
std::vector<ValueType> result = rewardModel.getTotalStateActionRewardVector(transitionMatrix.getRowCount(), transitionMatrix.getRowGroupIndices()); |
|||
|
|||
// Perform the matrix vector multiplication as often as required by the formula bound.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(result, nullptr, stepCount); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) { |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); |
|||
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(backwardTransitions, trueStates, targetStates); |
|||
infinityStates.complement(); |
|||
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; |
|||
STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); |
|||
STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
// Check whether we need to compute exact rewards for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values
|
|||
// are neither 0 nor infinity.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>()); |
|||
} else { |
|||
// In this case we have to compute the reward values for the remaining states.
|
|||
// We can eliminate the rows and columns from the original transition probability matrix.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true); |
|||
|
|||
// Converting the matrix from the fixpoint notation to the form needed for the equation
|
|||
// system. That is, we go from x = A*x + b to (I-A)x = b.
|
|||
submatrix.convertToEquationSystem(); |
|||
|
|||
// Initialize the x vector with 1 for each element. This is the initial guess for
|
|||
// the iterative solvers.
|
|||
std::vector<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>()); |
|||
|
|||
// Prepare the right-hand side of the equation system.
|
|||
std::vector<ValueType> b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates); |
|||
|
|||
// Now solve the resulting equation system.
|
|||
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(submatrix); |
|||
solver->solveEquationSystem(x, b); |
|||
|
|||
// Set values of resulting vector according to result.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template class SparseDtmcPrctlHelper<double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,39 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include <vector> |
|||
|
|||
#include "src/models/sparse/StandardRewardModel.h" |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/BitVector.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class SparseDtmcPrctlHelper { |
|||
public: |
|||
static std::vector<ValueType> computeBoundedUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeNextProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeUntilProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeLongRunAverage(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory); |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ */ |
|||
@ -0,0 +1,407 @@ |
|||
#include "src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
|
|||
|
|||
#include "src/storage/MaximalEndComponentDecomposition.h"
|
|||
|
|||
#include "src/utility/macros.h"
|
|||
#include "src/utility/vector.h"
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/exceptions/InvalidStateException.h"
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); |
|||
|
|||
// Determine the states that have 0 probability of reaching the target states.
|
|||
storm::storage::BitVector maybeStates; |
|||
if (minimize) { |
|||
maybeStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); |
|||
} else { |
|||
maybeStates = storm::utility::graph::performProbGreater0E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates, true, stepBound); |
|||
} |
|||
maybeStates &= ~psiStates; |
|||
STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
if (!maybeStates.empty()) { |
|||
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); |
|||
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, psiStates); |
|||
|
|||
// Create the vector with which to multiply.
|
|||
std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits()); |
|||
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(submatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, subresult, &b, stepBound); |
|||
|
|||
// Set the values of the resulting vector accordingly.
|
|||
storm::utility::vector::setVectorValues(result, maybeStates, subresult); |
|||
} |
|||
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeNextProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
// Create the vector with which to multiply and initialize it correctly.
|
|||
std::vector<ValueType> result(transitionMatrix.getRowCount()); |
|||
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::one<ValueType>()); |
|||
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, result); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); |
|||
|
|||
// We need to identify the states which have to be taken out of the matrix, i.e.
|
|||
// all states that have probability 0 and 1 of satisfying the until-formula.
|
|||
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01; |
|||
if (minimize) { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Min(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); |
|||
} else { |
|||
statesWithProbability01 = storm::utility::graph::performProb01Max(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, phiStates, psiStates); |
|||
} |
|||
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first); |
|||
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second); |
|||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(numberOfStates); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, ValueType(0.5)); |
|||
} else { |
|||
if (!maybeStates.empty()) { |
|||
// In this case we have have to compute the probabilities.
|
|||
|
|||
// First, we can eliminate the rows and columns from the original transition probability matrix for states
|
|||
// whose probabilities are already known.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); |
|||
|
|||
// 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<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1); |
|||
|
|||
// Create vector for results for maybe states.
|
|||
std::vector<ValueType> x(maybeStates.getNumberOfSetBits()); |
|||
|
|||
// Solve the corresponding system of equations.
|
|||
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); |
|||
} |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability0, storm::utility::zero<ValueType>()); |
|||
storm::utility::vector::setVectorValues<ValueType>(result, statesWithProbability1, storm::utility::one<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, bool minimize, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
// Only compute the result if the model has a state-based reward this->getModel().
|
|||
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Initialize result to state rewards of the this->getModel().
|
|||
std::vector<ValueType> result(rewardModel.getStateRewardVector()); |
|||
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, result, nullptr, stepCount); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, bool minimize, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Compute the reward vector to add in each step based on the available reward models.
|
|||
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(transitionMatrix); |
|||
|
|||
// Initialize result to either the state rewards of the model or the null vector.
|
|||
std::vector<ValueType> result; |
|||
if (rewardModel.hasStateRewards()) { |
|||
result = rewardModel.getStateRewardVector(); |
|||
} else { |
|||
result.resize(transitionMatrix.getRowCount()); |
|||
} |
|||
|
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(transitionMatrix); |
|||
solver->performMatrixVectorMultiplication(minimize, result, &totalRewardVector, stepBound); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
storm::storage::BitVector infinityStates; |
|||
storm::storage::BitVector trueStates(transitionMatrix.getRowCount(), true); |
|||
if (minimize) { |
|||
infinityStates = std::move(storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates)); |
|||
} else { |
|||
infinityStates = std::move(storm::utility::graph::performProb1E(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, targetStates)); |
|||
} |
|||
infinityStates.complement(); |
|||
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates; |
|||
LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states."); |
|||
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|||
|
|||
// Create resulting vector.
|
|||
std::vector<ValueType> result(transitionMatrix.getRowCount()); |
|||
|
|||
// Check whether we need to compute exact rewards for some states.
|
|||
if (qualitative) { |
|||
LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed."); |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values
|
|||
// are neither 0 nor infinity.
|
|||
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>()); |
|||
} else { |
|||
// In this case we have to compute the reward values for the remaining states.
|
|||
|
|||
// We can eliminate the rows and columns from the original transition probability matrix for states
|
|||
// whose reward values are already known.
|
|||
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); |
|||
|
|||
// Prepare the right-hand side of the equation system.
|
|||
std::vector<ValueType> b = rewardModel.getTotalRewardVector(submatrix.getRowCount(), transitionMatrix, maybeStates); |
|||
|
|||
// Create vector for results for maybe states.
|
|||
std::vector<ValueType> x(maybeStates.getNumberOfSetBits()); |
|||
|
|||
// Solve the corresponding system of equations.
|
|||
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); |
|||
} |
|||
|
|||
// Set values of resulting vector that are known exactly.
|
|||
storm::utility::vector::setVectorValues(result, targetStates, storm::utility::zero<ValueType>()); |
|||
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::infinity<ValueType>()); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
std::vector<ValueType> SparseMdpPrctlHelper<ValueType, RewardModelType>::computeLongRunAverage(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { |
|||
// If there are no goal states, we avoid the computation and directly return zero.
|
|||
uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); |
|||
if (psiStates.empty()) { |
|||
return std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>()); |
|||
} |
|||
|
|||
// Likewise, if all bits are set, we can avoid the computation and set.
|
|||
if ((~psiStates).empty()) { |
|||
return std::vector<ValueType>(numberOfStates, storm::utility::one<ValueType>()); |
|||
} |
|||
|
|||
// Start by decomposing the MDP into its MECs.
|
|||
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(transitionMatrix, backwardTransitions); |
|||
|
|||
// Get some data members for convenience.
|
|||
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); |
|||
ValueType zero = storm::utility::zero<ValueType>(); |
|||
|
|||
//first calculate LRA for the Maximal End Components.
|
|||
storm::storage::BitVector statesInMecs(numberOfStates); |
|||
std::vector<uint_fast64_t> stateToMecIndexMap(transitionMatrix.getColumnCount()); |
|||
std::vector<ValueType> lraValuesForEndComponents(mecDecomposition.size(), zero); |
|||
|
|||
for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) { |
|||
storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex]; |
|||
|
|||
lraValuesForEndComponents[currentMecIndex] = computeLraForMaximalEndComponent(minimize, transitionMatrix, psiStates, mec); |
|||
|
|||
// Gather information for later use.
|
|||
for (auto const& stateChoicesPair : mec) { |
|||
statesInMecs.set(stateChoicesPair.first); |
|||
stateToMecIndexMap[stateChoicesPair.first] = currentMecIndex; |
|||
} |
|||
} |
|||
|
|||
// For fast transition rewriting, we build some auxiliary data structures.
|
|||
storm::storage::BitVector statesNotContainedInAnyMec = ~statesInMecs; |
|||
uint_fast64_t firstAuxiliaryStateIndex = statesNotContainedInAnyMec.getNumberOfSetBits(); |
|||
uint_fast64_t lastStateNotInMecs = 0; |
|||
uint_fast64_t numberOfStatesNotInMecs = 0; |
|||
std::vector<uint_fast64_t> statesNotInMecsBeforeIndex; |
|||
statesNotInMecsBeforeIndex.reserve(numberOfStates); |
|||
for (auto state : statesNotContainedInAnyMec) { |
|||
while (lastStateNotInMecs <= state) { |
|||
statesNotInMecsBeforeIndex.push_back(numberOfStatesNotInMecs); |
|||
++lastStateNotInMecs; |
|||
} |
|||
++numberOfStatesNotInMecs; |
|||
} |
|||
|
|||
// Finally, we are ready to create the SSP matrix and right-hand side of the SSP.
|
|||
std::vector<ValueType> b; |
|||
typename storm::storage::SparseMatrixBuilder<ValueType> sspMatrixBuilder(0, 0, 0, false, true, numberOfStatesNotInMecs + mecDecomposition.size()); |
|||
|
|||
// If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications).
|
|||
uint_fast64_t currentChoice = 0; |
|||
for (auto state : statesNotContainedInAnyMec) { |
|||
sspMatrixBuilder.newRowGroup(currentChoice); |
|||
|
|||
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice, ++currentChoice) { |
|||
std::vector<ValueType> auxiliaryStateToProbabilityMap(mecDecomposition.size()); |
|||
b.push_back(storm::utility::zero<ValueType>()); |
|||
|
|||
for (auto element : transitionMatrix.getRow(choice)) { |
|||
if (statesNotContainedInAnyMec.get(element.getColumn())) { |
|||
// If the target state is not contained in an MEC, we can copy over the entry.
|
|||
sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); |
|||
} else { |
|||
// If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector
|
|||
// so that we are able to write the cumulative probability to the MEC into the matrix.
|
|||
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); |
|||
} |
|||
} |
|||
|
|||
// Now insert all (cumulative) probability values that target an MEC.
|
|||
for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { |
|||
if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { |
|||
sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Now we are ready to construct the choices for the auxiliary states.
|
|||
for (uint_fast64_t mecIndex = 0; mecIndex < mecDecomposition.size(); ++mecIndex) { |
|||
storm::storage::MaximalEndComponent const& mec = mecDecomposition[mecIndex]; |
|||
sspMatrixBuilder.newRowGroup(currentChoice); |
|||
|
|||
for (auto const& stateChoicesPair : mec) { |
|||
uint_fast64_t state = stateChoicesPair.first; |
|||
boost::container::flat_set<uint_fast64_t> const& choicesInMec = stateChoicesPair.second; |
|||
|
|||
for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) { |
|||
std::vector<ValueType> auxiliaryStateToProbabilityMap(mecDecomposition.size()); |
|||
|
|||
// If the choice is not contained in the MEC itself, we have to add a similar distribution to the auxiliary state.
|
|||
if (choicesInMec.find(choice) == choicesInMec.end()) { |
|||
b.push_back(storm::utility::zero<ValueType>()); |
|||
|
|||
for (auto element : transitionMatrix.getRow(choice)) { |
|||
if (statesNotContainedInAnyMec.get(element.getColumn())) { |
|||
// If the target state is not contained in an MEC, we can copy over the entry.
|
|||
sspMatrixBuilder.addNextValue(currentChoice, statesNotInMecsBeforeIndex[element.getColumn()], element.getValue()); |
|||
} else { |
|||
// If the target state is contained in MEC i, we need to add the probability to the corresponding field in the vector
|
|||
// so that we are able to write the cumulative probability to the MEC into the matrix.
|
|||
auxiliaryStateToProbabilityMap[stateToMecIndexMap[element.getColumn()]] += element.getValue(); |
|||
} |
|||
} |
|||
|
|||
// Now insert all (cumulative) probability values that target an MEC.
|
|||
for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { |
|||
if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { |
|||
sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); |
|||
} |
|||
} |
|||
|
|||
++currentChoice; |
|||
} |
|||
} |
|||
} |
|||
|
|||
// For each auxiliary state, there is the option to achieve the reward value of the LRA associated with the MEC.
|
|||
++currentChoice; |
|||
b.push_back(lraValuesForEndComponents[mecIndex]); |
|||
} |
|||
|
|||
// Finalize the matrix and solve the corresponding system of equations.
|
|||
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice); |
|||
|
|||
std::vector<ValueType> sspResult(numberOfStatesNotInMecs + mecDecomposition.size()); |
|||
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix); |
|||
solver->solveEquationSystem(minimize, sspResult, b); |
|||
|
|||
// Prepare result vector.
|
|||
std::vector<ValueType> result(numberOfStates, zero); |
|||
|
|||
// Set the values for states not contained in MECs.
|
|||
storm::utility::vector::setVectorValues(result, statesNotContainedInAnyMec, sspResult); |
|||
|
|||
// Set the values for all states in MECs.
|
|||
for (auto state : statesInMecs) { |
|||
result[state] = sspResult[firstAuxiliaryStateIndex + stateToMecIndexMap[state]]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
template<typename ValueType, typename RewardModelType> |
|||
ValueType SparseMdpPrctlHelper<ValueType, RewardModelType>::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec) { |
|||
std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC"); |
|||
solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); |
|||
|
|||
//// First, we need to create the variables for the problem.
|
|||
std::map<uint_fast64_t, storm::expressions::Variable> stateToVariableMap; |
|||
for (auto const& stateChoicesPair : mec) { |
|||
std::string variableName = "h" + std::to_string(stateChoicesPair.first); |
|||
stateToVariableMap[stateChoicesPair.first] = solver->addUnboundedContinuousVariable(variableName); |
|||
} |
|||
storm::expressions::Variable lambda = solver->addUnboundedContinuousVariable("L", 1); |
|||
solver->update(); |
|||
|
|||
// Now we encode the problem as constraints.
|
|||
for (auto const& stateChoicesPair : mec) { |
|||
uint_fast64_t state = stateChoicesPair.first; |
|||
|
|||
// Now, based on the type of the state, create a suitable constraint.
|
|||
for (auto choice : stateChoicesPair.second) { |
|||
storm::expressions::Expression constraint = -lambda; |
|||
ValueType r = 0; |
|||
|
|||
for (auto element : transitionMatrix.getRow(choice)) { |
|||
constraint = constraint + stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); |
|||
if (psiStates.get(element.getColumn())) { |
|||
r += element.getValue(); |
|||
} |
|||
} |
|||
constraint = solver->getConstant(r) + constraint; |
|||
|
|||
if (minimize) { |
|||
constraint = stateToVariableMap.at(state) <= constraint; |
|||
} else { |
|||
constraint = stateToVariableMap.at(state) >= constraint; |
|||
} |
|||
solver->addConstraint("state" + std::to_string(state) + "," + std::to_string(choice), constraint); |
|||
} |
|||
} |
|||
|
|||
solver->optimize(); |
|||
return solver->getContinuousValue(lambda); |
|||
} |
|||
|
|||
template class SparseMdpPrctlHelper<double>; |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,45 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include <vector> |
|||
|
|||
#include "src/models/sparse/StandardRewardModel.h" |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/storage/BitVector.h" |
|||
#include "src/storage/MaximalEndComponent.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>> |
|||
class SparseMdpPrctlHelper { |
|||
public: |
|||
static std::vector<ValueType> computeBoundedUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeNextProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeUntilProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& MinMaxLinearEquationSolverFactory, bool qualitative); |
|||
|
|||
static std::vector<ValueType> computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, bool minimize, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, bool minimize, uint_fast64_t stepBound, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeReachabilityRewards(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
static std::vector<ValueType> computeLongRunAverage(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); |
|||
|
|||
private: |
|||
static ValueType computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSE_MDP_PRCTL_MODELCHECKER_HELPER_H_ */ |
|||
@ -0,0 +1,195 @@ |
|||
#include "src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.h"
|
|||
|
|||
#include "src/storage/dd/DdType.h"
|
|||
#include "src/storage/dd/CuddAdd.h"
|
|||
#include "src/storage/dd/CuddBdd.h"
|
|||
#include "src/storage/dd/CuddOdd.h"
|
|||
|
|||
#include "src/utility/graph.h"
|
|||
|
|||
#include "src/exceptions/InvalidPropertyException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
|
|||
// probability 0 and 1 of satisfying the until-formula.
|
|||
std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> statesWithProbability01 = storm::utility::graph::performProb01(model, transitionMatrix, phiStates, psiStates); |
|||
storm::dd::Bdd<DdType> maybeStates = !statesWithProbability01.first && !statesWithProbability01.second && model.getReachableStates(); |
|||
|
|||
// Perform some logging.
|
|||
STORM_LOG_INFO("Found " << statesWithProbability01.first.getNonZeroCount() << " 'no' states."); |
|||
STORM_LOG_INFO("Found " << statesWithProbability01.second.getNonZeroCount() << " 'yes' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// Check whether we need to compute exact probabilities for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
|
|||
return statesWithProbability01.second.toAdd() + maybeStates.toAdd() * model.getManager().getConstant(0.5); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
storm::dd::Add<DdType> prob1StatesAsColumn = statesWithProbability01.second.toAdd(); |
|||
prob1StatesAsColumn = prob1StatesAsColumn.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
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)).
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; |
|||
|
|||
// Solve the equation system.
|
|||
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); |
|||
|
|||
return statesWithProbability01.second.toAdd() + result; |
|||
} else { |
|||
return statesWithProbability01.second.toAdd(); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeNextProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates) { |
|||
storm::dd::Add<DdType> result = transitionMatrix * nextStates.swapVariables(model.getRowColumnMetaVariablePairs()).toAdd(); |
|||
return result.sumAbstract(model.getColumnVariables()); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// We need to identify the states which have to be taken out of the matrix, i.e. all states that have
|
|||
// probability 0 or 1 of satisfying the until-formula.
|
|||
storm::dd::Bdd<DdType> statesWithProbabilityGreater0 = storm::utility::graph::performProbGreater0(model, transitionMatrix.notZero(), phiStates, psiStates, stepBound); |
|||
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.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
|
|||
// maybe states.
|
|||
storm::dd::Add<DdType> prob1StatesAsColumn = psiStates.toAdd().swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> subvector = (submatrix * prob1StatesAsColumn).sumAbstract(model.getColumnVariables()); |
|||
|
|||
// Finally cut away all columns targeting non-maybe states.
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->performMatrixVectorMultiplication(model.getManager().getAddZero(), &subvector, stepBound); |
|||
|
|||
return psiStates.toAdd() + result; |
|||
} else { |
|||
return psiStates.toAdd(); |
|||
} |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeCumulativeRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(model.hasStateRewards() || model.hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Compute the reward vector to add in each step based on the available reward models.
|
|||
storm::dd::Add<DdType> totalRewardVector = model.hasStateRewards() ? model.getStateRewardVector() : model.getManager().getAddZero(); |
|||
if (model.hasTransitionRewards()) { |
|||
totalRewardVector += (transitionMatrix * model.getTransitionRewardMatrix()).sumAbstract(model.getColumnVariables()); |
|||
} |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); |
|||
return solver->performMatrixVectorMultiplication(model.getManager().getAddZero(), &totalRewardVector, stepBound); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
// Only compute the result if the model has at least one reward this->getModel().
|
|||
STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Perform the matrix-vector multiplication.
|
|||
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(transitionMatrix, model.getReachableStates(), model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); |
|||
return solver->performMatrixVectorMultiplication(model.getStateRewardVector(), nullptr, stepBound); |
|||
} |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
storm::dd::Add<DdType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) { |
|||
|
|||
// Only compute the result if there is at least one reward model.
|
|||
STORM_LOG_THROW(stateRewardVector || transitionRewardMatrix, storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); |
|||
|
|||
// Determine which states have a reward of infinity by definition.
|
|||
storm::dd::Bdd<DdType> infinityStates = storm::utility::graph::performProb1(model, transitionMatrix.notZero(), model.getReachableStates(), targetStates); |
|||
infinityStates = !infinityStates && model.getReachableStates(); |
|||
storm::dd::Bdd<DdType> maybeStates = (!targetStates && !infinityStates) && model.getReachableStates(); |
|||
STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states."); |
|||
STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states."); |
|||
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states."); |
|||
|
|||
// Check whether we need to compute exact rewards for some states.
|
|||
if (qualitative) { |
|||
// Set the values for all maybe-states to 1 to indicate that their reward values
|
|||
// are neither 0 nor infinity.
|
|||
return infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + maybeStates.toAdd() * model.getManager().getConstant(storm::utility::one<ValueType>()); |
|||
} else { |
|||
// If there are maybe states, we need to solve an equation system.
|
|||
if (!maybeStates.isZero()) { |
|||
// Create the ODD for the translation between symbolic and explicit storage.
|
|||
storm::dd::Odd<DdType> odd(maybeStates); |
|||
|
|||
// Create the matrix and the vector for the equation system.
|
|||
storm::dd::Add<DdType> maybeStatesAdd = maybeStates.toAdd(); |
|||
|
|||
// Start by cutting away all rows that do not belong to maybe states. Note that this leaves columns targeting
|
|||
// non-maybe states in the matrix.
|
|||
storm::dd::Add<DdType> submatrix = transitionMatrix * maybeStatesAdd; |
|||
|
|||
// Then compute the state reward vector to use in the computation.
|
|||
storm::dd::Add<DdType> subvector = stateRewardVector ? maybeStatesAdd * stateRewardVector.get() : model.getManager().getAddZero(); |
|||
if (transitionRewardMatrix) { |
|||
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)).
|
|||
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs()); |
|||
submatrix = (model.getRowColumnIdentity() * maybeStatesAdd) - submatrix; |
|||
|
|||
// Solve the equation system.
|
|||
std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); |
|||
storm::dd::Add<DdType> result = solver->solveEquationSystem(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); |
|||
|
|||
return infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()) + result; |
|||
} else { |
|||
return infinityStates.toAdd() * model.getManager().getConstant(storm::utility::infinity<ValueType>()); |
|||
} |
|||
} |
|||
} |
|||
|
|||
template class SymbolicDtmcPrctlHelper<storm::dd::DdType::CUDD, double>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,35 @@ |
|||
#ifndef STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ |
|||
#define STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ |
|||
|
|||
#include "src/models/symbolic/Model.h" |
|||
|
|||
#include "src/storage/dd/Add.h" |
|||
#include "src/storage/dd/Bdd.h" |
|||
|
|||
#include "src/utility/solver.h" |
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template<storm::dd::DdType DdType, typename ValueType> |
|||
class SymbolicDtmcPrctlHelper { |
|||
public: |
|||
static storm::dd::Add<DdType> computeBoundedUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static storm::dd::Add<DdType> computeNextProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& nextStates); |
|||
|
|||
static storm::dd::Add<DdType> computeUntilProbabilities(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, storm::dd::Bdd<DdType> const& phiStates, storm::dd::Bdd<DdType> const& psiStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static storm::dd::Add<DdType> computeCumulativeRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static storm::dd::Add<DdType> computeInstantaneousRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, uint_fast64_t stepBound, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
|
|||
static storm::dd::Add<DdType> computeReachabilityRewards(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& transitionMatrix, boost::optional<storm::dd::Add<DdType>> const& stateRewardVector, boost::optional<storm::dd::Add<DdType>> const& transitionRewardMatrix, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory); |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* STORM_MODELCHECKER_SPARSE_DTMC_PRCTL_MODELCHECKER_HELPER_H_ */ |
|||
Reference in new issue
xxxxxxxxxx