Browse Source

Test case for SEQ bug

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
f1c91d9280
  1. 8
      resources/examples/testfiles/dft/seq6.dft
  2. 2
      src/test/storm-dft/api/DftModelCheckerTest.cpp

8
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";

2
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<double>());
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);

Loading…
Cancel
Save