Lanchid
13 years ago
60 changed files with 5676 additions and 1583 deletions
-
3109resources/cmake/cotire.cmake
-
2src/formula/AbstractFormula.h
-
4src/formula/AbstractPathFormula.h
-
2src/formula/AbstractStateFormula.h
-
2src/formula/And.h
-
2src/formula/Ap.h
-
8src/formula/BoundedEventually.h
-
9src/formula/BoundedNaryUntil.h
-
9src/formula/BoundedUntil.h
-
6src/formula/CumulativeReward.h
-
8src/formula/Eventually.h
-
10src/formula/Formulas.h
-
7src/formula/Globally.h
-
6src/formula/InstantaneousReward.h
-
6src/formula/Next.h
-
59src/formula/NoBoundOperator.h
-
2src/formula/Not.h
-
36src/formula/PathBoundOperator.h
-
11src/formula/PrctlFormulaChecker.h
-
27src/formula/ProbabilisticBoundOperator.h
-
14src/formula/ProbabilisticNoBoundOperator.h
-
7src/formula/ReachabilityReward.h
-
27src/formula/RewardBoundOperator.h
-
14src/formula/RewardNoBoundOperator.h
-
6src/formula/Until.h
-
139src/modelchecker/AbstractModelChecker.h
-
182src/modelchecker/DtmcPrctlModelChecker.h
-
21src/modelchecker/EigenDtmcPrctlModelChecker.h
-
3src/modelchecker/ForwardDeclarations.h
-
96src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
434src/modelchecker/GmmxxMdpPrctlModelChecker.h
-
286src/modelchecker/MdpPrctlModelChecker.h
-
54src/models/AbstractDeterministicModel.h
-
176src/models/AbstractModel.h
-
82src/models/AbstractNondeterministicModel.h
-
15src/models/AtomicPropositionsLabeling.h
-
149src/models/Ctmc.h
-
175src/models/Ctmdp.h
-
173src/models/Dtmc.h
-
104src/models/GraphTransitions.h
-
175src/models/Mdp.h
-
79src/parser/AutoParser.cpp
-
76src/parser/AutoParser.h
-
10src/parser/NondeterministicModelParser.cpp
-
7src/parser/NondeterministicModelParser.h
-
146src/parser/NondeterministicSparseTransitionParser.cpp
-
4src/parser/NondeterministicSparseTransitionParser.h
-
79src/reward/RewardModel.h
-
155src/solver/GraphAnalyzer.h
-
39src/storage/BitVector.h
-
220src/storage/SparseMatrix.h
-
71src/storm.cpp
-
8src/utility/ConstTemplates.h
-
421src/utility/GraphAnalyzer.h
-
2src/utility/IoUtility.cpp
-
63src/utility/Vector.h
-
183src/vector/dense_vector.h
-
8test/parser/ParseMdpTest.cpp
-
23test/reward/RewardModelTest.cpp
-
8test/storage/SparseMatrixTest.cpp
3109
resources/cmake/cotire.cmake
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
@ -0,0 +1,434 @@ |
|||
/* |
|||
* GmmxxDtmcPrctlModelChecker.h |
|||
* |
|||
* Created on: 06.12.2012 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ |
|||
|
|||
#include <cmath> |
|||
|
|||
#include "src/models/Mdp.h" |
|||
#include "src/modelchecker/MdpPrctlModelChecker.h" |
|||
#include "src/utility/GraphAnalyzer.h" |
|||
#include "src/utility/Vector.h" |
|||
#include "src/utility/ConstTemplates.h" |
|||
#include "src/utility/Settings.h" |
|||
#include "src/adapters/GmmxxAdapter.h" |
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/storage/JacobiDecomposition.h" |
|||
|
|||
#include "gmm/gmm_matrix.h" |
|||
#include "gmm/gmm_iter_solvers.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace modelChecker { |
|||
|
|||
/* |
|||
* A model checking engine that makes use of the gmm++ backend. |
|||
*/ |
|||
template <class Type> |
|||
class GmmxxMdpPrctlModelChecker : public MdpPrctlModelChecker<Type> { |
|||
|
|||
public: |
|||
explicit GmmxxMdpPrctlModelChecker(storm::models::Mdp<Type>& mdp) : MdpPrctlModelChecker<Type>(mdp) { } |
|||
|
|||
virtual ~GmmxxMdpPrctlModelChecker() { } |
|||
|
|||
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()); |
|||
|
|||
// Get the starting row indices for the non-deterministic choices to reduce the resulting |
|||
// vector properly. |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); |
|||
|
|||
// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. |
|||
tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *nondeterministicChoiceIndices); |
|||
|
|||
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(tmpMatrix); |
|||
|
|||
// 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>()); |
|||
|
|||
// Create vector for result of multiplication, which is reduced to the result vector after |
|||
// each multiplication. |
|||
std::vector<Type>* multiplyResult = new std::vector<Type>(this->getModel().getTransitionMatrix()->getRowCount(), 0); |
|||
|
|||
// Now perform matrix-vector multiplication as long as we meet the bound of the formula. |
|||
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { |
|||
gmm::mult(*gmmxxMatrix, *result, *multiplyResult); |
|||
if (this->minimumOperatorStack.top()) { |
|||
storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); |
|||
} else { |
|||
storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices); |
|||
} |
|||
} |
|||
delete multiplyResult; |
|||
|
|||
// Delete intermediate results and return result. |
|||
delete gmmxxMatrix; |
|||
delete leftStates; |
|||
delete rightStates; |
|||
return result; |
|||
} |
|||
|
|||
virtual std::vector<Type>* checkNext(const storm::formula::Next<Type>& formula, bool qualitative) const { |
|||
// First, we need to compute the states that satisfy the sub-formula of the next-formula. |
|||
storm::storage::BitVector* nextStates = formula.getChild().check(*this); |
|||
|
|||
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix()); |
|||
|
|||
// 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 sub-result. |
|||
delete nextStates; |
|||
|
|||
// Create resulting vector. |
|||
std::vector<Type>* temporaryResult = new std::vector<Type>(this->getModel().getTransitionMatrix()->getRowCount()); |
|||
|
|||
// Perform the actual computation, namely matrix-vector multiplication. |
|||
gmm::mult(*gmmxxMatrix, *result, *temporaryResult); |
|||
|
|||
// Get the starting row indices for the non-deterministic choices to reduce the resulting |
|||
// vector properly. |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); |
|||
|
|||
if (this->minimumOperatorStack.top()) { |
|||
storm::utility::reduceVectorMin(*temporaryResult, result, *nondeterministicChoiceIndices); |
|||
} else { |
|||
storm::utility::reduceVectorMax(*temporaryResult, result, *nondeterministicChoiceIndices); |
|||
} |
|||
|
|||
// Delete temporary matrix plus temporary result and return result. |
|||
delete gmmxxMatrix; |
|||
delete temporaryResult; |
|||
return result; |
|||
} |
|||
|
|||
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()); |
|||
if (this->minimumOperatorStack.top()) { |
|||
storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); |
|||
} else { |
|||
storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); |
|||
} |
|||
|
|||
// Delete sub-results that are obsolete now. |
|||
delete leftStates; |
|||
delete rightStates; |
|||
|
|||
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) { |
|||
// First, we can eliminate the rows and columns from the original transition probability matrix for states |
|||
// whose probabilities are already known. |
|||
storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); |
|||
|
|||
// Get the "new" nondeterministic choice indices for the submatrix. |
|||
std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); |
|||
|
|||
// Transform the submatrix to the gmm++ format to use its capabilities. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix); |
|||
|
|||
// Create vector for results for maybe states. |
|||
std::vector<Type>* x = new std::vector<Type>(maybeStatesSetBitCount); |
|||
|
|||
// 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(submatrix->getRowCount()); |
|||
this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b); |
|||
delete submatrix; |
|||
|
|||
// Solve the corresponding system of equations. |
|||
this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices); |
|||
|
|||
// Set values of resulting vector according to result. |
|||
storm::utility::setVectorValues<Type>(result, maybeStates, *x); |
|||
|
|||
// Delete temporary matrix and vector. |
|||
delete gmmxxMatrix; |
|||
delete x; |
|||
} |
|||
|
|||
// 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; |
|||
} |
|||
|
|||
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."; |
|||
} |
|||
|
|||
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix()); |
|||
|
|||
// Initialize result to state rewards of the model. |
|||
std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector()); |
|||
|
|||
// Now perform matrix-vector multiplication as long as we meet the bound of the formula. |
|||
std::vector<Type>* swap = nullptr; |
|||
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|||
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { |
|||
gmm::mult(*gmmxxMatrix, *result, *tmpResult); |
|||
swap = tmpResult; |
|||
tmpResult = result; |
|||
result = swap; |
|||
} |
|||
|
|||
// Delete temporary variables and return result. |
|||
delete tmpResult; |
|||
delete gmmxxMatrix; |
|||
return result; |
|||
} |
|||
|
|||
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."; |
|||
} |
|||
|
|||
// Transform the transition probability matrix to the gmm++ format to use its arithmetic. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix()); |
|||
|
|||
// 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().getNumberOfStates()); |
|||
|
|||
// Now perform matrix-vector multiplication as long as we meet the bound of the formula. |
|||
std::vector<Type>* swap = nullptr; |
|||
std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates()); |
|||
for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { |
|||
gmm::mult(*gmmxxMatrix, *result, *tmpResult); |
|||
swap = tmpResult; |
|||
tmpResult = result; |
|||
result = swap; |
|||
|
|||
// Add the reward vector to the result. |
|||
gmm::add(*totalRewardVector, *result); |
|||
} |
|||
|
|||
// Delete temporary variables and return result. |
|||
delete tmpResult; |
|||
delete gmmxxMatrix; |
|||
delete totalRewardVector; |
|||
return result; |
|||
} |
|||
|
|||
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); |
|||
// TODO: just commented out to make it compile |
|||
//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(); |
|||
|
|||
// Transform the submatrix to the gmm++ format to use its solvers. |
|||
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*submatrix); |
|||
delete submatrix; |
|||
|
|||
// 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 = new std::vector<Type>(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 = new std::vector<Type>(maybeStatesSetBitCount); |
|||
storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); |
|||
gmm::add(*subStateRewards, *b); |
|||
delete subStateRewards; |
|||
} |
|||
} 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::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); |
|||
} |
|||
|
|||
// Solve the corresponding system of linear equations. |
|||
// TODO: just commented out to make it compile |
|||
// this->solveEquationSystem(*gmmxxMatrix, 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 gmmxxMatrix; |
|||
delete b; |
|||
} |
|||
|
|||
// 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: |
|||
/*! |
|||
* Solves the given equation system under the given parameters using the power method. |
|||
* |
|||
* @param A The matrix A specifying the coefficients of the equations. |
|||
* @param x The vector x for which to solve the equations. The initial value of the elements of |
|||
* this vector are used as the initial guess and might thus influence performance and convergence. |
|||
* @param b The vector b specifying the values on the right-hand-sides of the equations. |
|||
* @return The solution of the system of linear equations in form of the elements of the vector |
|||
* x. |
|||
*/ |
|||
void solveEquationSystem(gmm::csr_matrix<Type> const& A, std::vector<Type>* x, std::vector<Type> const& b, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const { |
|||
// Get the settings object to customize solving. |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
|
|||
// Get relevant user-defined settings for solving the equations. |
|||
double precision = s->get<double>("precision"); |
|||
unsigned maxIterations = s->get<unsigned>("maxiter"); |
|||
bool relative = s->get<bool>("relative"); |
|||
|
|||
// Set up the environment for the power method. |
|||
std::vector<Type>* temporaryResult = new std::vector<Type>(b.size()); |
|||
std::vector<Type>* newX = new std::vector<Type>(x->size()); |
|||
std::vector<Type>* swap = nullptr; |
|||
bool converged = false; |
|||
uint_fast64_t iterations = 0; |
|||
|
|||
// Proceed with the iterations as long as the method did not converge or reach the |
|||
// user-specified maximum number of iterations. |
|||
while (!converged && iterations < maxIterations) { |
|||
// Compute x' = A*x + b. |
|||
gmm::mult(A, *x, *temporaryResult); |
|||
gmm::add(b, *temporaryResult); |
|||
|
|||
// Reduce the vector x' by applying min/max for all non-deterministic choices. |
|||
if (this->minimumOperatorStack.top()) { |
|||
storm::utility::reduceVectorMin(*temporaryResult, newX, nondeterministicChoiceIndices); |
|||
} else { |
|||
storm::utility::reduceVectorMax(*temporaryResult, newX, nondeterministicChoiceIndices); |
|||
} |
|||
|
|||
// Determine whether the method converged. |
|||
converged = storm::utility::equalModuloPrecision(*x, *newX, precision, relative); |
|||
|
|||
// Update environment variables. |
|||
swap = x; |
|||
x = newX; |
|||
newX = swap; |
|||
++iterations; |
|||
} |
|||
|
|||
delete temporaryResult; |
|||
|
|||
// Check if the solver converged and issue a warning otherwise. |
|||
if (converged) { |
|||
LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); |
|||
} else { |
|||
LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); |
|||
} |
|||
} |
|||
|
|||
std::shared_ptr<std::vector<uint_fast64_t>> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const { |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); |
|||
std::shared_ptr<std::vector<uint_fast64_t>> subNondeterministicChoiceIndices(new std::vector<uint_fast64_t>(constraint.getNumberOfSetBits() + 1)); |
|||
uint_fast64_t currentRowCount = 0; |
|||
uint_fast64_t currentIndexCount = 1; |
|||
(*subNondeterministicChoiceIndices)[0] = 0; |
|||
for (auto index : constraint) { |
|||
(*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; |
|||
currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; |
|||
++currentIndexCount; |
|||
} |
|||
(*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount; |
|||
|
|||
return subNondeterministicChoiceIndices; |
|||
} |
|||
}; |
|||
|
|||
} //namespace modelChecker |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ */ |
|||
@ -0,0 +1,286 @@ |
|||
/* |
|||
* MdpPrctlModelChecker.h |
|||
* |
|||
* Created on: 15.02.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELCHECKER_MDPPRCTLMODELCHECKER_H_ |
|||
#define STORM_MODELCHECKER_MDPPRCTLMODELCHECKER_H_ |
|||
|
|||
#include "src/formula/Formulas.h" |
|||
#include "src/utility/Vector.h" |
|||
#include "src/storage/SparseMatrix.h" |
|||
|
|||
#include "src/models/Mdp.h" |
|||
#include "src/storage/BitVector.h" |
|||
#include "src/exceptions/InvalidPropertyException.h" |
|||
#include "src/utility/Vector.h" |
|||
#include "src/modelchecker/AbstractModelChecker.h" |
|||
#include <vector> |
|||
#include <stack> |
|||
|
|||
#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 MdpPrctlModelChecker : |
|||
public AbstractModelChecker<Type> { |
|||
|
|||
public: |
|||
/*! |
|||
* Constructor |
|||
* |
|||
* @param model The dtmc model which is checked. |
|||
*/ |
|||
explicit MdpPrctlModelChecker(storm::models::Mdp<Type>& model) |
|||
: AbstractModelChecker<Type>(model), minimumOperatorStack() { |
|||
} |
|||
|
|||
/*! |
|||
* Copy constructor |
|||
* |
|||
* @param modelChecker The model checker that is copied. |
|||
*/ |
|||
explicit MdpPrctlModelChecker(const storm::modelChecker::MdpPrctlModelChecker<Type>* modelChecker) |
|||
: AbstractModelChecker<Type>(modelChecker), minimumOperatorStack() { |
|||
|
|||
} |
|||
|
|||
/*! |
|||
* Destructor |
|||
*/ |
|||
virtual ~MdpPrctlModelChecker() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* @returns A reference to the dtmc of the model checker. |
|||
*/ |
|||
storm::models::Mdp<Type>& getModel() const { |
|||
return AbstractModelChecker<Type>::template getModel<storm::models::Mdp<Type>>(); |
|||
} |
|||
|
|||
/*! |
|||
* Sets the DTMC model which is checked |
|||
* @param model |
|||
*/ |
|||
void setModel(storm::models::Mdp<Type>& model) { |
|||
AbstractModelChecker<Type>::setModel(model); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given state formula on the DTMC and prints the result (true/false) for all initial |
|||
* states. |
|||
* @param stateFormula The formula to be checked. |
|||
*/ |
|||
void check(const storm::formula::AbstractStateFormula<Type>& stateFormula) const { |
|||
std::cout << std::endl; |
|||
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); |
|||
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; |
|||
storm::storage::BitVector* result = nullptr; |
|||
try { |
|||
result = stateFormula.check(*this); |
|||
LOG4CPLUS_INFO(logger, "Result for initial states:"); |
|||
std::cout << "Result for initial states:" << std::endl; |
|||
for (auto initialState : *this->getModel().getLabeledStates("init")) { |
|||
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); |
|||
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; |
|||
} |
|||
delete result; |
|||
} catch (std::exception& e) { |
|||
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; |
|||
if (result != nullptr) { |
|||
delete result; |
|||
} |
|||
} |
|||
std::cout << std::endl; |
|||
storm::utility::printSeparationLine(std::cout); |
|||
} |
|||
|
|||
/*! |
|||
* Checks the given operator (with no bound) on the DTMC and prints the result |
|||
* (probability/rewards) for all initial states. |
|||
* @param noBoundFormula The formula to be checked. |
|||
*/ |
|||
void check(const storm::formula::NoBoundOperator<Type>& noBoundFormula) const { |
|||
std::cout << std::endl; |
|||
LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); |
|||
std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; |
|||
std::vector<Type>* result = nullptr; |
|||
try { |
|||
result = noBoundFormula.check(*this); |
|||
LOG4CPLUS_INFO(logger, "Result for initial states:"); |
|||
std::cout << "Result for initial states:" << std::endl; |
|||
for (auto initialState : *this->getModel().getLabeledStates("init")) { |
|||
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); |
|||
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; |
|||
} |
|||
delete result; |
|||
} catch (std::exception& e) { |
|||
std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; |
|||
if (result != nullptr) { |
|||
delete result; |
|||
} |
|||
} |
|||
std::cout << std::endl; |
|||
storm::utility::printSeparationLine(std::cout); |
|||
} |
|||
|
|||
/*! |
|||
* The check method for a formula with an AP node as root in its formula tree |
|||
* |
|||
* @param formula The Ap state formula to check |
|||
* @returns The set of states satisfying the formula, represented by a bit vector |
|||
*/ |
|||
storm::storage::BitVector* checkAp(const storm::formula::Ap<Type>& formula) const { |
|||
if (formula.getAp().compare("true") == 0) { |
|||
return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); |
|||
} else if (formula.getAp().compare("false") == 0) { |
|||
return new storm::storage::BitVector(this->getModel().getNumberOfStates()); |
|||
} |
|||
|
|||
if (!this->getModel().hasAtomicProposition(formula.getAp())) { |
|||
LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); |
|||
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; |
|||
return nullptr; |
|||
} |
|||
|
|||
return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); |
|||
} |
|||
|
|||
/*! |
|||
* 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 non-optimality operator and report an error in that case. |
|||
if (!formula.isOptimalityOperator()) { |
|||
LOG4CPLUS_ERROR(logger, "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Formula does not specify neither min nor max optimality, which is not meaningful over nondeterministic models."; |
|||
} |
|||
minimumOperatorStack.push(formula.isMinimumOperator()); |
|||
std::vector<Type>* result = formula.getPathFormula().check(*this, false); |
|||
minimumOperatorStack.pop(); |
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
/*! |
|||
* 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 = 0; |
|||
|
|||
protected: |
|||
mutable std::stack<bool> minimumOperatorStack; |
|||
}; |
|||
|
|||
} //namespace modelChecker |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */ |
|||
@ -0,0 +1,54 @@ |
|||
#ifndef STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ |
|||
|
|||
#include "AbstractModel.h" |
|||
#include "GraphTransitions.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace models { |
|||
|
|||
/*! |
|||
* @brief Base class for all deterministic model classes. |
|||
* |
|||
* This is base class defines a common interface for all deterministic models. |
|||
*/ |
|||
template<class T> |
|||
class AbstractDeterministicModel: public AbstractModel<T> { |
|||
|
|||
public: |
|||
/*! Constructs an abstract determinstic model from the given parameters. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param stateLabeling The labeling that assigns a set of atomic |
|||
* propositions to each state. |
|||
* @param stateRewardVector The reward values associated with the states. |
|||
* @param transitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
|||
std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix) |
|||
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { |
|||
} |
|||
|
|||
/*! |
|||
* Destructor. |
|||
*/ |
|||
virtual ~AbstractDeterministicModel() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Copy Constructor. |
|||
*/ |
|||
AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other) { |
|||
// Intentionally left empty. |
|||
} |
|||
}; |
|||
|
|||
} // namespace models |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ |
|||
@ -0,0 +1,82 @@ |
|||
#ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ |
|||
#define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ |
|||
|
|||
#include "AbstractModel.h" |
|||
#include "GraphTransitions.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace models { |
|||
|
|||
/*! |
|||
* @brief Base class for all non-deterministic model classes. |
|||
* |
|||
* This is base class defines a common interface for all non-deterministic models. |
|||
*/ |
|||
template<class T> |
|||
class AbstractNondeterministicModel: public AbstractModel<T> { |
|||
|
|||
public: |
|||
/*! Constructs an abstract non-determinstic model from the given parameters. |
|||
* @param transitionMatrix The matrix representing the transitions in the model. |
|||
* @param stateLabeling The labeling that assigns a set of atomic |
|||
* propositions to each state. |
|||
* @param choiceIndices A mapping from states to rows in the transition matrix. |
|||
* @param stateRewardVector The reward values associated with the states. |
|||
* @param transitionRewardMatrix The reward values associated with the transitions of the model. |
|||
*/ |
|||
AbstractNondeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices, |
|||
std::shared_ptr<std::vector<T>> stateRewardVector, |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix) |
|||
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), |
|||
nondeterministicChoiceIndices(nondeterministicChoiceIndices) { |
|||
} |
|||
|
|||
/*! |
|||
* Destructor. |
|||
*/ |
|||
virtual ~AbstractNondeterministicModel() { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Copy Constructor. |
|||
*/ |
|||
AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other), |
|||
nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the size of the internal representation of the model in memory. |
|||
* @return the size of the internal representation of the model in memory |
|||
* measured in bytes. |
|||
*/ |
|||
virtual uint_fast64_t getSizeInMemory() const { |
|||
return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t); |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the vector indicating which matrix rows represent non-deterministic choices |
|||
* of a certain state. |
|||
* @param the vector indicating which matrix rows represent non-deterministic choices |
|||
* of a certain state. |
|||
*/ |
|||
std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const { |
|||
return nondeterministicChoiceIndices; |
|||
} |
|||
|
|||
private: |
|||
/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */ |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices; |
|||
}; |
|||
|
|||
} // namespace models |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */ |
|||
@ -1,79 +0,0 @@ |
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
#include <string>
|
|||
#include <cctype>
|
|||
|
|||
#include "src/exceptions/WrongFormatException.h"
|
|||
#include "src/models/AbstractModel.h"
|
|||
#include "src/parser/DeterministicModelParser.h"
|
|||
#include "src/parser/NonDeterministicModelParser.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile, std::string const & transitionRewardFile) |
|||
: model(nullptr) { |
|||
storm::models::ModelType type = this->analyzeHint(transitionSystemFile); |
|||
|
|||
if (type == storm::models::Unknown) { |
|||
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << "."); |
|||
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again."); |
|||
throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do actual parsing
|
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getDtmc(); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getCtmc(); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getMdp(); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); |
|||
this->model = parser.getCtmdp(); |
|||
break; |
|||
} |
|||
default: ; // Unknown
|
|||
} |
|||
|
|||
|
|||
if (!this->model) { |
|||
LOG4CPLUS_WARN(logger, "Model is still null."); |
|||
} |
|||
} |
|||
|
|||
storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
// Open file
|
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.data; |
|||
|
|||
// parse hint
|
|||
char hint[128]; |
|||
sscanf(buf, "%s\n", hint); |
|||
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); |
|||
|
|||
// check hint
|
|||
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; |
|||
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; |
|||
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; |
|||
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; |
|||
|
|||
return hintType; |
|||
} |
|||
|
|||
} // namespace parser
|
|||
} // namespace storm
|
|||
@ -1,79 +0,0 @@ |
|||
/* |
|||
* RewardModel.h |
|||
* |
|||
* Created on: 25.10.2012 |
|||
* Author: Philipp Berger |
|||
*/ |
|||
|
|||
#ifndef STORM_REWARD_REWARDMODEL_H_ |
|||
#define STORM_REWARD_REWARDMODEL_H_ |
|||
|
|||
#include <stdexcept> |
|||
|
|||
#include "boost/integer/integer_mask.hpp" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace reward { |
|||
|
|||
/*! This class represents a single reward model with a type DataClass value for each state contained in a Vector of type VectorImpl |
|||
*/ |
|||
template<template<class, class> class VectorImpl, class DataClass> |
|||
class RewardModel { |
|||
|
|||
//! Shorthand for a constant reference to the DataClass type |
|||
typedef const DataClass& crDataClass; |
|||
|
|||
public: |
|||
RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : state_count(state_count), null_value(null_value) { |
|||
|
|||
this->reward_vector = new VectorImpl<DataClass, std::allocator<DataClass>>(this->state_count); |
|||
// init everything to zero |
|||
for (uint_fast32_t i = 0; i < this->state_count; ++i) { |
|||
this->setReward(i, this->null_value); |
|||
} |
|||
} |
|||
|
|||
virtual ~RewardModel() { |
|||
delete reward_vector; |
|||
} |
|||
|
|||
bool setReward(const uint_fast32_t state_index, crDataClass reward) { |
|||
if (state_index < this->state_count) { |
|||
this->reward_vector->at(state_index) = reward; |
|||
// [state_index] = reward; |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
crDataClass getReward(const uint_fast32_t state_index) { |
|||
if (state_index < this->state_count) { |
|||
return this->reward_vector->at(state_index); |
|||
} |
|||
return this->null_value; |
|||
} |
|||
|
|||
bool resetReward(const uint_fast32_t state_index) { |
|||
if (state_index < this->state_count) { |
|||
this->reward_vector[state_index] = this->null_value; |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
uint_fast32_t getSize() const { |
|||
return this->state_count; |
|||
} |
|||
private: |
|||
uint_fast32_t state_count; |
|||
VectorImpl<DataClass, std::allocator<DataClass>>* reward_vector; |
|||
const DataClass& null_value; |
|||
|
|||
}; |
|||
|
|||
} //namespace reward |
|||
|
|||
} //namespace storm |
|||
|
|||
#endif /* STORM_REWARD_REWARDMODEL_H_ */ |
|||
@ -1,155 +0,0 @@ |
|||
/* |
|||
* GraphAnalyzer.h |
|||
* |
|||
* Created on: 28.11.2012 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_SOLVER_GRAPHANALYZER_H_ |
|||
#define STORM_SOLVER_GRAPHANALYZER_H_ |
|||
|
|||
#include "src/models/Dtmc.h" |
|||
#include "src/exceptions/InvalidArgumentException.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace solver { |
|||
|
|||
class GraphAnalyzer { |
|||
public: |
|||
/*! |
|||
* Performs a backwards depth-first search trough the underlying graph structure |
|||
* of the given model to determine which states of the model can reach one |
|||
* of the given target states whilst always staying in the set of filter states |
|||
* before. The resulting states are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess |
|||
* a paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void getExistsPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) { |
|||
// Check for valid parameter. |
|||
if (existsPhiUntilPsiStates == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); |
|||
} |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions(); |
|||
|
|||
// Add all psi states as the already satisfy the condition. |
|||
*existsPhiUntilPsiStates |= psiStates; |
|||
|
|||
// Initialize the stack used for the DFS with the states |
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
psiStates.getList(stack); |
|||
|
|||
// Perform the actual DFS. |
|||
while(!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) { |
|||
existsPhiUntilPsiStates->set(*it, true); |
|||
stack.push_back(*it); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Computes the set of states of the given model for which all paths lead to |
|||
* the given set of target states and only visit states from the filter set |
|||
* before. In order to do this, it uses the given set of states that |
|||
* characterizes the states that possess at least one path to a target state. |
|||
* The results are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path |
|||
* satisfying phi until psi. |
|||
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only |
|||
* have paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { |
|||
// Check for valid parameter. |
|||
if (alwaysPhiUntilPsiStates == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
} |
|||
|
|||
GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); |
|||
alwaysPhiUntilPsiStates->complement(); |
|||
} |
|||
|
|||
/*! |
|||
* Computes the set of states of the given model for which all paths lead to |
|||
* the given set of target states and only visit states from the filter set |
|||
* before. The results are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only |
|||
* have paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { |
|||
// Check for valid parameter. |
|||
if (alwaysPhiUntilPsiStates == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
} |
|||
|
|||
storm::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates()); |
|||
GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, &existsPhiUntilPsiStates); |
|||
GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); |
|||
alwaysPhiUntilPsiStates->complement(); |
|||
} |
|||
|
|||
|
|||
/*! |
|||
* Computes the set of states of the given model for which all paths lead to |
|||
* the given set of target states and only visit states from the filter set |
|||
* before. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess |
|||
* a path satisfying phi until psi. |
|||
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only |
|||
* have paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void getPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) { |
|||
// Check for valid parameters. |
|||
if (existsPhiUntilPsiStates == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null."); |
|||
} |
|||
if (alwaysPhiUntilPsiStates == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null."); |
|||
} |
|||
|
|||
// Perform search. |
|||
GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates); |
|||
GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates); |
|||
} |
|||
|
|||
}; |
|||
|
|||
} // namespace solver |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_SOLVER_GRAPHANALYZER_H_ */ |
|||
@ -0,0 +1,421 @@ |
|||
/* |
|||
* GraphAnalyzer.h |
|||
* |
|||
* Created on: 28.11.2012 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_UTILITY_GRAPHANALYZER_H_ |
|||
#define STORM_UTILITY_GRAPHANALYZER_H_ |
|||
|
|||
#include "src/models/AbstractDeterministicModel.h" |
|||
#include "src/models/AbstractNondeterministicModel.h" |
|||
#include "src/exceptions/InvalidArgumentException.h" |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace utility { |
|||
|
|||
class GraphAnalyzer { |
|||
public: |
|||
/*! |
|||
* Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a |
|||
* deterministic model. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates The set of all states satisfying phi. |
|||
* @param psiStates The set of all states satisfying psi. |
|||
* @param statesWithProbability0 A pointer to a bit vector that is initially empty and will contain all states with |
|||
* probability 0 after the invocation of the function. |
|||
* @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with |
|||
* probability 1 after the invocation of the function. |
|||
*/ |
|||
template <class T> |
|||
static void performProb01(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameters. |
|||
if (statesWithProbability0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); |
|||
} |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
// Perform the actual search. |
|||
GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbability0); |
|||
GraphAnalyzer::performProb1(model, phiStates, psiStates, *statesWithProbability0, statesWithProbability1); |
|||
statesWithProbability0->complement(); |
|||
} |
|||
|
|||
/*! |
|||
* Performs a backwards depth-first search trough the underlying graph structure |
|||
* of the given model to determine which states of the model have a positive probability |
|||
* of satisfying phi until psi. The resulting states are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess |
|||
* a positive probability of satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { |
|||
// Check for valid parameter. |
|||
if (statesWithProbabilityGreater0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbabilityGreater0' must not be null."); |
|||
} |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), false); |
|||
|
|||
// Add all psi states as the already satisfy the condition. |
|||
*statesWithProbabilityGreater0 |= psiStates; |
|||
|
|||
// Initialize the stack used for the DFS with the states |
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
psiStates.addSetIndicesToList(stack); |
|||
|
|||
// Perform the actual DFS. |
|||
while(!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !statesWithProbabilityGreater0->get(*it)) { |
|||
statesWithProbabilityGreater0->set(*it, true); |
|||
stack.push_back(*it); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Computes the set of states of the given model for which all paths lead to |
|||
* the given set of target states and only visit states from the filter set |
|||
* before. In order to do this, it uses the given set of states that |
|||
* characterizes the states that possess at least one path to a target state. |
|||
* The results are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive |
|||
* probability mass of satisfying phi until psi. |
|||
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only |
|||
* have paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameter. |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0, statesWithProbability1); |
|||
statesWithProbability1->complement(); |
|||
} |
|||
|
|||
/*! |
|||
* Computes the set of states of the given model for which all paths lead to |
|||
* the given set of target states and only visit states from the filter set |
|||
* before. In order to do this, it uses the given set of states that |
|||
* characterizes the states that possess at least one path to a target state. |
|||
* The results are written to the given bit vector. |
|||
* @param model The model whose graph structure to search. |
|||
* @param phiStates A bit vector of all states satisfying phi. |
|||
* @param psiStates A bit vector of all states satisfying psi. |
|||
* @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only |
|||
* have paths satisfying phi until psi. |
|||
*/ |
|||
template <class T> |
|||
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameter. |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
storm::storage::BitVector* statesWithProbabilityGreater0 = new storm::storage::BitVector(model.getNumberOfStates()); |
|||
GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0); |
|||
GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(*statesWithProbabilityGreater0), statesWithProbability1); |
|||
delete statesWithProbabilityGreater0; |
|||
statesWithProbability1->complement(); |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameters. |
|||
if (statesWithProbability0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); |
|||
} |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
// Perform the actual search. |
|||
GraphAnalyzer::performProb0A(model, phiStates, psiStates, statesWithProbability0); |
|||
GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1); |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { |
|||
// Check for valid parameter. |
|||
if (statesWithProbability0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); |
|||
} |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false); |
|||
|
|||
// Add all psi states as the already satisfy the condition. |
|||
*statesWithProbability0 |= psiStates; |
|||
|
|||
// Initialize the stack used for the DFS with the states |
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
psiStates.addSetIndicesToList(stack); |
|||
|
|||
// Perform the actual DFS. |
|||
while(!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !statesWithProbability0->get(*it)) { |
|||
statesWithProbability0->set(*it, true); |
|||
stack.push_back(*it); |
|||
} |
|||
} |
|||
} |
|||
|
|||
statesWithProbability0->complement(); |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameters. |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
// Get some temporaries for convenience. |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix(); |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false); |
|||
|
|||
storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true); |
|||
|
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
|
|||
bool done = false; |
|||
while (!done) { |
|||
stack.clear(); |
|||
storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates); |
|||
psiStates.addSetIndicesToList(stack); |
|||
|
|||
while (!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !nextStates->get(*it)) { |
|||
// Check whether the predecessor has only successors in the current state set for one of the |
|||
// nondeterminstic choices. |
|||
for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { |
|||
bool allSuccessorsInCurrentStates = true; |
|||
for (auto colIt = transitionMatrix->beginConstColumnIterator(row); colIt != transitionMatrix->endConstColumnIterator(row); ++colIt) { |
|||
if (!currentStates->get(*colIt)) { |
|||
allSuccessorsInCurrentStates = false; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// If all successors for a given nondeterministic choice are in the current state set, we |
|||
// add it to the set of states for the next iteration and perform a backward search from |
|||
// that state. |
|||
if (allSuccessorsInCurrentStates) { |
|||
nextStates->set(*it, true); |
|||
stack.push_back(*it); |
|||
break; |
|||
} |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Check whether we need to perform an additional iteration. |
|||
if (*currentStates == *nextStates) { |
|||
done = true; |
|||
} else { |
|||
*currentStates = *nextStates; |
|||
} |
|||
} |
|||
|
|||
*statesWithProbability1 = *currentStates; |
|||
delete currentStates; |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameters. |
|||
if (statesWithProbability0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); |
|||
} |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
// Perform the actual search. |
|||
GraphAnalyzer::performProb0E(model, phiStates, psiStates, statesWithProbability0); |
|||
GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1); |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { |
|||
// Check for valid parameter. |
|||
if (statesWithProbability0 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null."); |
|||
} |
|||
|
|||
// Get some temporaries for convenience. |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix(); |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T> backwardTransitions(transitionMatrix, nondeterministicChoiceIndices, false); |
|||
|
|||
// Add all psi states as the already satisfy the condition. |
|||
*statesWithProbability0 |= psiStates; |
|||
|
|||
// Initialize the stack used for the DFS with the states |
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
psiStates.addSetIndicesToList(stack); |
|||
|
|||
// Perform the actual DFS. |
|||
while(!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !statesWithProbability0->get(*it)) { |
|||
// Check whether the predecessor has at least one successor in the current state |
|||
// set for every nondeterministic choice. |
|||
bool addToStatesWithProbability0 = true; |
|||
for (auto rowIt = nondeterministicChoiceIndices->begin() + *it; rowIt != nondeterministicChoiceIndices->begin() + *it + 1; ++rowIt) { |
|||
bool hasAtLeastOneSuccessorWithProbabilityGreater0 = false; |
|||
for (auto colIt = transitionMatrix->beginConstColumnIterator(*rowIt); colIt != transitionMatrix->endConstColumnIterator(*rowIt); ++colIt) { |
|||
if (statesWithProbability0->get(*colIt)) { |
|||
hasAtLeastOneSuccessorWithProbabilityGreater0 = true; |
|||
break; |
|||
} |
|||
} |
|||
if (!hasAtLeastOneSuccessorWithProbabilityGreater0) { |
|||
addToStatesWithProbability0 = false; |
|||
break; |
|||
} |
|||
} |
|||
|
|||
// If we need to add the state, then actually add it and perform further search |
|||
// from the state. |
|||
if (addToStatesWithProbability0) { |
|||
statesWithProbability0->set(*it, true); |
|||
stack.push_back(*it); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
statesWithProbability0->complement(); |
|||
} |
|||
|
|||
template <class T> |
|||
static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { |
|||
// Check for valid parameters. |
|||
if (statesWithProbability1 == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null."); |
|||
throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null."); |
|||
} |
|||
|
|||
// Get some temporaries for convenience. |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix = model.getTransitionMatrix(); |
|||
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); |
|||
|
|||
// Get the backwards transition relation from the model to ease the search. |
|||
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false); |
|||
|
|||
storm::storage::BitVector* currentStates = new storm::storage::BitVector(model.getNumberOfStates(), true); |
|||
|
|||
std::vector<uint_fast64_t> stack; |
|||
stack.reserve(model.getNumberOfStates()); |
|||
|
|||
bool done = false; |
|||
while (!done) { |
|||
stack.clear(); |
|||
storm::storage::BitVector* nextStates = new storm::storage::BitVector(psiStates); |
|||
psiStates.addSetIndicesToList(stack); |
|||
|
|||
while (!stack.empty()) { |
|||
uint_fast64_t currentState = stack.back(); |
|||
stack.pop_back(); |
|||
|
|||
for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { |
|||
if (phiStates.get(*it) && !nextStates->get(*it)) { |
|||
// Check whether the predecessor has only successors in the current state set for all of the |
|||
// nondeterminstic choices. |
|||
bool allSuccessorsInCurrentStatesForAllChoices = true; |
|||
for (uint_fast64_t row = (*nondeterministicChoiceIndices)[*it]; row < (*nondeterministicChoiceIndices)[*it + 1]; ++row) { |
|||
for (auto colIt = transitionMatrix->beginConstColumnIterator(row); colIt != transitionMatrix->endConstColumnIterator(row); ++colIt) { |
|||
if (!currentStates->get(*colIt)) { |
|||
allSuccessorsInCurrentStatesForAllChoices = false; |
|||
goto afterCheckLoop; |
|||
} |
|||
} |
|||
} |
|||
|
|||
afterCheckLoop: |
|||
// If all successors for all nondeterministic choices are in the current state set, we |
|||
// add it to the set of states for the next iteration and perform a backward search from |
|||
// that state. |
|||
if (allSuccessorsInCurrentStatesForAllChoices) { |
|||
nextStates->set(*it, true); |
|||
stack.push_back(*it); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Check whether we need to perform an additional iteration. |
|||
if (*currentStates == *nextStates) { |
|||
done = true; |
|||
} else { |
|||
*currentStates = *nextStates; |
|||
} |
|||
} |
|||
|
|||
*statesWithProbability1 = *currentStates; |
|||
delete currentStates; |
|||
} |
|||
}; |
|||
|
|||
} // namespace utility |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */ |
|||
@ -1,183 +0,0 @@ |
|||
#ifndef MRMC_VECTOR_BITVECTOR_H_ |
|||
#define MRMC_VECTOR_BITVECTOR_H_ |
|||
|
|||
#include <exception> |
|||
#include <new> |
|||
#include <cmath> |
|||
#include "boost/integer/integer_mask.hpp" |
|||
|
|||
#include <pantheios/pantheios.hpp> |
|||
#include <pantheios/inserters/integer.hpp> |
|||
|
|||
#include "src/exceptions/invalid_state.h" |
|||
#include "src/exceptions/invalid_argument.h" |
|||
#include "src/exceptions/out_of_range.h" |
|||
|
|||
namespace mrmc { |
|||
|
|||
namespace vector { |
|||
|
|||
//! A Vector |
|||
/*! |
|||
A bit vector for boolean fields or quick selection schemas on Matrix entries. |
|||
Does NOT perform index bound checks! |
|||
*/ |
|||
template <class T> |
|||
class DenseVector { |
|||
public: |
|||
//! Constructor |
|||
/*! |
|||
\param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() |
|||
*/ |
|||
BitVector(uint_fast64_t initial_length) { |
|||
bucket_count = initial_length / 64; |
|||
if (initial_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
|
|||
// init all 0 |
|||
for (uint_fast64_t i = 0; i < bucket_count; ++i) { |
|||
bucket_array[i] = 0; |
|||
} |
|||
} |
|||
|
|||
//! Copy Constructor |
|||
/*! |
|||
Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. |
|||
@param bv A reference to the bit vector that should be copied from |
|||
*/ |
|||
BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) |
|||
{ |
|||
pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor."); |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count); |
|||
} |
|||
|
|||
~BitVector() { |
|||
if (bucket_array != NULL) { |
|||
delete[] bucket_array; |
|||
} |
|||
} |
|||
|
|||
void resize(uint_fast64_t new_length) { |
|||
uint_fast64_t* tempArray = new uint_fast64_t[new_length](); |
|||
|
|||
// 64 bit/entries per uint_fast64_t |
|||
uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count); |
|||
memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize); |
|||
|
|||
bucket_count = new_length / 64; |
|||
if (new_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
|
|||
delete[] bucket_array; |
|||
bucket_array = tempArray; |
|||
} |
|||
|
|||
void set(const uint_fast64_t index, const bool value) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
if (value) { |
|||
bucket_array[bucket] |= mask; |
|||
} else { |
|||
bucket_array[bucket] &= ~mask; |
|||
} |
|||
} |
|||
|
|||
bool get(const uint_fast64_t index) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
return ((bucket_array[bucket] & mask) == mask); |
|||
} |
|||
|
|||
// Operators |
|||
BitVector operator &(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
BitVector operator |(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ^(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ~() { |
|||
BitVector result(this->bucket_count * 64); |
|||
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) { |
|||
result.bucket_array[i] = ~this->bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the number of bits that are set (to one) in this bit vector. |
|||
* @return The number of bits that are set (to one) in this bit vector. |
|||
*/ |
|||
uint_fast64_t getNumberOfSetBits() { |
|||
uint_fast64_t set_bits = 0; |
|||
for (uint_fast64_t i = 0; i < bucket_count; i++) { |
|||
#ifdef __GNUG__ // check if we are using g++ and use built-in function if available |
|||
set_bits += __builtin_popcount (this->bucket_array[i]); |
|||
#else |
|||
uint_fast32_t cnt; |
|||
uint_fast64_t bitset = this->bucket_array[i]; |
|||
for (cnt = 0; bitset; cnt++) { |
|||
bitset &= bitset - 1; |
|||
} |
|||
set_bits += cnt; |
|||
#endif |
|||
} |
|||
return set_bits; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the size of the bit vector in memory measured in bytes. |
|||
* @return The size of the bit vector in memory measured in bytes. |
|||
*/ |
|||
uint_fast64_t getSizeInMemory() { |
|||
return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count; |
|||
} |
|||
|
|||
private: |
|||
uint_fast64_t bucket_count; |
|||
|
|||
/*! Array containing the boolean bits for each node, 64bits/64nodes per element */ |
|||
uint_fast64_t* bucket_array; |
|||
|
|||
}; |
|||
|
|||
} // namespace vector |
|||
|
|||
} // namespace mrmc |
|||
|
|||
#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ |
|||
@ -1,23 +0,0 @@ |
|||
#include "gtest/gtest.h"
|
|||
|
|||
#include "Eigen/Sparse"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "boost/integer/integer_mask.hpp"
|
|||
#include <vector>
|
|||
|
|||
#include "reward/RewardModel.h"
|
|||
|
|||
TEST(RewardModelTest, ReadWriteTest) { |
|||
// 50 entries
|
|||
storm::reward::RewardModel<std::vector, double> rm(50, 0.0); |
|||
|
|||
double values[50]; |
|||
for (int i = 0; i < 50; ++i) { |
|||
values[i] = 1.0 + i; |
|||
ASSERT_TRUE(rm.setReward(i, values[i])); |
|||
|
|||
ASSERT_EQ(rm.getReward(i), values[i]); |
|||
} |
|||
|
|||
} |
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue