Added tests for mutex

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;

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;

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;

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>());
     }
 
 }