dehnert
12 years ago
27 changed files with 871 additions and 968 deletions
-
58CMakeLists.txt
-
1src/formula/ReachabilityReward.h
-
13src/modelchecker/AbstractModelChecker.h
-
5src/modelchecker/DtmcPrctlModelChecker.h
-
21src/modelchecker/EigenDtmcPrctlModelChecker.h
-
49src/modelchecker/GmmxxDtmcPrctlModelChecker.h
-
54src/models/AbstractDeterministicModel.h
-
174src/models/AbstractModel.h
-
82src/models/AbstractNondeterministicModel.h
-
149src/models/Ctmc.h
-
175src/models/Ctmdp.h
-
173src/models/Dtmc.h
-
104src/models/GraphTransitions.h
-
171src/models/Mdp.h
-
79src/parser/AutoParser.cpp
-
76src/parser/AutoParser.h
-
8src/parser/NondeterministicModelParser.cpp
-
7src/parser/NondeterministicModelParser.h
-
10src/parser/NondeterministicSparseTransitionParser.cpp
-
4src/parser/NondeterministicSparseTransitionParser.h
-
155src/solver/GraphAnalyzer.h
-
6src/storage/SparseMatrix.h
-
3src/storm.cpp
-
242src/utility/GraphAnalyzer.h
-
2src/utility/IoUtility.cpp
-
8test/parser/ParseMdpTest.cpp
-
8test/storage/SparseMatrixTest.cpp
@ -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/WrongFileFormatException.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::WrongFileFormatException() << "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,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,242 @@ |
|||||
|
/* |
||||
|
* 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.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) && !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.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) && !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) { |
||||
|
|
||||
|
} |
||||
|
|
||||
|
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) { |
||||
|
|
||||
|
} |
||||
|
|
||||
|
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) { |
||||
|
// This result is a rough guess and does not compute all states with probability 1. |
||||
|
// TODO: Check whether it makes sense to implement the precise but complicated algorithm here. |
||||
|
*statesWithProbability1 = psiStates; |
||||
|
} |
||||
|
}; |
||||
|
|
||||
|
} // namespace utility |
||||
|
|
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue