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

SmgRpatlModelCheckerTest.cpp: google tests for MSECs

main
Fabian Russold 1 year ago
committed by sp
parent
1e40b9e5a3
commit
3b0eeb1e88
1 changed files with 134 additions and 0 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. 134
      src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp

134
src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp
View File

@ -426,6 +426,73 @@ namespace {
storm::storage::MaximalEndComponentDecomposition<ValueType> MSEC = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, backwardTransitions);
// testing MSEC
// =====================================================
ASSERT_TRUE(MSEC.size() == 3);
storm::storage::MaximalEndComponent const& mec1 = MSEC[0];
if (mec1.containsState(0)) {
ASSERT_TRUE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(2));
ASSERT_FALSE(mec1.containsState(3));
}
else if (mec1.containsState(2)) {
ASSERT_FALSE(mec1.containsState(0));
ASSERT_FALSE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(3));
}
else if (mec1.containsState(3)) {
ASSERT_FALSE(mec1.containsState(0));
ASSERT_FALSE(mec1.containsState(1));
ASSERT_FALSE(mec1.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
storm::storage::MaximalEndComponent const& mec2 = MSEC[1];
if (mec2.containsState(0)) {
ASSERT_TRUE(mec2.containsState(1));
ASSERT_FALSE(mec2.containsState(2));
ASSERT_FALSE(mec2.containsState(3));
}
else if (mec2.containsState(2)) {
ASSERT_FALSE(mec2.containsState(0));
ASSERT_FALSE(mec2.containsState(1));
ASSERT_FALSE(mec2.containsState(3));
}
else if (mec2.containsState(3)) {
ASSERT_FALSE(mec2.containsState(0));
ASSERT_FALSE(mec2.containsState(1));
ASSERT_FALSE(mec2.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
storm::storage::MaximalEndComponent const& mec3 = MSEC[2];
if (mec3.containsState(0)) {
ASSERT_TRUE(mec3.containsState(1));
ASSERT_FALSE(mec3.containsState(2));
ASSERT_FALSE(mec3.containsState(3));
}
else if (mec3.containsState(2)) {
ASSERT_FALSE(mec3.containsState(0));
ASSERT_FALSE(mec3.containsState(1));
ASSERT_FALSE(mec3.containsState(3));
}
else if (mec3.containsState(3)) {
ASSERT_FALSE(mec3.containsState(0));
ASSERT_FALSE(mec3.containsState(1));
ASSERT_FALSE(mec3.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
// =====================================================
// reducing the choiceValuesU
size_t i = 0;
auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) {
@ -471,6 +538,73 @@ namespace {
MSEC = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, backwardTransitions);
// testing MSEC
// =====================================================
ASSERT_TRUE(MSEC.size() == 3);
storm::storage::MaximalEndComponent const& mec4 = MSEC[0];
if (mec4.containsState(0)) {
ASSERT_TRUE(mec4.containsState(1));
ASSERT_FALSE(mec4.containsState(2));
ASSERT_FALSE(mec4.containsState(3));
}
else if (mec4.containsState(2)) {
ASSERT_FALSE(mec4.containsState(0));
ASSERT_FALSE(mec4.containsState(1));
ASSERT_FALSE(mec4.containsState(3));
}
else if (mec4.containsState(3)) {
ASSERT_FALSE(mec4.containsState(0));
ASSERT_FALSE(mec4.containsState(1));
ASSERT_FALSE(mec4.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
storm::storage::MaximalEndComponent const& mec5 = MSEC[1];
if (mec5.containsState(0)) {
ASSERT_TRUE(mec5.containsState(1));
ASSERT_FALSE(mec5.containsState(2));
ASSERT_FALSE(mec5.containsState(3));
}
else if (mec5.containsState(2)) {
ASSERT_FALSE(mec5.containsState(0));
ASSERT_FALSE(mec5.containsState(1));
ASSERT_FALSE(mec5.containsState(3));
}
else if (mec5.containsState(3)) {
ASSERT_FALSE(mec5.containsState(0));
ASSERT_FALSE(mec5.containsState(1));
ASSERT_FALSE(mec5.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
storm::storage::MaximalEndComponent const& mec6 = MSEC[2];
if (mec6.containsState(0)) {
ASSERT_TRUE(mec6.containsState(1));
ASSERT_FALSE(mec6.containsState(2));
ASSERT_FALSE(mec6.containsState(3));
}
else if (mec6.containsState(2)) {
ASSERT_FALSE(mec6.containsState(0));
ASSERT_FALSE(mec6.containsState(1));
ASSERT_FALSE(mec6.containsState(3));
}
else if (mec6.containsState(3)) {
ASSERT_FALSE(mec6.containsState(0));
ASSERT_FALSE(mec6.containsState(1));
ASSERT_FALSE(mec6.containsState(2));
}
else {
// This case must never happen
ASSERT_TRUE(false);
}
// =====================================================
// reducing the choiceValuesU
i = 0;
new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) {

Write Preview
Loading…
Cancel
Save