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

Fixed SCC decomposition. Added functional tests for SCC decomposition. 

Former-commit-id: 25a7805fcb
tempestpy_adaptions
dehnert 11 years ago
parent
e80bb0caa5
commit
f79329bd9d
6 changed files with 142 additions and 99 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/storage/MaximalEndComponentDecomposition.cpp
  2. 28
      src/storage/StronglyConnectedComponentDecomposition.cpp
  3. 33
      test/functional/storage/MaximalEndComponentDecompositionTest.cpp
  4. 46
      test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
  5. 70
      test/performance/graph/GraphTest.cpp
  6. 48
      test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp

4
src/storage/MaximalEndComponentDecomposition.cpp
View File

@ -73,7 +73,7 @@ namespace storm {
// We need to do another iteration in case we have either more than once SCC or the SCC is smaller than
// the MEC canditate itself.
mecChanged |= sccs.size() > 1 || sccs[0].size() < mec.size();
mecChanged |= sccs.size() > 1 || (sccs.size() > 0 && sccs[0].size() < mec.size());
// Check for each of the SCCs whether there is at least one action for each state that does not leave the SCC.
for (auto& scc : sccs) {
@ -115,7 +115,7 @@ namespace storm {
// Now check which states should be reconsidered, because successors of them were removed.
statesToCheck.clear();
for (auto state : statesToRemove) {
for (auto const& entry : transitionMatrix.getRow(state)) {
for (auto const& entry : backwardTransitions.getRow(state)) {
if (scc.find(entry.first) != scc.end()) {
statesToCheck.set(entry.first);
}

28
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -94,12 +94,6 @@ namespace storm {
statesWithSelfloop = storm::storage::BitVector(lowlinks.size());
}
// Store a bit vector of all states that can leave their SCC to be able to detect bottom SCCs.
storm::storage::BitVector statesThatCanLeaveTheirScc;
if (onlyBottomSccs) {
statesThatCanLeaveTheirScc = storm::storage::BitVector(lowlinks.size());
}
// Initialize the recursion stacks with the given initial state (and its successor iterator).
recursionStateStack.push_back(startState);
recursionIteratorStack.push_back(model.getRows(startState).begin());
@ -144,18 +138,9 @@ namespace storm {
recursionStepBackward:
lowlinks[currentState] = std::min(lowlinks[currentState], lowlinks[successorIt->first]);
// If we are interested in bottom SCCs only, we need to check whether the current state
// can leave the SCC.
if (onlyBottomSccs && lowlinks[currentState] != lowlinks[successorIt->first]) {
statesThatCanLeaveTheirScc.set(currentState);
}
} else if (tarjanStackStates.get(successorIt->first)) {
// Update the lowlink of the current state.
lowlinks[currentState] = std::min(lowlinks[currentState], stateIndices[successorIt->first]);
// Since it is known that in this case, the successor state is in the same SCC as the
// current state we don't need to update the bit vector of states that can leave their SCC.
}
}
}
@ -166,7 +151,6 @@ namespace storm {
Block scc;
uint_fast64_t lastState = 0;
bool isBottomScc = true;
do {
// Pop topmost state from the algorithm's stack.
lastState = tarjanStack.back();
@ -175,11 +159,19 @@ namespace storm {
// Add the state to the current SCC.
scc.insert(lastState);
} while (lastState != currentState);
if (onlyBottomSccs && isBottomScc && statesThatCanLeaveTheirScc.get(lastState)) {
bool isBottomScc = true;
if (onlyBottomSccs) {
for (auto const& state : scc) {
for (auto const& successor : model.getRows(state)) {
if (scc.find(successor.first) == scc.end()) {
isBottomScc = false;
break;
}
}
}
}
} while (lastState != currentState);
// Now determine whether we want to keep this SCC in the decomposition.
// First, we need to check whether we should drop the SCC because of the requirement to not include

33
test/functional/storage/MaximalEndComponentDecompositionTest.cpp
View File

@ -3,7 +3,7 @@
#include "src/parser/AutoParser.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
TEST(MaximalEndComponentDecomposition, FullSystem) {
TEST(MaximalEndComponentDecomposition, FullSystem1) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
@ -71,6 +71,35 @@ TEST(MaximalEndComponentDecomposition, FullSystem) {
}
}
TEST(MaximalEndComponentDecomposition, FullSystem2) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
ASSERT_EQ(1, mecDecomposition.size());
// Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0];
if (mec1.containsState(4)) {
ASSERT_TRUE(mec1.containsState(5));
ASSERT_TRUE(mec1.containsState(6));
ASSERT_TRUE(mec1.containsState(7));
ASSERT_FALSE(mec1.containsState(0));
ASSERT_FALSE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(2));
ASSERT_FALSE(mec1.containsState(3));
ASSERT_FALSE(mec1.containsState(8));
ASSERT_FALSE(mec1.containsState(9));
ASSERT_FALSE(mec1.containsState(10));
} else {
// This case must never happen as the only two existing MECs contain 4.
ASSERT_TRUE(false);
}
}
TEST(MaximalEndComponentDecomposition, Subsystem) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
@ -86,8 +115,6 @@ TEST(MaximalEndComponentDecomposition, Subsystem) {
storm::storage::MaximalEndComponent const& mec1 = mecDecomposition[0];
std::cout << mec1 << std::endl;
if (mec1.containsState(3)) {
ASSERT_TRUE(mec1.containsState(8));
ASSERT_TRUE(mec1.containsState(9));

46
test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

@ -0,0 +1,46 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
TEST(StronglyConnectedComponentDecomposition, FullSystem1) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton));
ASSERT_EQ(5, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true));
ASSERT_EQ(2, sccDecomposition.size());
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, true));
ASSERT_EQ(2, sccDecomposition.size());
markovAutomaton = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, false));
ASSERT_EQ(sccDecomposition.size(), 2);
// Now, because there is no ordering we have to check the contents of the MECs in a symmetrical way.
storm::storage::StateBlock const& scc1 = sccDecomposition[0];
storm::storage::StateBlock const& scc2 = sccDecomposition[1];
std::vector<uint_fast64_t> correctScc1 = {1, 3, 8, 9, 10};
std::vector<uint_fast64_t> correctScc2 = {4, 5, 6, 7};
ASSERT_TRUE(scc1 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc1 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
ASSERT_TRUE(scc2 == storm::storage::StateBlock(correctScc1.begin(), correctScc1.end()) || scc2 == storm::storage::StateBlock(correctScc2.begin(), correctScc2.end()));
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, true));
ASSERT_EQ(1, sccDecomposition.size());
markovAutomaton = nullptr;
}

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

