Browse Source
Merge branch 'master' into PrctlParser
Merge branch 'master' into PrctlParser
Conflicts: src/modelchecker/AbstractModelChecker.h src/modelchecker/GmmxxDtmcPrctlModelChecker.hmain
Lanchid
14 years ago
51 changed files with 1496 additions and 1500 deletions
-
41CMakeLists.txt
-
2src/formula/AbstractPathFormula.h
-
2src/formula/AbstractStateFormula.h
-
2src/formula/And.h
-
2src/formula/Ap.h
-
2src/formula/BoundedEventually.h
-
2src/formula/BoundedNaryUntil.h
-
2src/formula/BoundedUntil.h
-
2src/formula/CumulativeReward.h
-
2src/formula/Eventually.h
-
3src/formula/Formulas.h
-
2src/formula/Globally.h
-
2src/formula/InstantaneousReward.h
-
2src/formula/Next.h
-
2src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
2src/formula/Or.h
-
2src/formula/ProbabilisticBoundOperator.h
-
2src/formula/ReachabilityReward.h
-
2src/formula/RewardBoundOperator.h
-
2src/formula/StateBoundOperator.h
-
2src/formula/SteadyStateOperator.h
-
2src/formula/SteadyStateReward.h
-
2src/formula/Until.h
-
182src/modelchecker/AbstractModelChecker.h
-
411src/modelchecker/DtmcPrctlModelChecker.h
-
12src/modelchecker/EigenDtmcPrctlModelChecker.h
-
14src/modelchecker/ForwardDeclarations.h
-
220src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
83src/modelchecker/GmmxxMdpPrctlModelChecker.h
-
454src/modelchecker/SparseDtmcPrctlModelChecker.h
-
407src/modelchecker/SparseMdpPrctlModelChecker.h
-
68src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
-
6src/models/Dtmc.h
-
44src/models/GraphTransitions.h
-
12src/parser/PrctlFileParser.cpp
-
2src/parser/PrctlFileParser.h
-
744src/storage/SparseMatrix.h
-
16src/storm.cpp
-
28src/utility/GraphAnalyzer.h
-
71src/utility/IoUtility.cpp
-
45src/utility/IoUtility.h
-
12src/utility/Vector.h
-
6test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
-
8test/functional/GmmxxMdpPrctModelCheckerTest.cpp
-
25test/parser/ParseDtmcTest.cpp
-
1test/parser/ParseMdpTest.cpp
-
29test/parser/ReadLabFileTest.cpp
-
2test/parser/ReadTraFileTest.cpp
-
4test/storage/SparseMatrixTest.cpp
-
2test/storm-tests.cpp
@ -1,411 +0,0 @@ |
|||||
/* |
|
||||
* DtmcPrctlModelChecker.h |
|
||||
* |
|
||||
* Created on: 22.10.2012 |
|
||||
* Author: Thomas Heinemann |
|
||||
*/ |
|
||||
|
|
||||
#ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ |
|
||||
#define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ |
|
||||
|
|
||||
#include <vector> |
|
||||
|
|
||||
#include "src/formula/Formulas.h" |
|
||||
#include "src/utility/Vector.h" |
|
||||
#include "src/storage/SparseMatrix.h" |
|
||||
|
|
||||
#include "src/models/Dtmc.h" |
|
||||
#include "src/storage/BitVector.h" |
|
||||
#include "src/exceptions/InvalidPropertyException.h" |
|
||||
#include "src/utility/Vector.h" |
|
||||
#include "src/utility/GraphAnalyzer.h" |
|
||||
#include "src/modelchecker/AbstractModelChecker.h" |
|
||||
|
|
||||
#include "log4cplus/logger.h" |
|
||||
#include "log4cplus/loggingmacros.h" |
|
||||
extern log4cplus::Logger logger; |
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
namespace modelChecker { |
|
||||
|
|
||||
/*! |
|
||||
* @brief |
|
||||
* Interface for model checker classes. |
|
||||
* |
|
||||
* This class provides basic functions that are the same for all subclasses, but mainly only declares |
|
||||
* abstract methods that are to be implemented in concrete instances. |
|
||||
* |
|
||||
* @attention This class is abstract. |
|
||||
*/ |
|
||||
template<class Type> |
|
||||
class DtmcPrctlModelChecker : public AbstractModelChecker<Type> { |
|
||||
|
|
||||
public: |
|
||||
/*! |
|
||||
* Constructor |
|
||||
* |
|
||||
* @param model The dtmc model which is checked. |
|
||||
*/ |
|
||||
explicit DtmcPrctlModelChecker(storm::models::Dtmc<Type>& model) : AbstractModelChecker<Type>(model) { |
|
||||
// Intentionally left empty. |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* Copy constructor |
|
||||
* |
|
||||
* @param modelChecker The model checker that is copied. |
|
||||
*/ |
|
||||
explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker<Type>* modelChecker) : AbstractModelChecker<Type>(modelChecker) { |
|
||||
// Intentionally left empty. |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* Destructor |
|
||||
*/ |
|
||||
virtual ~DtmcPrctlModelChecker() { |
|
||||
// Intentionally left empty. |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* @returns A reference to the dtmc of the model checker. |
|
||||
*/ |
|
||||
storm::models::Dtmc<Type>& getModel() const { |
|
||||
return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>(); |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a state formula with a probabilistic operator node without bounds as root |
|
||||
* in its formula tree |
|
||||
* |
|
||||
* @param formula The state formula to check |
|
||||
* @returns The set of states satisfying the formula, represented by a bit vector |
|
||||
*/ |
|
||||
std::vector<Type>* checkNoBoundOperator(const storm::formula::NoBoundOperator<Type>& formula) const { |
|
||||
// Check if the operator was an optimality operator and report a warning in that case. |
|
||||
if (formula.isOptimalityOperator()) { |
|
||||
LOG4CPLUS_WARN(logger, "Formula contains min/max operator which is not meaningful over deterministic models."); |
|
||||
} |
|
||||
return formula.getPathFormula().check(*this, false); |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Bounded Until operator node as root in its formula tree |
|
||||
* |
|
||||
* @param formula The Bounded Until path formula to check |
|
||||
* @returns for each state the probability that the path formula holds. |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkBoundedUntil(const storm::formula::BoundedUntil<Type>& formula, bool qualitative) const { |
|
||||
// First, we need to compute the states that satisfy the sub-formulas of the until-formula. |
|
||||
storm::storage::BitVector* leftStates = formula.getLeft().check(*this); |
|
||||
storm::storage::BitVector* rightStates = formula.getRight().check(*this); |
|
||||
|
|
||||
// Copy the matrix before we make any changes. |
|
||||
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix()); |
|
||||
|
|
||||
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. |
|
||||
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); |
|
||||
|
|
||||
// Delete obsolete intermediates. |
|
||||
delete leftStates; |
|
||||
delete rightStates; |
|
||||
|
|
||||
// Create the vector with which to multiply. |
|
||||
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|
||||
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>()); |
|
||||
|
|
||||
// Perform the matrix vector multiplication as often as required by the formula bound. |
|
||||
this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); |
|
||||
|
|
||||
// Return result. |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Next operator node as root in its formula tree |
|
||||
* |
|
||||
* @param formula The Next path formula to check |
|
||||
* @returns for each state the probability that the path formula holds. |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const { |
|
||||
// First, we need to compute the states that satisfy the child formula of the next-formula. |
|
||||
storm::storage::BitVector* nextStates = formula.getChild().check(*this); |
|
||||
|
|
||||
// Create the vector with which to multiply and initialize it correctly. |
|
||||
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|
||||
storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>()); |
|
||||
|
|
||||
// Delete obsolete intermediate. |
|
||||
delete nextStates; |
|
||||
|
|
||||
// Perform one single matrix-vector multiplication. |
|
||||
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result); |
|
||||
|
|
||||
// Return result. |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Bounded Eventually operator node as root in its |
|
||||
* formula tree |
|
||||
* |
|
||||
* @param formula The Bounded Eventually path formula to check |
|
||||
* @returns for each state the probability that the path formula holds |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkBoundedEventually(const storm::formula::BoundedEventually<Type>& formula, bool qualitative) const { |
|
||||
// Create equivalent temporary bounded until formula and check it. |
|
||||
storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound()); |
|
||||
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with an Eventually operator node as root in its formula tree |
|
||||
* |
|
||||
* @param formula The Eventually path formula to check |
|
||||
* @returns for each state the probability that the path formula holds |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkEventually(const storm::formula::Eventually<Type>& formula, bool qualitative) const { |
|
||||
// Create equivalent temporary until formula and check it. |
|
||||
storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone()); |
|
||||
return this->checkUntil(temporaryUntilFormula, qualitative); |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Globally operator node as root in its formula tree |
|
||||
* |
|
||||
* @param formula The Globally path formula to check |
|
||||
* @returns for each state the probability that the path formula holds |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkGlobally(const storm::formula::Globally<Type>& formula, bool qualitative) const { |
|
||||
// Create "equivalent" temporary eventually formula and check it. |
|
||||
storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone())); |
|
||||
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative); |
|
||||
|
|
||||
// Now subtract the resulting vector from the constant one vector to obtain final result. |
|
||||
storm::utility::subtractFromConstantOneVector(result); |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with an Until operator node as root in its formula tree |
|
||||
* |
|
||||
* @param formula The Until path formula to check |
|
||||
* @returns for each state the probability that the path formula holds. |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkUntil(const storm::formula::Until<Type>& formula, bool qualitative) const { |
|
||||
// First, we need to compute the states that satisfy the sub-formulas of the until-formula. |
|
||||
storm::storage::BitVector* leftStates = formula.getLeft().check(*this); |
|
||||
storm::storage::BitVector* rightStates = formula.getRight().check(*this); |
|
||||
|
|
||||
// Then, 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. |
|
||||
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); |
|
||||
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); |
|
||||
storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); |
|
||||
|
|
||||
// Delete intermediate results that are obsolete now. |
|
||||
delete leftStates; |
|
||||
delete rightStates; |
|
||||
|
|
||||
// Perform some logging. |
|
||||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
|
||||
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
|
||||
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
|
||||
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
|
||||
|
|
||||
// Create resulting vector. |
|
||||
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|
||||
|
|
||||
// Only try to solve system if there are states for which the probability is unknown. |
|
||||
uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); |
|
||||
if (maybeStatesSetBitCount > 0 && !qualitative) { |
|
||||
// Now we can eliminate the rows and columns from the original transition probability matrix. |
|
||||
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); |
|
||||
// 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<Type> x(maybeStatesSetBitCount, Type(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<Type> b(maybeStatesSetBitCount); |
|
||||
this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b); |
|
||||
|
|
||||
this->solveEquationSystem(*submatrix, x, b); |
|
||||
|
|
||||
// Delete the created submatrix. |
|
||||
delete submatrix; |
|
||||
|
|
||||
// Set values of resulting vector according to result. |
|
||||
storm::utility::setVectorValues<Type>(result, maybeStates, x); |
|
||||
} else if (qualitative) { |
|
||||
// If we only need a qualitative result, we can safely assume that the results will only be compared to |
|
||||
// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. |
|
||||
storm::utility::setVectorValues<Type>(result, maybeStates, Type(0.5)); |
|
||||
} |
|
||||
|
|
||||
// Set values of resulting vector that are known exactly. |
|
||||
storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>()); |
|
||||
storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>()); |
|
||||
|
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with an Instantaneous Reward operator node as root in its |
|
||||
* formula tree |
|
||||
* |
|
||||
* @param formula The Instantaneous Reward formula to check |
|
||||
* @returns for each state the reward that the instantaneous reward yields |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkInstantaneousReward(const storm::formula::InstantaneousReward<Type>& formula, bool qualitative) const { |
|
||||
// Only compute the result if the model has a state-based reward model. |
|
||||
if (!this->getModel().hasStateRewards()) { |
|
||||
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); |
|
||||
throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; |
|
||||
} |
|
||||
|
|
||||
// Initialize result to state rewards of the model. |
|
||||
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
|
||||
|
|
||||
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. |
|
||||
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); |
|
||||
|
|
||||
// Return result. |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Cumulative Reward operator node as root in its |
|
||||
* formula tree |
|
||||
* |
|
||||
* @param formula The Cumulative Reward formula to check |
|
||||
* @returns for each state the reward that the cumulative reward yields |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkCumulativeReward(const storm::formula::CumulativeReward<Type>& formula, bool qualitative) const { |
|
||||
// Only compute the result if the model has at least one reward model. |
|
||||
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
|
||||
LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); |
|
||||
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
|
||||
} |
|
||||
|
|
||||
// Compute the reward vector to add in each step based on the available reward models. |
|
||||
std::vector<Type>* totalRewardVector = nullptr; |
|
||||
if (this->getModel().hasTransitionRewards()) { |
|
||||
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); |
|
||||
if (this->getModel().hasStateRewards()) { |
|
||||
gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); |
|
||||
} |
|
||||
} else { |
|
||||
totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
|
||||
} |
|
||||
|
|
||||
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
|
||||
|
|
||||
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); |
|
||||
|
|
||||
// Delete temporary variables and return result. |
|
||||
delete totalRewardVector; |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
/*! |
|
||||
* The check method for a path formula with a Reachability Reward operator node as root in its |
|
||||
* formula tree |
|
||||
* |
|
||||
* @param formula The Reachbility Reward formula to check |
|
||||
* @returns for each state the reward that the reachability reward yields |
|
||||
*/ |
|
||||
virtual std::vector<Type>* checkReachabilityReward(const storm::formula::ReachabilityReward<Type>& formula, bool qualitative) const { |
|
||||
// Only compute the result if the model has at least one reward model. |
|
||||
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
|
||||
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); |
|
||||
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
|
||||
} |
|
||||
|
|
||||
// Determine the states for which the target predicate holds. |
|
||||
storm::storage::BitVector* targetStates = formula.getChild().check(*this); |
|
||||
|
|
||||
// Determine which states have a reward of infinity by definition. |
|
||||
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); |
|
||||
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); |
|
||||
storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); |
|
||||
infinityStates.complement(); |
|
||||
|
|
||||
// Create resulting vector. |
|
||||
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|
||||
|
|
||||
// Check whether there are states for which we have to compute the result. |
|
||||
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; |
|
||||
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); |
|
||||
if (maybeStatesSetBitCount > 0) { |
|
||||
// Now we can eliminate the rows and columns from the original transition probability matrix. |
|
||||
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); |
|
||||
// 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<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>()); |
|
||||
|
|
||||
// Prepare the right-hand side of the equation system. |
|
||||
std::vector<Type> b(maybeStatesSetBitCount); |
|
||||
if (this->getModel().hasTransitionRewards()) { |
|
||||
// If a transition-based reward model is available, we initialize the right-hand |
|
||||
// side to the vector resulting from summing the rows of the pointwise product |
|
||||
// of the transition probability matrix and the transition reward matrix. |
|
||||
std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); |
|
||||
storm::utility::selectVectorValues(&b, maybeStates, *pointwiseProductRowSumVector); |
|
||||
delete pointwiseProductRowSumVector; |
|
||||
|
|
||||
if (this->getModel().hasStateRewards()) { |
|
||||
// If a state-based reward model is also available, we need to add this vector |
|
||||
// as well. As the state reward vector contains entries not just for the states |
|
||||
// that we still consider (i.e. maybeStates), we need to extract these values |
|
||||
// first. |
|
||||
std::vector<Type> subStateRewards(maybeStatesSetBitCount); |
|
||||
storm::utility::selectVectorValues(&subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); |
|
||||
gmm::add(subStateRewards, b); |
|
||||
} |
|
||||
} else { |
|
||||
// If only a state-based reward model is available, we take this vector as the |
|
||||
// right-hand side. As the state reward vector contains entries not just for the |
|
||||
// states that we still consider (i.e. maybeStates), we need to extract these values |
|
||||
// first. |
|
||||
storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector()); |
|
||||
} |
|
||||
|
|
||||
this->solveEquationSystem(*submatrix, x, b); |
|
||||
|
|
||||
// Set values of resulting vector according to result. |
|
||||
storm::utility::setVectorValues<Type>(result, maybeStates, x); |
|
||||
|
|
||||
// Delete temporary matrix and right-hand side. |
|
||||
delete submatrix; |
|
||||
} |
|
||||
|
|
||||
// Set values of resulting vector that are known exactly. |
|
||||
storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>()); |
|
||||
storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>()); |
|
||||
|
|
||||
// Delete temporary storages and return result. |
|
||||
delete targetStates; |
|
||||
return result; |
|
||||
} |
|
||||
|
|
||||
private: |
|
||||
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type>* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; |
|
||||
|
|
||||
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& matrix, std::vector<Type>& vector, std::vector<Type> const& b) const = 0; |
|
||||
}; |
|
||||
|
|
||||
} //namespace modelChecker |
|
||||
|
|
||||
} //namespace storm |
|
||||
|
|
||||
#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ |
|
||||
@ -0,0 +1,454 @@ |
|||||
|
/* |
||||
|
* SparseDtmcPrctlModelChecker.h |
||||
|
* |
||||
|
* Created on: 22.10.2012 |
||||
|
* Author: Thomas Heinemann |
||||
|
*/ |
||||
|
|
||||
|
#ifndef STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ |
||||
|
#define STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ |
||||
|
|
||||
|
#include "src/modelchecker/AbstractModelChecker.h" |
||||
|
#include "src/models/Dtmc.h" |
||||
|
#include "src/utility/Vector.h" |
||||
|
#include "src/utility/GraphAnalyzer.h" |
||||
|
|
||||
|
#include <vector> |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
|
||||
|
/*! |
||||
|
* @brief |
||||
|
* Interface for all model checkers that can verify PRCTL formulae over DTMCs represented as a sparse matrix. |
||||
|
*/ |
||||
|
template<class Type> |
||||
|
class SparseDtmcPrctlModelChecker : public AbstractModelChecker<Type> { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructs a SparseDtmcPrctlModelChecker with the given model. |
||||
|
* |
||||
|
* @param model The DTMC to be checked. |
||||
|
*/ |
||||
|
explicit SparseDtmcPrctlModelChecker(storm::models::Dtmc<Type> const& model) : AbstractModelChecker<Type>(model) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Copy constructs a SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly |
||||
|
* constructed model checker will have the model of the given model checker as its associated model. |
||||
|
*/ |
||||
|
explicit SparseDtmcPrctlModelChecker(storm::modelchecker::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker) { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Virtual destructor. Needs to be virtual, because this class has virtual methods. |
||||
|
*/ |
||||
|
virtual ~SparseDtmcPrctlModelChecker() { |
||||
|
// Intentionally left empty. |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Returns a constant reference to the DTMC associated with this model checker. |
||||
|
* @returns A constant reference to the DTMC associated with this model checker. |
||||
|
*/ |
||||
|
storm::models::Dtmc<Type> const& getModel() const { |
||||
|
return AbstractModelChecker<Type>::template getModel<storm::models::Dtmc<Type>>(); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a P/R operator without a bound. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @returns The set of states satisfying the formula represented by a bit vector. |
||||
|
*/ |
||||
|
std::vector<Type>* checkNoBoundOperator(storm::formula::NoBoundOperator<Type> const& formula) const { |
||||
|
// Check if the operator was an optimality operator and report a warning in that case. |
||||
|
if (formula.isOptimalityOperator()) { |
||||
|
LOG4CPLUS_WARN(logger, "Formula contains min/max operator, which is not meaningful over deterministic models."); |
||||
|
} |
||||
|
return formula.getPathFormula().check(*this, false); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a bounded-until formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkBoundedUntil(storm::formula::BoundedUntil<Type> const& formula, bool qualitative) const { |
||||
|
// First, we need to compute the states that satisfy the sub-formulas of the bounded until-formula. |
||||
|
storm::storage::BitVector* leftStates = formula.getLeft().check(*this); |
||||
|
storm::storage::BitVector* rightStates = formula.getRight().check(*this); |
||||
|
|
||||
|
// Copy the matrix before we make any changes. |
||||
|
storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix()); |
||||
|
|
||||
|
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. |
||||
|
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); |
||||
|
|
||||
|
// Delete obsolete intermediates. |
||||
|
delete leftStates; |
||||
|
delete rightStates; |
||||
|
|
||||
|
// Create the vector with which to multiply. |
||||
|
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
||||
|
storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne<Type>()); |
||||
|
|
||||
|
// Perform the matrix vector multiplication as often as required by the formula bound. |
||||
|
this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); |
||||
|
|
||||
|
// Return result. |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a next formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkNext(storm::formula::Next<Type> const& formula, bool qualitative) const { |
||||
|
// First, we need to compute the states that satisfy the child formula of the next-formula. |
||||
|
storm::storage::BitVector* nextStates = formula.getChild().check(*this); |
||||
|
|
||||
|
// Create the vector with which to multiply and initialize it correctly. |
||||
|
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
||||
|
storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne<Type>()); |
||||
|
|
||||
|
// Delete obsolete intermediate. |
||||
|
delete nextStates; |
||||
|
|
||||
|
// Perform one single matrix-vector multiplication. |
||||
|
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result); |
||||
|
|
||||
|
// Return result. |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a bounded-eventually formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkBoundedEventually(storm::formula::BoundedEventually<Type> const& formula, bool qualitative) const { |
||||
|
// Create equivalent temporary bounded until formula and check it. |
||||
|
storm::formula::BoundedUntil<Type> temporaryBoundedUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone(), formula.getBound()); |
||||
|
return this->checkBoundedUntil(temporaryBoundedUntilFormula, qualitative); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is an eventually formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkEventually(storm::formula::Eventually<Type> const& formula, bool qualitative) const { |
||||
|
// Create equivalent temporary until formula and check it. |
||||
|
storm::formula::Until<Type> temporaryUntilFormula(new storm::formula::Ap<Type>("true"), formula.getChild().clone()); |
||||
|
return this->checkUntil(temporaryUntilFormula, qualitative); |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a globally formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkGlobally(storm::formula::Globally<Type> const& formula, bool qualitative) const { |
||||
|
// Create "equivalent" (equivalent up to negation) temporary eventually formula and check it. |
||||
|
storm::formula::Eventually<Type> temporaryEventuallyFormula(new storm::formula::Not<Type>(formula.getChild().clone())); |
||||
|
std::vector<Type>* result = this->checkEventually(temporaryEventuallyFormula, qualitative); |
||||
|
|
||||
|
// Now subtract the resulting vector from the constant one vector to obtain final result. |
||||
|
storm::utility::subtractFromConstantOneVector(result); |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Check the given formula that is an until formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bounds 0 and 1. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bounds 0 and 1. |
||||
|
* @returns The probabilities for the given formula to hold on every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact probabilities might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkUntil(storm::formula::Until<Type> const& formula, bool qualitative) const { |
||||
|
// First, we need to compute the states that satisfy the sub-formulas of the until-formula. |
||||
|
storm::storage::BitVector* leftStates = formula.getLeft().check(*this); |
||||
|
storm::storage::BitVector* rightStates = formula.getRight().check(*this); |
||||
|
|
||||
|
// Then, 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. |
||||
|
storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); |
||||
|
storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); |
||||
|
storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); |
||||
|
|
||||
|
// Delete intermediate results that are obsolete now. |
||||
|
delete leftStates; |
||||
|
delete rightStates; |
||||
|
|
||||
|
// Perform some logging. |
||||
|
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); |
||||
|
LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); |
||||
|
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); |
||||
|
LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); |
||||
|
|
||||
|
// Create resulting vector. |
||||
|
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
||||
|
|
||||
|
// Only try to solve system if there are states for which the probability is unknown. |
||||
|
uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); |
||||
|
if (maybeStatesSetBitCount > 0 && !qualitative) { |
||||
|
// Now we can eliminate the rows and columns from the original transition probability matrix. |
||||
|
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); |
||||
|
// 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<Type> x(maybeStatesSetBitCount, Type(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<Type> b = this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1); |
||||
|
|
||||
|
// Now solve the created system of linear equations. |
||||
|
this->solveEquationSystem(submatrix, x, b); |
||||
|
|
||||
|
// Set values of resulting vector according to result. |
||||
|
storm::utility::setVectorValues<Type>(result, maybeStates, x); |
||||
|
} else if (qualitative) { |
||||
|
// If we only need a qualitative result, we can safely assume that the results will only be compared to |
||||
|
// bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. |
||||
|
storm::utility::setVectorValues<Type>(result, maybeStates, Type(0.5)); |
||||
|
} |
||||
|
|
||||
|
// Set values of resulting vector that are known exactly. |
||||
|
storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>()); |
||||
|
storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>()); |
||||
|
|
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is an instantaneous reward formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bound 0. |
||||
|
* @returns The reward values for the given formula for every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact values might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkInstantaneousReward(storm::formula::InstantaneousReward<Type> const& formula, bool qualitative) const { |
||||
|
// Only compute the result if the model has a state-based reward model. |
||||
|
if (!this->getModel().hasStateRewards()) { |
||||
|
LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); |
||||
|
throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; |
||||
|
} |
||||
|
|
||||
|
// Initialize result to state rewards of the model. |
||||
|
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
||||
|
|
||||
|
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. |
||||
|
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); |
||||
|
|
||||
|
// Return result. |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Check the given formula that is a cumulative reward formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bound 0. |
||||
|
* @returns The reward values for the given formula for every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact values might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkCumulativeReward(storm::formula::CumulativeReward<Type> const& formula, bool qualitative) const { |
||||
|
// Only compute the result if the model has at least one reward model. |
||||
|
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
||||
|
LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); |
||||
|
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
||||
|
} |
||||
|
|
||||
|
// Compute the reward vector to add in each step based on the available reward models. |
||||
|
std::vector<Type> totalRewardVector; |
||||
|
if (this->getModel().hasTransitionRewards()) { |
||||
|
totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); |
||||
|
if (this->getModel().hasStateRewards()) { |
||||
|
gmm::add(*this->getModel().getStateRewardVector(), totalRewardVector); |
||||
|
} |
||||
|
} else { |
||||
|
totalRewardVector = std::vector<Type>(*this->getModel().getStateRewardVector()); |
||||
|
} |
||||
|
|
||||
|
// Initialize result to either the state rewards of the model or the null vector. |
||||
|
std::vector<Type>* result = nullptr; |
||||
|
if (this->getModel().hasStateRewards()) { |
||||
|
result = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
||||
|
} else { |
||||
|
result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
||||
|
} |
||||
|
|
||||
|
// Perform the actual matrix-vector multiplication as long as the bound of the formula is met. |
||||
|
this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, &totalRewardVector, formula.getBound()); |
||||
|
|
||||
|
// Return result. |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
/*! |
||||
|
* Checks the given formula that is a reachability reward formula. |
||||
|
* |
||||
|
* @param formula The formula to check. |
||||
|
* @param qualitative A flag indicating whether the formula only needs to be evaluated qualitatively, i.e. if the |
||||
|
* results are only compared against the bound 0. If set to true, this will most likely results that are only |
||||
|
* qualitatively correct, i.e. do not represent the correct value, but only the correct relation with respect to the |
||||
|
* bound 0. |
||||
|
* @returns The reward values for the given formula for every state of the model associated with this model |
||||
|
* checker. If the qualitative flag is set, exact values might not be computed. |
||||
|
*/ |
||||
|
virtual std::vector<Type>* checkReachabilityReward(storm::formula::ReachabilityReward<Type> const& formula, bool qualitative) const { |
||||
|
// Only compute the result if the model has at least one reward model. |
||||
|
if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { |
||||
|
LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); |
||||
|
throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; |
||||
|
} |
||||
|
|
||||
|
// Determine the states for which the target predicate holds. |
||||
|
storm::storage::BitVector* targetStates = formula.getChild().check(*this); |
||||
|
|
||||
|
// Determine which states have a reward of infinity by definition. |
||||
|
storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); |
||||
|
storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); |
||||
|
storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); |
||||
|
infinityStates.complement(); |
||||
|
|
||||
|
// Create resulting vector. |
||||
|
std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates()); |
||||
|
|
||||
|
// Check whether there are states for which we have to compute the result. |
||||
|
storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; |
||||
|
const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); |
||||
|
if (maybeStatesSetBitCount > 0) { |
||||
|
// Now we can eliminate the rows and columns from the original transition probability matrix. |
||||
|
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); |
||||
|
// 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<Type> x(maybeStatesSetBitCount, storm::utility::constGetOne<Type>()); |
||||
|
|
||||
|
// Prepare the right-hand side of the equation system. |
||||
|
std::vector<Type> b(maybeStatesSetBitCount); |
||||
|
if (this->getModel().hasTransitionRewards()) { |
||||
|
// If a transition-based reward model is available, we initialize the right-hand |
||||
|
// side to the vector resulting from summing the rows of the pointwise product |
||||
|
// of the transition probability matrix and the transition reward matrix. |
||||
|
std::vector<Type> pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); |
||||
|
storm::utility::selectVectorValues(&b, maybeStates, pointwiseProductRowSumVector); |
||||
|
|
||||
|
if (this->getModel().hasStateRewards()) { |
||||
|
// If a state-based reward model is also available, we need to add this vector |
||||
|
// as well. As the state reward vector contains entries not just for the states |
||||
|
// that we still consider (i.e. maybeStates), we need to extract these values |
||||
|
// first. |
||||
|
std::vector<Type> subStateRewards(maybeStatesSetBitCount); |
||||
|
storm::utility::selectVectorValues(&subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); |
||||
|
gmm::add(subStateRewards, b); |
||||
|
} |
||||
|
} else { |
||||
|
// If only a state-based reward model is available, we take this vector as the |
||||
|
// right-hand side. As the state reward vector contains entries not just for the |
||||
|
// states that we still consider (i.e. maybeStates), we need to extract these values |
||||
|
// first. |
||||
|
storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector()); |
||||
|
} |
||||
|
|
||||
|
// Now solve the resulting equation system. |
||||
|
this->solveEquationSystem(submatrix, x, b); |
||||
|
|
||||
|
// Set values of resulting vector according to result. |
||||
|
storm::utility::setVectorValues<Type>(result, maybeStates, x); |
||||
|
} |
||||
|
|
||||
|
// Set values of resulting vector that are known exactly. |
||||
|
storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero<Type>()); |
||||
|
storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<Type>()); |
||||
|
|
||||
|
// Delete temporary storages and return result. |
||||
|
delete targetStates; |
||||
|
return result; |
||||
|
} |
||||
|
|
||||
|
private: |
||||
|
/*! |
||||
|
* Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes x[i+1] = A*x[i] + b |
||||
|
* until x[n], where x[0] = x. |
||||
|
* |
||||
|
* @param A The matrix that is to be multiplied against the vector. |
||||
|
* @param x The initial vector that is to be multiplied against the matrix. This is also the output parameter, |
||||
|
* i.e. after the method returns, this vector will contain the computed values. |
||||
|
* @param b If not null, this vector is being added to the result after each matrix-vector multiplication. |
||||
|
* @param n Specifies the number of iterations the matrix-vector multiplication is performed. |
||||
|
* @returns The result of the repeated matrix-vector multiplication as the content of the parameter vector. |
||||
|
*/ |
||||
|
virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type>* b = nullptr, uint_fast64_t n = 1) const = 0; |
||||
|
|
||||
|
/*! |
||||
|
* Solves the equation system A*x = b given by the parameters. |
||||
|
* |
||||
|
* @param A The matrix specifying the coefficients of the linear equations. |
||||
|
* @param x The solution vector x. The initial values of x represent a guess of the real values to the solver, but |
||||
|
* may be ignored. |
||||
|
* @param b The right-hand side of the equation system. |
||||
|
* @returns The solution vector x of the system of linear equations as the content of the parameter x. |
||||
|
*/ |
||||
|
virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const = 0; |
||||
|
}; |
||||
|
|
||||
|
} // namespace modelchecker |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ */ |
||||
744
src/storage/SparseMatrix.h
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -1,71 +0,0 @@ |
|||||
/*
|
|
||||
* IoUtility.cpp |
|
||||
* |
|
||||
* Created on: 17.10.2012 |
|
||||
* Author: Thomas Heinemann |
|
||||
*/ |
|
||||
|
|
||||
#include "src/utility/IoUtility.h"
|
|
||||
|
|
||||
#include <fstream>
|
|
||||
|
|
||||
#include "src/parser/DeterministicSparseTransitionParser.h"
|
|
||||
#include "src/parser/AtomicPropositionLabelingParser.h"
|
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
namespace utility { |
|
||||
|
|
||||
void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) { |
|
||||
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionMatrix()); |
|
||||
std::ofstream file; |
|
||||
file.open(filename); |
|
||||
|
|
||||
file << "digraph dtmc {\n"; |
|
||||
|
|
||||
//Specify the nodes and their labels
|
|
||||
for (uint_fast64_t i = 1; i < dtmc.getNumberOfStates(); i++) { |
|
||||
file << "\t" << i << "[label=\"" << i << "\\n{"; |
|
||||
char komma=' '; |
|
||||
std::set<std::string> propositions = dtmc.getPropositionsForState(i); |
|
||||
for(auto it = propositions.begin(); |
|
||||
it != propositions.end(); |
|
||||
it++) { |
|
||||
file << komma << *it; |
|
||||
komma=','; |
|
||||
} |
|
||||
|
|
||||
file << " }\"];\n"; |
|
||||
|
|
||||
} |
|
||||
|
|
||||
for (uint_fast64_t row = 0; row < dtmc.getNumberOfStates(); row++ ) { |
|
||||
|
|
||||
//Then, iterate through the row and write each non-diagonal value into the file
|
|
||||
for ( auto it = matrix->beginConstColumnIterator(row); |
|
||||
it != matrix->endConstColumnIterator(row); |
|
||||
it++) { |
|
||||
double value = 0; |
|
||||
matrix->getValue(row,*it,&value); |
|
||||
file << "\t" << row << " -> " << *it << " [label=" << value << "]\n"; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
file << "}\n"; |
|
||||
file.close(); |
|
||||
} |
|
||||
|
|
||||
//TODO: Should this stay here or be integrated in the new parser structure?
|
|
||||
/*storm::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file) {
|
|
||||
storm::parser::DeterministicSparseTransitionParser tp(tra_file); |
|
||||
uint_fast64_t node_count = tp.getMatrix()->getRowCount(); |
|
||||
|
|
||||
storm::parser::AtomicPropositionLabelingParser lp(node_count, lab_file); |
|
||||
|
|
||||
storm::models::Dtmc<double>* result = new storm::models::Dtmc<double>(tp.getMatrix(), lp.getLabeling()); |
|
||||
return result; |
|
||||
}*/ |
|
||||
|
|
||||
} |
|
||||
|
|
||||
} |
|
||||
@ -1,45 +0,0 @@ |
|||||
/* |
|
||||
* IoUtility.h |
|
||||
* |
|
||||
* Created on: 17.10.2012 |
|
||||
* Author: Thomas Heinemann |
|
||||
*/ |
|
||||
|
|
||||
#ifndef STORM_UTILITY_IOUTILITY_H_ |
|
||||
#define STORM_UTILITY_IOUTILITY_H_ |
|
||||
|
|
||||
#include "src/models/Dtmc.h" |
|
||||
|
|
||||
namespace storm { |
|
||||
|
|
||||
namespace utility { |
|
||||
|
|
||||
/*! |
|
||||
Creates a DOT file which provides the graph of the DTMC. |
|
||||
|
|
||||
Currently, only a version for DTMCs using probabilities of type double is provided. |
|
||||
Adaptions for other types may be included later. |
|
||||
|
|
||||
@param dtmc The DTMC to output |
|
||||
@param filename The Name of the file to write in. If the file already exists, |
|
||||
it will be overwritten. |
|
||||
|
|
||||
*/ |
|
||||
void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename); |
|
||||
|
|
||||
/*! |
|
||||
Parses a transition file and a labeling file and produces a DTMC out of them. |
|
||||
Note that the labeling file may have at most as many nodes as the transition file! |
|
||||
|
|
||||
@param tra_file String containing the location of the transition file (....tra) |
|
||||
@param lab_file String containing the location of the labeling file (....lab) |
|
||||
@returns The DTMC described by the two files. |
|
||||
|
|
||||
*/ |
|
||||
//storm::models::Dtmc<double>* parseDTMC(std::string const &tra_file, std::string const &lab_file); |
|
||||
|
|
||||
} //namespace utility |
|
||||
|
|
||||
} //namespace storm |
|
||||
|
|
||||
#endif /* STORM_UTILITY_IOUTILITY_H_ */ |
|
||||
@ -1,25 +0,0 @@ |
|||||
/*
|
|
||||
* ParseDtmcTest.cpp |
|
||||
* |
|
||||
* Created on: 03.12.2012 |
|
||||
* Author: Thomas Heinemann |
|
||||
*/ |
|
||||
|
|
||||
|
|
||||
#include "gtest/gtest.h"
|
|
||||
#include "storm-config.h"
|
|
||||
#include "src/parser/DeterministicModelParser.h"
|
|
||||
#include "src/utility/IoUtility.h"
|
|
||||
|
|
||||
TEST(ParseDtmcTest, parseAndOutput) { |
|
||||
storm::parser::DeterministicModelParser* dtmcParser = nullptr; |
|
||||
ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser( |
|
||||
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra", |
|
||||
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); |
|
||||
|
|
||||
ASSERT_NO_THROW(storm::utility::dtmcToDot(*(dtmcParser->getDtmc()), STORM_CPP_TESTS_BASE_PATH "/parser/output.dot")); |
|
||||
|
|
||||
delete dtmcParser; |
|
||||
} |
|
||||
|
|
||||
|
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue