Browse Source

Skip a test if LTL model checking is not available.

tempestpy_adaptions
Tim Quatmann 3 years ago
committed by Stefan Pranger
parent
commit
3a3587370e
  1. 5
      src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp

5
src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp

@ -351,6 +351,7 @@ namespace {
}
TYPED_TEST(MarkovAutomatonCslModelCheckerTest, LtlSimple) {
#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
std::string formulasString = "Pmax=? [X X s=3]";
formulasString += "; Pmax=? [X X G s>2]";
formulasString += "; Pmin=? [X X G s>2]";
@ -382,6 +383,8 @@ namespace {
} else {
EXPECT_FALSE(checker->canHandle(tasks[0]));
}
#else
GTEST_SKIP();
#endif
}
}
Loading…
Cancel
Save