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

Added functional tests for MEC decomposition. 

Former-commit-id: 66b1265ebb
main
dehnert 12 years ago
parent
f32853b6aa
commit
e80bb0caa5
3 changed files with 111 additions and 2 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. 5
      src/storage/MaximalEndComponentDecomposition.cpp
  2. 2
      src/storage/PartialScheduler.cpp
  3. 106
      test/functional/storage/MaximalEndComponentDecompositionTest.cpp

5
src/storage/MaximalEndComponentDecomposition.cpp
View File

@ -70,7 +70,10 @@ namespace storm {
// Get an SCC decomposition of the current MEC candidate.
StronglyConnectedComponentDecomposition<ValueType> sccs(model, mec, true);
mecChanged |= sccs.size() > 1;
// 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();
// 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) {

2
src/storage/PartialScheduler.cpp
View File

@ -9,7 +9,7 @@ namespace storm {
}
bool PartialScheduler::isChoiceDefined(uint_fast64_t state) const {
return stateToChoiceMapping.find(state) != choices.end();
return stateToChoiceMapping.find(state) != stateToChoiceMapping.end();
}
uint_fast64_t PartialScheduler::getChoice(uint_fast64_t state) const {

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

@ -0,0 +1,106 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
TEST(MaximalEndComponentDecomposition, FullSystem) {
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::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
ASSERT_EQ(2, 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(3)) {
ASSERT_TRUE(mec1.containsState(8));
ASSERT_TRUE(mec1.containsState(9));
ASSERT_TRUE(mec1.containsState(10));
ASSERT_FALSE(mec1.containsState(0));
ASSERT_FALSE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(2));
ASSERT_FALSE(mec1.containsState(4));
ASSERT_FALSE(mec1.containsState(5));
ASSERT_FALSE(mec1.containsState(6));
ASSERT_FALSE(mec1.containsState(7));
} else 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 either 3 or 4.
ASSERT_TRUE(false);
}
storm::storage::MaximalEndComponent const& mec2 = mecDecomposition[1];
if (mec2.containsState(3)) {
ASSERT_TRUE(mec2.containsState(8));
ASSERT_TRUE(mec2.containsState(9));
ASSERT_TRUE(mec2.containsState(10));
ASSERT_FALSE(mec2.containsState(0));
ASSERT_FALSE(mec2.containsState(1));
ASSERT_FALSE(mec2.containsState(2));
ASSERT_FALSE(mec2.containsState(4));
ASSERT_FALSE(mec2.containsState(5));
ASSERT_FALSE(mec2.containsState(6));
ASSERT_FALSE(mec2.containsState(7));
} else if (mec2.containsState(4)) {
ASSERT_TRUE(mec2.containsState(5));
ASSERT_TRUE(mec2.containsState(6));
ASSERT_TRUE(mec2.containsState(7));
ASSERT_FALSE(mec2.containsState(0));
ASSERT_FALSE(mec2.containsState(1));
ASSERT_FALSE(mec2.containsState(2));
ASSERT_FALSE(mec2.containsState(3));
ASSERT_FALSE(mec2.containsState(8));
ASSERT_FALSE(mec2.containsState(9));
ASSERT_FALSE(mec2.containsState(10));
} else {
// This case must never happen as the only two existing MECs contain either 3 or 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", "", "");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
storm::storage::BitVector subsystem(markovAutomaton->getNumberOfStates(), true);
subsystem.set(7, false);
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton, subsystem));
ASSERT_EQ(1, mecDecomposition.size());
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));
ASSERT_TRUE(mec1.containsState(10));
ASSERT_FALSE(mec1.containsState(0));
ASSERT_FALSE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(2));
ASSERT_FALSE(mec1.containsState(4));
ASSERT_FALSE(mec1.containsState(5));
ASSERT_FALSE(mec1.containsState(6));
ASSERT_FALSE(mec1.containsState(7));
} else {
// This case must never happen as the only two existing MEC contains 3.
ASSERT_TRUE(false);
}
}
Write Preview
Loading…
Cancel
Save