Browse Source

Added tests for cycles and SEQ children

tempestpy_adaptions
Alexander Bork 6 years ago
parent
commit
2ab7c34b4d
  1. 5
      resources/examples/testfiles/dft/cyclic.dft
  2. 5
      resources/examples/testfiles/dft/seqChild.dft
  3. 10
      src/test/storm-dft/api/DftParserTest.cpp

5
resources/examples/testfiles/dft/cyclic.dft

@ -0,0 +1,5 @@
toplevel "A";
"A" and "B";
"B" and "C";
"C" and "A" "D";
"D" lambda=0.5 dorm=0.3;

5
resources/examples/testfiles/dft/seqChild.dft

@ -0,0 +1,5 @@
toplevel "A";
"A" and "B" "X";
"X" seq "B" "C";
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;

10
src/test/storm-dft/api/DftParserTest.cpp

@ -20,4 +20,14 @@ namespace {
EXPECT_EQ(2ul, dft->nrBasicElements()); EXPECT_EQ(2ul, dft->nrBasicElements());
EXPECT_TRUE(storm::api::isWellFormed(*dft)); EXPECT_TRUE(storm::api::isWellFormed(*dft));
} }
TEST(DftParserTest, CatchCycles) {
std::string file = STORM_TEST_RESOURCES_DIR "/dft/cyclic.dft";
EXPECT_THROW(storm::api::loadDFTGalileoFile<double>(file), storm::exceptions::WrongFormatException);
}
TEST(DftParserTest, CatchSeqChildren) {
std::string file = STORM_TEST_RESOURCES_DIR "/dft/seqChild.dft";
EXPECT_THROW(storm::api::loadDFTGalileoFile<double>(file), storm::exceptions::WrongFormatException);
}
} }
Loading…
Cancel
Save