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

Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer.

tempestpy_adaptions
dehnert 12 years ago
parent
2fcd6c95fb
commit
ed4c6c8429
8 changed files with 133 additions and 15 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. 4
      src/models/AbstractDeterministicModel.h
  2. 6
      src/models/AbstractModel.h
  3. 4
      src/models/AbstractNondeterministicModel.h
  4. 2
      src/storage/SparseMatrix.h
  5. 6
      src/utility/GraphAnalyzer.h
  6. 117
      test/performance/graph/GraphTest.cpp
  7. 3
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  8. 6
      test/performance/storm-performance-tests.cpp

4
src/models/AbstractDeterministicModel.h
View File

@ -52,7 +52,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const {
return this->getTransitionMatrix()->constColumnIteratorBegin(state);
}
@ -62,7 +62,7 @@ class AbstractDeterministicModel: public AbstractModel<T> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const {
return this->getTransitionMatrix()->constColumnIteratorEnd(state);
}
};

6
src/models/AbstractModel.h
View File

@ -91,7 +91,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @param stronglyConnectedComponents A vector containing the SCCs of the system.
* @param stateToSccMap A mapping from state indices to
*/
virtual storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> const& stateToSccMap) {
storm::storage::SparseMatrix<bool> extractSccDependencyGraph(std::vector<std::vector<uint_fast64_t>> const& stronglyConnectedComponents, std::map<uint_fast64_t, uint_fast64_t> 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<bool> sccDependencyGraph(numberOfStates);
@ -132,7 +132,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) = 0;
virtual typename storm::storage::SparseMatrix<T>::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<AbstractModel<T>> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) = 0;
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const = 0;
/*!
* Returns the state space size of the model.

4
src/models/AbstractNondeterministicModel.h
View File

@ -84,7 +84,7 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) {
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorBegin(uint_fast64_t state) const {
return this->getTransitionMatrix()->constColumnIteratorBegin((*nondeterministicChoiceIndices)[state]);
}
@ -94,7 +94,7 @@ class AbstractNondeterministicModel: public AbstractModel<T> {
* @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<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) {
virtual typename storm::storage::SparseMatrix<T>::ConstIndexIterator constStateSuccessorIteratorEnd(uint_fast64_t state) const {
return this->getTransitionMatrix()->constColumnIteratorEnd((*nondeterministicChoiceIndices)[state + 1] - 1);
}

2
src/storage/SparseMatrix.h
View File

@ -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) {

6
src/utility/GraphAnalyzer.h
View File

@ -428,10 +428,10 @@ public:
* graph of the SCCs.
*/
template <typename T>
static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> performSccDecomposition(storm::models::AbstractNondeterministicModel<T> const& model) {
static std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> performSccDecomposition(storm::models::AbstractModel<T> const& model) {
LOG4CPLUS_INFO(logger, "Computing SCC decomposition.");
std::pair<std::vector<std::vector<uint_fast64_t>>, storm::models::GraphTransitions<T>> sccDecomposition;
std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> 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);
}
}

117
test/performance/graph/GraphTest.cpp
View File

@ -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<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_INFO(logger, "Computing prob01 (3 times) for crowds/crowds20_5.");
std::pair<storm::storage::BitVector, storm::storage::BitVector> 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<double> 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<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
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<double> 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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_INFO(logger, "Computing prob01min for asynchronous_leader/leader7");
std::pair<storm::storage::BitVector, storm::storage::BitVector> 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<double> 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<storm::models::Mdp<double>> mdp2 = parser2.getModel<storm::models::Mdp<double>>();
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<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_INFO(logger, "Computing SCC decomposition of crowds/crowds20_5.");
std::pair<std::vector<std::vector<uint_fast64_t>>, storm::storage::SparseMatrix<bool>> 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<double> 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<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
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<double> 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<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
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<double> 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<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
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);
}

3
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -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;
}
}

6
test/performance/storm-performance-tests.cpp
View File

@ -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<log4cplus::Layout>(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

Write Preview
Loading…
Cancel
Save