diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index c669a295c..aa44ba736 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel { AbstractDeterministicModel(std::shared_ptr> transitionMatrix, std::shared_ptr stateLabeling, std::shared_ptr> stateRewardVector, std::shared_ptr> transitionRewardMatrix) - : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix), backwardTransitions(nullptr) { + : AbstractModel(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) { } /*! @@ -42,42 +42,9 @@ class AbstractDeterministicModel: public AbstractModel { /*! * Copy Constructor. */ - AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel(other), backwardTransitions(nullptr) { - if (other.backwardTransitions != nullptr) { - backwardTransitions = new storm::models::GraphTransitions(*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::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& getBackwardTransitions() { - if (this->backwardTransitions == nullptr) { - this->backwardTransitions = std::shared_ptr>(new storm::models::GraphTransitions(this->getTransitionMatrix(), this->getNumberOfStates(), false)); - } - return *this->backwardTransitions; + AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel(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> backwardTransitions; }; } // namespace models diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h index 561165501..64d5c65cd 100644 --- a/src/models/GraphTransitions.h +++ b/src/models/GraphTransitions.h @@ -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> transitionMatrix, uint_fast64_t numberOfStates, bool forward) - : successorList(nullptr), stateIndications(nullptr), numberOfStates(numberOfStates), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { + GraphTransitions(std::shared_ptr> transitionMatrix, bool forward) + : successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) { if (forward) { this->initializeForward(transitionMatrix); } else { diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index f6b70e719..26436fb55 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s /* * Create row mapping. */ - this->rowMapping = std::shared_ptr>(new std::vector(maxnode+1,0)); + this->rowMapping = std::shared_ptr>(new std::vector(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."; /* diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index 07ba3eeaf..3464c9710 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -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 - static void performProb01(storm::models::AbstractDeterministicModel& 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& 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 - static void performProbGreater0(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) { + static void performProbGreater0(storm::models::AbstractDeterministicModel& 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& backwardTransitions = model.getBackwardTransitions(); + storm::models::GraphTransitions 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 - static void performProb1(storm::models::AbstractDeterministicModel& 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& 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 - static void performProb1(storm::models::AbstractDeterministicModel& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* statesWithProbability1) { + static void performProb1(storm::models::AbstractDeterministicModel& 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 + static void performProb01Max(storm::models::AbstractNonDeterministicModel& 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 + static void performProb0A(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + + } + + template + static void performProb1E(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) { + + } + + template + static void performProb01Min(storm::models::AbstractNonDeterministicModel& 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 + static void performProb0E(storm::models::AbstractNonDeterministicModel& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) { + + } + + template + static void performProb1A(storm::models::AbstractNonDeterministicModel& 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