From ed4c6c84293173d86ee7414b8f048dd8c838a0bf Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 23:51:56 +0200 Subject: [PATCH] Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer. --- src/models/AbstractDeterministicModel.h | 4 +- src/models/AbstractModel.h | 6 +- src/models/AbstractNondeterministicModel.h | 4 +- src/storage/SparseMatrix.h | 2 +- src/utility/GraphAnalyzer.h | 6 +- test/performance/graph/GraphTest.cpp | 117 ++++++++++++++++++ .../GmmxxDtmcPrctModelCheckerTest.cpp | 3 +- test/performance/storm-performance-tests.cpp | 6 +- 8 files changed, 133 insertions(+), 15 deletions(-) create mode 100644 test/performance/graph/GraphTest.cpp diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 7048ab3ed..1986aa776 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -52,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorBegin(state); } @@ -62,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @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) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorEnd(state); } }; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index e50aa683f..806cfed67 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -91,7 +91,7 @@ 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 */ - virtual storm::storage::SparseMatrix extractSccDependencyGraph(std::vector> const& stronglyConnectedComponents, std::map const& stateToSccMap) { + 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. uint_fast64_t numberOfStates = stronglyConnectedComponents.size(); storm::storage::SparseMatrix sccDependencyGraph(numberOfStates); @@ -132,7 +132,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const = 0; /*! * Returns an iterator pointing to the element past the successors of the given state. @@ -140,7 +140,7 @@ class AbstractModel: public std::enable_shared_from_this> { * @param state The state for which to return the iterator. * @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) = 0; + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const = 0; /*! * Returns the state space size of the model. diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index cd2700a49..d3f0dcf25 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -84,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @return An iterator to the successors of the given state. */ - virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]); } @@ -94,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @param state The state for which to return the iterator. * @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) { + virtual typename storm::storage::SparseMatrix::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const { return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1); } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b0d2a1cc2..4ae474304 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -219,7 +219,7 @@ public: * * @param size The number of rows and columns of the matrix. */ - SparseMatrix(uint_fast64_t size) + SparseMatrix(uint_fast64_t size = 0) : rowCount(size), colCount(size), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h index c8530e7ef..fb272fd99 100644 --- a/src/utility/GraphAnalyzer.h +++ b/src/utility/GraphAnalyzer.h @@ -428,10 +428,10 @@ public: * graph of the SCCs. */ template - static std::pair>, storm::models::GraphTransitions> performSccDecomposition(storm::models::AbstractNondeterministicModel const& model) { + static std::pair>, storm::storage::SparseMatrix> performSccDecomposition(storm::models::AbstractModel const& model) { LOG4CPLUS_INFO(logger, "Computing SCC decomposition."); - std::pair>, storm::models::GraphTransitions> sccDecomposition; + std::pair>, storm::storage::SparseMatrix> sccDecomposition; uint_fast64_t numberOfStates = model.getNumberOfStates(); // Set up the environment of Tarjan's algorithm. @@ -447,7 +447,7 @@ public: 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(), sccDecomposition.first, stateToSccMap); } } diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp new file mode 100644 index 000000000..0d69d3d57 --- /dev/null +++ b/test/performance/graph/GraphTest.cpp @@ -0,0 +1,117 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/utility/Settings.h" +#include "src/parser/AutoParser.h" +#include "src/utility/GraphAnalyzer.h" + +TEST(GraphAnalyzerTest, PerformProb01) { + 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 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); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 46046u); + + prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeIGreater1"))); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 574016u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 825797u); + + prob01 = storm::utility::GraphAnalyzer::performProb01(*dtmc, storm::storage::BitVector(dtmc->getNumberOfStates(), true), storm::storage::BitVector(dtmc->getLabeledStates("observeOnlyTrueSender"))); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 1785309u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 40992u); + LOG4CPLUS_INFO(logger, "Done computing prob01 (3 times) for crowds/crowds20_5."); + + 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"); + 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"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 1312334u); +} + +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"); + 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"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + LOG4CPLUS_INFO(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"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 2095783u); + + 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"); + 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"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); + + LOG4CPLUS_INFO(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"); + + ASSERT_EQ(prob01.first.getNumberOfSetBits(), 0u); + ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616u); +} + +TEST(GraphAnalyzerTest, PerformSCCDecomposition) { + 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."); + + ASSERT_EQ(sccDecomposition.first.size(), 1290297u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1371253u); + + 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"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*dtmc2); + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of synchronous_leader/leader6_8."); + + ASSERT_EQ(sccDecomposition.first.size(), 1279673u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 1535367u); + + 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"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp); + LOG4CPLUS_INFO(logger, "Done computing SCC decomposition of asynchronous_leader/leader7"); + + ASSERT_EQ(sccDecomposition.first.size(), 1914691u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 7023587u); + + 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"); + sccDecomposition = storm::utility::GraphAnalyzer::performSccDecomposition(*mdp2); + LOG4CPLUS_INFO(logger, "Computing SCC decomposition of consensus/coin4_6"); + + ASSERT_EQ(sccDecomposition.first.size(), 63611u); + ASSERT_EQ(sccDecomposition.second.getNonZeroEntryCount(), 213400u); +} \ No newline at end of file diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index 2609ba0a1..3e5aa39b8 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -1,6 +1,5 @@ #include "gtest/gtest.h" #include "storm-config.h" - #include "src/utility/Settings.h" #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "src/parser/AutoParser.h" @@ -112,4 +111,4 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { delete rewardFormula; delete result; -} +} \ No newline at end of file diff --git a/test/performance/storm-performance-tests.cpp b/test/performance/storm-performance-tests.cpp index 1e1317a80..1c52acc03 100644 --- a/test/performance/storm-performance-tests.cpp +++ b/test/performance/storm-performance-tests.cpp @@ -15,10 +15,12 @@ log4cplus::Logger logger; * Initializes the logging framework. */ void setUpLogging() { - log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-functional-tests.log")); + logger = log4cplus::Logger::getInstance(LOG4CPLUS_TEXT("main")); + logger.setLogLevel(log4cplus::INFO_LOG_LEVEL); + log4cplus::SharedAppenderPtr fileLogAppender(new log4cplus::FileAppender("storm-performance-tests.log")); fileLogAppender->setName("mainFileAppender"); + fileLogAppender->setThreshold(log4cplus::WARN_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