From fbe1f41213bef2799a9ec4ce5f3e9545786ddeb1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 16 May 2013 16:19:00 +0200 Subject: [PATCH] Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests. --- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 2 +- ...ogicalValueIterationMdpPrctlModelChecker.h | 6 +- src/models/AbstractDeterministicModel.h | 5 +- src/models/AbstractModel.h | 73 ++++- src/models/AbstractNondeterministicModel.h | 7 +- src/models/GraphTransitions.h | 258 ------------------ src/storage/SparseMatrix.h | 24 +- src/utility/GraphAnalyzer.h | 41 ++- test/functional/storm-functional-tests.cpp | 9 +- test/performance/graph/GraphTest.cpp | 98 +++++-- .../GmmxxDtmcPrctModelCheckerTest.cpp | 14 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 40 ++- test/performance/storm-performance-tests.cpp | 12 +- 13 files changed, 244 insertions(+), 345 deletions(-) delete mode 100644 src/models/GraphTransitions.h diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index 48c4c6304..3b340dadf 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -151,7 +151,7 @@ private: if (converged) { LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations."); } else { - LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); + LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } } }; diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h index 1466c02ec..7368a91bf 100644 --- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h +++ b/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h @@ -67,10 +67,8 @@ private: bool relative = s->get("relative"); // Now, we need to determine the SCCs of the MDP and a topological sort. - std::pair>, storm::models::GraphTransitions> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); - std::vector> stronglyConnectedComponents = std::move(sccDecomposition.first); - storm::models::GraphTransitions stronglyConnectedComponentsDependencyGraph = std::move(sccDecomposition.second); - + std::vector> stronglyConnectedComponents = storm::utility::GraphAnalyzer::performSccDecomposition(this->getModel(), stronglyConnectedComponents, stronglyConnectedComponentsDependencyGraph); + storm::storage::SparseMatrix stronglyConnectedComponentsDependencyGraph = this->getModel().extractSccDependencyGraph(stronglyConnectedComponents); std::vector topologicalSort = storm::utility::GraphAnalyzer::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 1986aa776..a45b5df77 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -2,7 +2,6 @@ #define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ #include "AbstractModel.h" -#include "GraphTransitions.h" #include @@ -53,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorBegin(state); + return this->transitionMatrix->constColumnIteratorBegin(state); } /*! @@ -63,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorEnd(state); + return this->transitionMatrix->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 806cfed67..c4896a6c6 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,9 +91,20 @@ class AbstractModel: public std::enable_shared_from_this> { * @param stronglyConnectedComponents A vector containing the SCCs of the system. * @param stateToSccMap A mapping from state indices to */ - storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) const { - // The resulting sparse matrix will have as many rows/columns as there are SCCs. + storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents) const { uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); + + // First, we need to create a mapping of states to their SCC index, to ease the computation + // of dependency transitions later. + std::vector stateToSccMap(this->getNumberOfStates()); + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (uint_fast64_t j = 0; j < stronglyConnectedComponents[i].size(); ++j) { + stateToSccMap[stronglyConnectedComponents[i][j]] = i; + } + } + + // The resulting sparse matrix will have as many rows/columns as there are SCCs. + storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); sccDependencyGraph.initialize(); @@ -105,7 +116,7 @@ class AbstractModel: public std::enable_shared_from_this> { std::set allTargetSccs; for (auto state : scc) { for (typename storm::storage::SparseMatrix::ConstIndexIterator succIt = this->constStateSuccessorIteratorBegin(state), succIte = this->constStateSuccessorIteratorEnd(state); succIt != succIte; ++succIt) { - uint_fast64_t targetScc = stateToSccMap.find(*succIt)->second; + uint_fast64_t targetScc = stateToSccMap[*succIt]; // We only need to consider transitions that are actually leaving the SCC. if (targetScc != currentSccIndex) { @@ -125,6 +136,59 @@ class AbstractModel: public std::enable_shared_from_this> { return sccDependencyGraph; } + + /*! + * Retrieves the backward transition relation of the model, i.e. a set of transitions + * between states that correspond to the reversed transition relation of this model. + * + * @return A sparse matrix that represents the backward transitions of this model. + */ + virtual storm::storage::SparseMatrix getBackwardTransitions() const { + uint_fast64_t numberOfStates = this->getNumberOfStates(); + uint_fast64_t numberOfTransitions = this->getNumberOfTransitions(); + + std::vector rowIndications(numberOfStates + 1); + std::vector columnIndications(numberOfTransitions); + std::vector values(numberOfTransitions, true); + + // First, we need to count how many backward transitions each state has. + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { + rowIndications[*rowIt + 1]++; + } + } + + // Now compute the accumulated offsets. + for (uint_fast64_t i = 1; i < numberOfStates; ++i) { + rowIndications[i] = rowIndications[i - 1] + rowIndications[i]; + } + + // Put a sentinel element at the end of the indices list. This way, + // for each state i the range of indices can be read off between + // state_indices_list[i] and state_indices_list[i + 1]. + // FIXME: This should not be necessary and already be implied by the first steps. + rowIndications[numberOfStates] = numberOfTransitions; + + // Create an array that stores the next index for each state. Initially + // this corresponds to the previously computed accumulated offsets. + std::vector nextIndices = rowIndications; + + // Now we are ready to actually fill in the list of predecessors for + // every state. Again, we start by considering all but the last row. + for (uint_fast64_t i = 0; i < numberOfStates; ++i) { + for (auto rowIt = this->constStateSuccessorIteratorBegin(i), rowIte = this->constStateSuccessorIteratorEnd(i); rowIt != rowIte; ++rowIt) { + columnIndications[nextIndices[*rowIt]++] = i; + } + } + + storm::storage::SparseMatrix backwardTransitionMatrix(numberOfStates, numberOfStates, + numberOfTransitions, + std::move(rowIndications), + std::move(columnIndications), + std::move(values)); + + return backwardTransitionMatrix; + } /*! * Returns an iterator to the successors of the given state. @@ -269,10 +333,11 @@ class AbstractModel: public std::enable_shared_from_this> { << std::endl; } - private: + protected: /*! A matrix representing the likelihoods of moving between states. */ std::shared_ptr> transitionMatrix; +private: /*! The labeling of the states of the model. */ std::shared_ptr stateLabeling; diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index d3f0dcf25..b64359d2f 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -2,7 +2,6 @@ #define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_ #include "AbstractModel.h" -#include "GraphTransitions.h" #include @@ -56,7 +55,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return The number of choices for all states of the MDP. */ uint_fast64_t getNumberOfChoices() const { - return this->getTransitionMatrix()->getRowCount(); + return this->transitionMatrix->getRowCount(); } /*! @@ -85,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator to the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); + return this->transitionMatrix->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); } /*! @@ -95,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return An iterator pointing to the element past the successors of the given state. */ virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { - return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); + return this->transitionMatrix->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); } private: diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h deleted file mode 100644 index de435a00b..000000000 --- a/src/models/GraphTransitions.h +++ /dev/null @@ -1,258 +0,0 @@ -/* - * GraphTransitions.h - * - * Created on: 17.11.2012 - * Author: Christian Dehnert - */ - -#ifndef STORM_MODELS_GRAPHTRANSITIONS_H_ -#define STORM_MODELS_GRAPHTRANSITIONS_H_ - -#include "src/storage/SparseMatrix.h" - -#include -#include - -namespace storm { - -namespace models { - -/*! - * This class stores the successors of all states in a state space of the - * given size. - */ -template -class GraphTransitions { - -public: - /*! - * Just typedef the iterator as a pointer to the index type. - */ - typedef const uint_fast64_t * stateSuccessorIterator; - - //! Constructor - /*! - * Constructs an object representing the graph structure of the given - * transition relation, which is given by a sparse matrix. - * @param transitionMatrix The (0-based) matrix representing the transition - * relation. - * @param forward If set to true, this objects will store the graph structure - * of the backwards transition relation. - */ - GraphTransitions(storm::storage::SparseMatrix const& transitionMatrix, bool forward) - : numberOfStates(transitionMatrix.getColumnCount()), numberOfTransitions(transitionMatrix.getNonZeroEntryCount()), successorList(numberOfTransitions), stateIndications(numberOfStates + 1) { - if (forward) { - this->initializeForward(transitionMatrix); - } else { - this->initializeBackward(transitionMatrix); - } - } - - GraphTransitions(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, bool forward) - : numberOfStates(transitionMatrix.getColumnCount()), numberOfTransitions(transitionMatrix.getNonZeroEntryCount()), successorList(numberOfTransitions), stateIndications(numberOfStates + 1) { - if (forward) { - this->initializeForward(transitionMatrix, nondeterministicChoiceIndices); - } else { - this->initializeBackward(transitionMatrix, nondeterministicChoiceIndices); - } - } - - GraphTransitions(GraphTransitions const& transitions, std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) - : numberOfStates(stronglyConnectedComponents.size()), numberOfTransitions(0), successorList(), stateIndications(numberOfStates + 1) { - this->initializeFromSccDecomposition(transitions, stronglyConnectedComponents, stateToSccMap); - } - - GraphTransitions() : numberOfStates(0), numberOfTransitions(0), successorList(), stateIndications() { - // Intentionally left empty. - } - - /*! - * Retrieves the size of the internal representation of the graph transitions in memory. - * @return the size of the internal representation of the graph transitions in memory - * measured in bytes. - */ - virtual uint_fast64_t getSizeInMemory() const { - uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfTransitions + 1) * sizeof(uint_fast64_t); - return result; - } - - uint_fast64_t getNumberOfStates() const { - return numberOfStates; - } - - uint_fast64_t getNumberOfTransitions() const { - return numberOfTransitions; - } - - /*! - * Returns an iterator to the successors of the given state. - * @param state The state for which to get the successor iterator. - * @return An iterator to the predecessors of the given states. - */ - stateSuccessorIterator beginStateSuccessorsIterator(uint_fast64_t state) const { - return &(this->successorList[0]) + this->stateIndications[state]; - } - - /*! - * Returns an iterator referring to the element after the successors of - * the given state. - * @param state The state for which to get the iterator. - * @return An iterator referring to the element after the successors of - * the given state. - */ - stateSuccessorIterator endStateSuccessorsIterator(uint_fast64_t state) const { - return &(this->successorList[0]) + this->stateIndications[state + 1]; - } - - /*! - * Returns a (naive) string representation of the transitions in this object. - * @returns a (naive) string representation of the transitions in this object. - */ - std::string toString() const { - std::stringstream stream; - for (uint_fast64_t state = 0; state < numberOfStates; ++state) { - for (auto succIt = this->beginStateSuccessorsIterator(state), succIte = this->endStateSuccessorsIterator(state); succIt != succIte; ++succIt) { - stream << state << " -> " << *succIt << std::endl; - } - } - return stream.str(); - } - -private: - /*! - * Initializes this graph transitions object using the forward transition - * relation given by means of a sparse matrix. - */ - void initializeForward(storm::storage::SparseMatrix const& transitionMatrix) { - // First, we copy the index list from the sparse matrix as this will - // stay the same. - std::copy(transitionMatrix.constColumnIteratorBegin(), transitionMatrix.constColumnIteratorEnd(), this->stateIndications.begin()); - - // Now we can iterate over all rows of the transition matrix and record the target state. - for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->successorList[currentNonZeroElement++] = *rowIt; - } - } - } - - void initializeForward(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices) { - // We can directly copy the starting indices from the transition matrix as we do not - // eliminate duplicate transitions and therefore will have as many non-zero entries as this - // matrix. - typename storm::storage::SparseMatrix::ConstRowsIterator rowsIt(transitionMatrix); - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - rowsIt.moveToRow(nondeterministicChoiceIndices[i]); - this->stateIndications[i] = rowsIt.index(); - } - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Now we can iterate over all rows of the transition matrix and record - // the target state. - for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->successorList[currentNonZeroElement++] = *rowIt; - } - } - } - } - - /*! - * Initializes this graph transitions object using the backwards transition - * relation, whose forward transition relation is given by means of a sparse - * matrix. - */ - void initializeBackward(storm::storage::SparseMatrix const& transitionMatrix) { - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->stateIndications[*rowIt + 1]++; - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; ++i) { - this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i]; - } - - // Put a sentinel element at the end of the indices list. This way, - // for each state i the range of indices can be read off between - // state_indices_list[i] and state_indices_list[i + 1]. - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = stateIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(i); rowIt != transitionMatrix.constColumnIteratorEnd(i); ++rowIt) { - this->successorList[nextIndices[*rowIt]++] = i; - } - } - } - - void initializeBackward(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices) { - // First, we need to count how many backward transitions each state has. - for (uint_fast64_t i = 0; i < numberOfStates; ++i) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->stateIndications[*rowIt + 1]++; - } - } - } - - // Now compute the accumulated offsets. - for (uint_fast64_t i = 1; i < numberOfStates; i++) { - this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i]; - } - - // Put a sentinel element at the end of the indices list. This way, - // for each state i the range of indices can be read off between - // state_indices_list[i] and state_indices_list[i + 1]. - this->stateIndications[numberOfStates] = numberOfTransitions; - - // Create an array that stores the next index for each state. Initially - // this corresponds to the previously computed accumulated offsets. - std::vector nextIndices = stateIndications; - - // Now we are ready to actually fill in the list of predecessors for - // every state. Again, we start by considering all but the last row. - for (uint_fast64_t i = 0; i < numberOfStates; i++) { - for (uint_fast64_t j = nondeterministicChoiceIndices[i]; j < nondeterministicChoiceIndices[i + 1]; ++j) { - for (auto rowIt = transitionMatrix.constColumnIteratorBegin(j); rowIt != transitionMatrix.constColumnIteratorEnd(j); ++rowIt) { - this->successorList[nextIndices[*rowIt]++] = i; - } - } - } - } - - /*! - * Store the number of states to determine the highest index at which the - * state_indices_list may be accessed. - */ - uint_fast64_t numberOfStates; - - /*! - * Store the number of non-zero transition entries to determine the highest - * index at which the predecessor_list may be accessed. - */ - uint_fast64_t numberOfTransitions; - - /*! A list of successors for *all* states. */ - std::vector successorList; - - /*! - * A list of indices indicating at which position in the global array the - * successors of a state can be found. - */ - std::vector stateIndications; -}; - -} // namespace models - -} // namespace storm - -#endif /* STORM_MODELS_GRAPHTRANSITIONS_H_ */ diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 4ae474304..a968f7ee5 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -211,7 +211,7 @@ public: */ SparseMatrix(uint_fast64_t rows, uint_fast64_t cols) : rowCount(rows), colCount(cols), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { - + // Intentionally left empty. } /*! @@ -222,8 +222,28 @@ public: SparseMatrix(uint_fast64_t size = 0) : rowCount(size), colCount(size), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { - + // Intentionally left empty. } + + /*! + * Constructs a sparse matrix object with the given (moved) contents. + * + * @param rowCount The number of rows. + * @param colCount The number of columns. + * @param nonZeroEntryCount The number of non-zero entries. + * @param rowIndications The vector indicating where the rows start. + * @param columnIndications The vector indicating the column for each non-zero element. + * @param values The vector containing the non-zero values. + */ + SparseMatrix(uint_fast64_t rowCount, uint_fast64_t colCount, uint_fast64_t nonZeroEntryCount, + std::vector&& rowIndications, + std::vector&& columnIndications, std::vector&& values) + : rowCount(rowCount), colCount(colCount), nonZeroEntryCount(nonZeroEntryCount), + valueStorage(values), columnIndications(columnIndications), + rowIndications(rowIndications), internalStatus(MatrixStatus::Initialized), + currentSize(0), lastRow(0) { + // Intentionally left empty. + } /*! * Initializes the sparse matrix with the given number of non-zero entries diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index fb272fd99..577bccf74 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -58,7 +58,7 @@ public: storm::storage::BitVector statesWithProbabilityGreater0(model.getNumberOfStates()); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbabilityGreater0 |= psiStates; @@ -73,7 +73,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState); it != backwardTransitions.constColumnIteratorEnd(currentState); ++it) { if (phiStates.get(*it) && !statesWithProbabilityGreater0.get(*it)) { statesWithProbabilityGreater0.set(*it, true); stack.push_back(*it); @@ -161,7 +161,7 @@ public: storm::storage::BitVector statesWithProbability0(model.getNumberOfStates()); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -176,7 +176,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++it) { if (phiStates.get(*it) && !statesWithProbability0.get(*it)) { statesWithProbability0.set(*it, true); stack.push_back(*it); @@ -207,7 +207,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); storm::storage::BitVector currentStates(model.getNumberOfStates(), true); @@ -225,7 +225,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++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. @@ -300,7 +300,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*transitionMatrix, *nondeterministicChoiceIndices, false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Add all psi states as the already satisfy the condition. statesWithProbability0 |= psiStates; @@ -315,7 +315,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++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. @@ -366,7 +366,7 @@ public: std::shared_ptr> nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); // Get the backwards transition relation from the model to ease the search. - storm::models::GraphTransitions backwardTransitions(*model.getTransitionMatrix(), *model.getNondeterministicChoiceIndices(), false); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); storm::storage::BitVector currentStates(model.getNumberOfStates(), true); @@ -384,7 +384,7 @@ public: uint_fast64_t currentState = stack.back(); stack.pop_back(); - for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) { + for(auto it = backwardTransitions.constColumnIteratorBegin(currentState), ite = backwardTransitions.constColumnIteratorEnd(currentState); it != ite; ++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. @@ -421,17 +421,16 @@ public: } /*! - * Performs a decomposition of the given nondeterministic model into its SCCs. + * Performs a decomposition of the given model into its SCCs. * * @param model The nondeterminstic model to decompose. - * @return A pair whose first component represents the SCCs and whose second component represents the dependency - * graph of the SCCs. + * @return A vector of SCCs of the model. */ template - static std::pair>, storm::storage::SparseMatrix> performSccDecomposition(storm::models::AbstractModel const& model) { + static std::vector> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - std::pair>, storm::storage::SparseMatrix> sccDecomposition; + std::vector> scc; uint_fast64_t numberOfStates = model.getNumberOfStates(); // Set up the environment of Tarjan's algorithm. @@ -441,21 +440,17 @@ public: std::vector stateIndices(numberOfStates); std::vector lowlinks(numberOfStates); storm::storage::BitVector visitedStates(numberOfStates); - std::map stateToSccMap; // Start the search for SCCs from every vertex in the graph structure, because there is. uint_fast64_t currentIndex = 0; for (uint_fast64_t state = 0; state < numberOfStates; ++state) { if (!visitedStates.get(state)) { - performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), sccDecomposition.first, stateToSccMap); + performSccDecompositionHelper(state, currentIndex, stateIndices, lowlinks, tarjanStack, tarjanStackStates, visitedStates, *model.getTransitionMatrix(), scc); } } - - // Finally, determine the dependency graph over the SCCs and return result. - sccDecomposition.second = model.extractSccDependencyGraph(sccDecomposition.first, stateToSccMap); LOG4CPLUS_INFO(logger, "Done computing SCC decomposition."); - return sccDecomposition; + return scc; } /*! @@ -551,10 +546,9 @@ private: * @param visitedStates A bit vector that stores all states that have already been visited. * @param matrix The transition matrix representing the graph structure. * @param stronglyConnectedComponents A vector of strongly connected components to which newly found SCCs are added. - * @param stateToSccMap A mapping from state indices to SCC indices that maps each state to its SCC. */ template - static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents, std::map& stateToSccMap) { + static void performSccDecompositionHelper(uint_fast64_t startState, uint_fast64_t& currentIndex, std::vector& stateIndices, std::vector& lowlinks, std::vector& tarjanStack, storm::storage::BitVector& tarjanStackStates, storm::storage::BitVector& visitedStates, storm::storage::SparseMatrix const& matrix, std::vector>& stronglyConnectedComponents) { // Create the stacks needed for turning the recursive formulation of Tarjan's algorithm // into an iterative version. In particular, we keep one stack for states and one stack // for the iterators. The last one is not strictly needed, but reduces iteration work when @@ -623,7 +617,6 @@ private: // Add the state to the current SCC. stronglyConnectedComponents.back().push_back(lastState); - stateToSccMap[lastState] = stronglyConnectedComponents.size() - 1; } while (lastState != currentState); } diff --git a/test/functional/storm-functional-tests.cpp b/test/functional/storm-functional-tests.cpp index 7139bed3c..abfb5a125 100644 --- a/test/functional/storm-functional-tests.cpp +++ b/test/functional/storm-functional-tests.cpp @@ -15,10 +15,12 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::ERROR_LOG_LEVEL); log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setThreshold(log4cplus::FATAL_LOG_LEVEL); fileLogAppender->setLayout(std::auto_ptr(new log4cplus::PatternLayout("%-5p - %D{%H:%M} (%r ms) - %F:%L : %m%n"))); - logger = log4cplus::Logger::getInstance("mainLogger"); logger.addAppender(fileLogAppender); // Uncomment these lines to enable console logging output @@ -62,5 +64,8 @@ int main(int argc, char* argv[]) { testing::InitGoogleTest(&argc, argv); - return RUN_ALL_TESTS(); + int result = RUN_ALL_TESTS(); + + logger.closeNestedAppenders(); + return result; } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 0d69d3d57..84f264004 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -9,7 +9,7 @@ TEST(GraphAnalyzerTest, PerformProb01) { std::shared_ptr> dtmc = parser.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01 (3 times) for crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); std::pair prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observe0Greater1"))); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1724414u); @@ -24,94 +24,132 @@ TEST(GraphAnalyzerTest, PerformProb01) { ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); - LOG4CPLUS_INFO(logger, "Done computing prob01 (3 times) for crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Done."); + + dtmc = nullptr; storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); std::shared_ptr> dtmc2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01 for synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8..."); prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc2, storm::storage::BitVector(dtmc2->getNumberOfStates(), true), storm::storage::BitVector(dtmc2->getLabeledStates("elected"))); - LOG4CPLUS_INFO(logger, "Done computing prob01 for synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); + + dtmc2 = nullptr; } TEST(GraphAnalyzerTest, PerformProb01MinMax) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr> mdp = parser.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01min for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7..."); std::pair prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); - LOG4CPLUS_INFO(logger, "Done computing prob01min for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); - LOG4CPLUS_INFO(logger, "Computing prob01max for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing prob01max for asynchronous_leader/leader7..."); prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp, storm::storage::BitVector(mdp->getNumberOfStates(), true), mdp->getLabeledStates("elected")); - LOG4CPLUS_INFO(logger, "Done computing prob01max for asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + mdp = nullptr; storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); std::shared_ptr> mdp2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing prob01min for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6..."); prob01 = storm::utility::GraphAnalyzer::performProb01Min(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); - LOG4CPLUS_INFO(logger, "Done computing prob01min for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); - LOG4CPLUS_INFO(logger, "Computing prob01max for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing prob01max for consensus/coin4_6..."); prob01 = storm::utility::GraphAnalyzer::performProb01Max(*mdp2, storm::storage::BitVector(mdp2->getNumberOfStates(), true), mdp2->getLabeledStates("finished")); - LOG4CPLUS_INFO(logger, "Done computing prob01max for consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + + mdp2 = nullptr; } -TEST(GraphAnalyzerTest, PerformSCCDecomposition) { +TEST(GraphAnalyzerTest, PerformSCCDecompositionAndGetDependencyGraph) { storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr> dtmc = parser.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of crowds/crowds20_5."); - std::pair>, storm::storage::SparseMatrix> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); - LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of crowds/crowds20_5."); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5..."); + std::vector> sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1290297u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1371253u); + ASSERT_EQ(sccDecomposition.size(), 1290297u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5..."); + storm::storage::SparseMatrix sccDependencyGraph = dtmc->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1371253u); + + dtmc = nullptr; storm::parser::AutoParser parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew"); std::shared_ptr> dtmc2 = parser2.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8."); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1279673u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1535367u); + ASSERT_EQ(sccDecomposition.size(), 1279673u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); + sccDependencyGraph = dtmc2->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); + + dtmc2 = nullptr; + + /* storm::parser::AutoParser parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew"); std::shared_ptr> mdp = parser3.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader7..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp); - LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of asynchronous_leader/leader7"); + LOG4CPLUS_WARN(logger, "Done."); - ASSERT_EQ(sccDecomposition.first.size(), 1914691u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 7023587u); + ASSERT_EQ(sccDecomposition.size(), 1914691u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader7..."); + sccDependencyGraph = mdp->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 7023587u); + + mdp = nullptr; + */ storm::parser::AutoParser parser4(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); std::shared_ptr> mdp2 = parser4.getModel>(); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6..."); sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2); - LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDecomposition.size(), 63611u); + + LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); + sccDependencyGraph = mdp2->extractSccDependencyGraph(sccDecomposition); + LOG4CPLUS_WARN(logger, "Done."); + + ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u); - ASSERT_EQ(sccDecomposition.first.size(), 63611u); - ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 213400u); + mdp2 = nullptr; } \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 3e5aa39b8..bf0a72403 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -22,7 +22,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5..."); std::vector* result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -35,8 +37,10 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5..."); result = probFormula->check(mc); - + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_NE(nullptr, result); ASSERT_LT(std::abs((*result)[0] - 0.05072232915), s->get("precision")); @@ -48,7 +52,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5..."); result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -77,7 +83,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8..."); std::vector* result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -90,7 +98,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), apFormula, 20); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); + LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8..."); result = probFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -103,7 +113,9 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); + LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8..."); result = rewardFormula->check(mc); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); diff --git a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp index dc9bea32b..cf8e91581 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp @@ -22,7 +22,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F elected] on asynchronous_leader/leader7..."); std::vector* result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -35,7 +37,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { eventuallyFormula = new storm::property::prctl::Eventually(apFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -48,7 +52,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=25 elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -61,7 +67,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 25); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=25 elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -74,7 +82,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F elected] on asynchronous_leader/leader7..."); result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_LT(std::abs((*result)[0] - 6.172433512), s->get("precision")); @@ -85,7 +95,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = mc.checkNoBoundOperator(*rewardFormula);; + LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F elected] on asynchronous_leader/leader7..."); + result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done"); ASSERT_NE(nullptr, result); @@ -97,6 +109,8 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::settings::Settings* s = storm::settings::instance(); + s->set("maxiter", 20000); + std::cout << s->get("maxiter") << std::endl; storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); @@ -112,7 +126,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished] on consensus/coin4_6..."); std::vector* result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -127,7 +143,9 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F finished & all_coins_equal_0] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); @@ -142,10 +160,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & all_coins_equal_1] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0.5282872761373342829216), s->get("precision")); delete probFormula; @@ -158,10 +177,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { eventuallyFormula = new storm::property::prctl::Eventually(andFormula); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F finished & !agree] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0.10343451035775527713), s->get("precision")); delete probFormula; @@ -171,10 +191,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Pmin=? [F<=50 finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; @@ -184,10 +205,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(apFormula, 50); probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + LOG4CPLUS_WARN(logger, "Model Checking Pmax=? [F<=50 finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*probFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 0), s->get("precision")); delete probFormula; @@ -197,8 +219,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); + LOG4CPLUS_WARN(logger, "Model Checking Rmin=? [F finished] on consensus/coin4_6..."); result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); + ASSERT_NE(nullptr, result); ASSERT_LT(std::abs((*result)[31168] - 1725.5933133943854045), s->get("precision")); delete rewardFormula; @@ -208,10 +233,11 @@ TEST(GmmxxMdpPrctModelCheckerTest, Consensus) { reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(apFormula); rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - result = mc.checkNoBoundOperator(*rewardFormula);; + LOG4CPLUS_WARN(logger, "Model Checking Rmax=? [F finished] on consensus/coin4_6..."); + result = mc.checkNoBoundOperator(*rewardFormula); + LOG4CPLUS_WARN(logger, "Done."); ASSERT_NE(nullptr, result); - ASSERT_LT(std::abs((*result)[31168] - 2179.014847073392047605011), s->get("precision")); delete rewardFormula; diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp index 1c52acc03..49983a9e1 100644 --- a/test/performance/storm-performance-tests.cpp +++ b/test/performance/storm-performance-tests.cpp @@ -16,7 +16,7 @@ log4cplus::Logger logger; */ void setUpLogging() { logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); - logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + logger.setLogLevel(log4cplus::WARN_LOG_LEVEL); log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-performance-tests.log")); fileLogAppender->setName("mainFileAppender"); fileLogAppender->setThreshold(log4cplus::WARN_LOG_LEVEL); @@ -42,9 +42,8 @@ bool parseOptions(int const argc, char const * const argv[]) { storm::settings::Settings::registerModule>(); s = storm::settings::newInstance(argc, argv, nullptr, true); } catch (storm::exceptions::InvalidSettingsException& e) { - std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; - std::cout << std::endl << storm::settings::help; - return false; + // Ignore this case. + return true; } if (s->isSet("help")) { @@ -64,5 +63,8 @@ int main(int argc, char* argv[]) { testing::InitGoogleTest(&argc, argv); - return RUN_ALL_TESTS(); + int result = RUN_ALL_TESTS(); + + logger.closeNestedAppenders(); + return result; }