diff --git a/resources/examples/testfiles/dft/cyclic.dft b/resources/examples/testfiles/dft/cyclic.dft new file mode 100644 index 000000000..b683dcf42 --- /dev/null +++ b/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; \ No newline at end of file diff --git a/resources/examples/testfiles/dft/seqChild.dft b/resources/examples/testfiles/dft/seqChild.dft new file mode 100644 index 000000000..ad68072c8 --- /dev/null +++ b/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; diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index 4a19aed08..dfa7ad769 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -20,4 +20,14 @@ namespace { EXPECT_EQ(2ul, dft->nrBasicElements()); EXPECT_TRUE(storm::api::isWellFormed(*dft)); } + + TEST(DftParserTest, CatchCycles) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/cyclic.dft"; + EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); + } + + TEST(DftParserTest, CatchSeqChildren) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/seqChild.dft"; + EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); + } }