Browse Source

Added tests for mutex

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
9ce3f9f58d
  1. 8
      resources/examples/testfiles/dft/mutex.dft
  2. 7
      resources/examples/testfiles/dft/mutex2.dft
  3. 6
      resources/examples/testfiles/dft/mutex3.dft
  4. 7
      src/test/storm-dft/api/DftModelCheckerTest.cpp

8
resources/examples/testfiles/dft/mutex.dft

@ -0,0 +1,8 @@
toplevel "T";
"T" or "A" "B";
"B" and "B1" "B2";
"M" seq "C" "B";
"A" lambda=2 dorm=1;
"B1" lambda=4 dorm=1;
"B2" lambda=5 dorm=1;
"C" lambda=0 dorm=1;

7
resources/examples/testfiles/dft/mutex2.dft

@ -0,0 +1,7 @@
toplevel "T";
"T" or "B";
"B" and "B1" "B2";
"M" seq "C" "B";
"B1" lambda=4 dorm=1;
"B2" lambda=5 dorm=1;
"C" lambda=0 dorm=1;

6
resources/examples/testfiles/dft/mutex3.dft

@ -0,0 +1,6 @@
toplevel "T";
"T" and "A" "B" "C";
"M" mutex "B" "C";
"A" lambda=2 dorm=1;
"B" lambda=4 dorm=1;
"C" lambda=5 dorm=1;

7
src/test/storm-dft/api/DftModelCheckerTest.cpp

@ -198,6 +198,13 @@ 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/mutex.dft");
EXPECT_FLOAT_EQ(result, 0.5);
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft");
EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
}
}
Loading…
Cancel
Save