diff --git a/resources/examples/testfiles/dft/seq6.dft b/resources/examples/testfiles/dft/seq6.dft new file mode 100644 index 000000000..633d399ab --- /dev/null +++ b/resources/examples/testfiles/dft/seq6.dft @@ -0,0 +1,8 @@ +toplevel "T"; +"T" wsp "A" "C"; +"A" lambda=1e-4 dorm=1; +"C" lambda=5e-5 dorm=0; +"seq" seq "OR" "C"; +"OR" or "F"; +"F" lambda=0 dorm=0; +"FDEP" fdep "A" "F"; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 73550a3af..2600252a5 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -194,6 +194,8 @@ namespace { EXPECT_FLOAT_EQ(result, 6); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft"); EXPECT_EQ(result, storm::utility::infinity()); + result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft"); + EXPECT_FLOAT_EQ(result, 30000); result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft"); EXPECT_FLOAT_EQ(result, 0.5);