From 2ccd6d22dcf09ab54aed6c84cec8a37c80d182ff Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 11 Apr 2019 11:03:13 +0200
Subject: [PATCH] Added tests for mutex

---
 resources/examples/testfiles/dft/mutex.dft     | 8 ++++++++
 resources/examples/testfiles/dft/mutex2.dft    | 7 +++++++
 resources/examples/testfiles/dft/mutex3.dft    | 6 ++++++
 src/test/storm-dft/api/DftModelCheckerTest.cpp | 7 +++++++
 4 files changed, 28 insertions(+)
 create mode 100644 resources/examples/testfiles/dft/mutex.dft
 create mode 100644 resources/examples/testfiles/dft/mutex2.dft
 create mode 100644 resources/examples/testfiles/dft/mutex3.dft

diff --git a/resources/examples/testfiles/dft/mutex.dft b/resources/examples/testfiles/dft/mutex.dft
new file mode 100644
index 000000000..e3c081c4d
--- /dev/null
+++ b/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;
diff --git a/resources/examples/testfiles/dft/mutex2.dft b/resources/examples/testfiles/dft/mutex2.dft
new file mode 100644
index 000000000..951e2e039
--- /dev/null
+++ b/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;
diff --git a/resources/examples/testfiles/dft/mutex3.dft b/resources/examples/testfiles/dft/mutex3.dft
new file mode 100644
index 000000000..686469755
--- /dev/null
+++ b/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;
diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 790c29509..baf30dc02 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/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>());
     }
 
 }