@ -87,73 +87,3 @@ TEST(GraphTest, PerformProb01MinMax) {
mdp2 = nullptr;
}
TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
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_WARN(logger, "Computing SCC decomposition of crowds/crowds20_5...");
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition(*dtmc);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1290297ull);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of crowds/crowds20_5...");
storm::storage::SparseMatrix<double> sccDependencyGraph(std::move(dtmc->extractPartitionDependencyGraph(sccDecomposition)));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1371253ull);
dtmc = nullptr;
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", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8...");
sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc2);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1279673ull);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8...");
sccDependencyGraph = std::move(dtmc2->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getEntryCount(), 1535367ull);
dtmc2 = nullptr;
storm::parser::AutoParser<double> parser3(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6...");
sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 146844ull);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6...");
sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getEntryCount(), 489918ull);
mdp = nullptr;
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", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6...");
sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp2);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 2611ull);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6...");
sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getEntryCount(), 7888ull);
mdp2 = nullptr;
}

48
test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
View File

@ -0,0 +1,48 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
TEST(StronglyConnectedComponentDecomposition, Crowds) {
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>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
ASSERT_EQ(sccDecomposition.size(), 1290297ull);
dtmc = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", "");
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*dtmc));
ASSERT_EQ(sccDecomposition.size(), 1279673ull);
dtmc = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
ASSERT_EQ(sccDecomposition.size(), 146844ull);
mdp = nullptr;
}
TEST(StronglyConnectedComponentDecomposition, Consensus) {
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*mdp));
ASSERT_EQ(sccDecomposition.size(), 2611ull);
mdp = nullptr;
}
Write Preview
Loading…
Cancel
Save