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

Prepared methods for performing reachability searches for non-deterministic models. Removed storage of backward transition relation: it is now (re-)created on demand in the model checkers.

main
dehnert 13 years ago
parent
5d849018de
commit
19cbe13691
4 changed files with 70 additions and 44 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 39
      src/models/AbstractDeterministicModel.h
  2. 4
      src/models/GraphTransitions.h
  3. 4
      src/parser/NonDeterministicSparseTransitionParser.cpp
  4. 67
      src/utility/GraphAnalyzer.h

39
src/models/AbstractDeterministicModel.h
View File

@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
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), backwardTransitions(nullptr) {
: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
}
/*!
@ -42,42 +42,9 @@ class AbstractDeterministicModel: public AbstractModel<T> {
/*!
* Copy Constructor.
*/
AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other), backwardTransitions(nullptr) {
if (other.backwardTransitions != nullptr) {
backwardTransitions = new storm::models::GraphTransitions<T>(*other.backwardTransitions);
}
}
/*!
* 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 {
uint_fast64_t result = AbstractModel<T>::getSizeInMemory();
if (backwardTransitions != nullptr) {
result += backwardTransitions->getSizeInMemory();
}
return result;
}
/*!
* Retrieves a reference to the backwards transition relation.
* @return A reference to the backwards transition relation.
*/
storm::models::GraphTransitions<T>& getBackwardTransitions() {
if (this->backwardTransitions == nullptr) {
this->backwardTransitions = std::shared_ptr<storm::models::GraphTransitions<T>>(new storm::models::GraphTransitions<T>(this->getTransitionMatrix(), this->getNumberOfStates(), false));
}
return *this->backwardTransitions;
AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other) {
// Intentionally left empty.
}
private:
/*!
* A data structure that stores the predecessors for all states. This is
* needed for backwards directed searches.
*/
std::shared_ptr<storm::models::GraphTransitions<T>> backwardTransitions;
};
} // namespace models

4
src/models/GraphTransitions.h
View File

@ -39,8 +39,8 @@ public:
* @param forward If set to true, this objects will store the graph structure
* of the backwards transition relation.
*/
GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, uint_fast64_t numberOfStates, bool forward)
: successorList(nullptr), stateIndications(nullptr), numberOfStates(numberOfStates), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
if (forward) {
this->initializeForward(transitionMatrix);
} else {

4
src/parser/NonDeterministicSparseTransitionParser.cpp
View File

@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
/*
* Create row mapping.
*/
this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+1,0));
this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+2,0));
/*
* Parse file content.
@ -288,6 +288,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
curRow++;
}
this->rowMapping->at(maxnode+1) = curRow;
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*

67
src/utility/GraphAnalyzer.h
View File

@ -9,6 +9,7 @@
#define STORM_UTILITY_GRAPHANALYZER_H_
#include "src/models/AbstractDeterministicModel.h"
#include "src/models/AbstractNonDeterministicModel.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "log4cplus/logger.h"
@ -34,7 +35,7 @@ public:
* probability 1 after the invocation of the function.
*/
template <class T>
static void performProb01(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
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.");
@ -62,7 +63,7 @@ public:
* a positive probability of satisfying phi until psi.
*/
template <class T>
static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
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.");
@ -70,7 +71,7 @@ public:
}
// Get the backwards transition relation from the model to ease the search.
storm::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions();
storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), false);
// Add all psi states as the already satisfy the condition.
*statesWithProbabilityGreater0 |= psiStates;
@ -109,7 +110,7 @@ public:
* have paths satisfying phi until psi.
*/
template <class T>
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
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.");
@ -133,7 +134,7 @@ public:
* have paths satisfying phi until psi.
*/
template <class T>
static void performProb1(storm::models::AbstractDeterministicModel<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability1) {
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.");
@ -146,6 +147,62 @@ public:
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) {
}
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

Write Preview
Loading…
Cancel
Save