Added more DFT tests

resources/examples/testfiles/dft/fdep.dft

@@ -0,0 +1,8 @@
+toplevel "System";
+"System" or "Power" "Machine";
+"Power" fdep "B_Power" "P" "B";
+"Machine" or "P" "B";
+
+"B_Power" lambda=0.5 dorm=0;
+"P" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0.5;

resources/examples/testfiles/dft/fdep2.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C";
+"F" fdep "B" "C";
+"B" lambda=0.5 dorm=0;
+"C" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/fdep3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C" "F";
+"F" fdep "B" "C";
+"B" lambda=0.4 dorm=0;
+"C" lambda=0.8 dorm=0;

resources/examples/testfiles/dft/fdep4.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" or "F" "B";
+"F" fdep "E" "C" "D";
+"B" wsp "C" "D";
+"C" lambda=1 dorm=0;
+"D" lambda=1 dorm=0.5;
+"E" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/fdep5.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "B" "C" "D" "E";
+"F" fdep "B" "C" "D";
+"B" lambda=0.5 dorm=0;
+"C" lambda=0.5 dorm=0;
+"D" lambda=0.5 dorm=0;
+"E" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/or.dft

@@ -0,0 +1,4 @@
+toplevel "A";
+"A" or "B" "C";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/pand.dft

@@ -0,0 +1,4 @@
+toplevel "A";
+"A" pand "B" "C";
+"B" lambda=0.4 dorm=0.3;
+"C" lambda=0.2 dorm=0.3;

resources/examples/testfiles/dft/pdep.dft

@@ -0,0 +1,12 @@
+// From Junges2015
+// Example 3.19
+
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/pdep2.dft

@@ -0,0 +1,9 @@
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S" "MB";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/pdep3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C" "F";
+"F" pdep=0.3 "B" "C";
+"B" lambda=0.4 dorm=0;
+"C" lambda=0.8 dorm=0;

resources/examples/testfiles/dft/pdep4.dft

@@ -0,0 +1,7 @@
+toplevel "SF";
+"SF" pand "S" "A" "B";
+"PDEP" pdep=0.2 "S" "A" "B";
+
+"S" lambda=0.5 dorm=0;
+"A" lambda=0.5 dorm=0;
+"B" lambda=0.5 dorm=0;

resources/examples/testfiles/dft/por.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" por "B" "C" "D";
+"B" lambda=0.4 dorm=0.0;
+"C" lambda=0.2 dorm=0.0;
+"D" lambda=0.2 dorm=0.0;

resources/examples/testfiles/dft/seq.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" and "B" "C";
+"X" seq "B" "C";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq2.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "B" "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq3.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" and "C" "D";
+"X" seq "B" "C" "D";
+"B" lambda=0.5 dorm=0.3;
+"C" lambda=0.5 dorm=0.3;
+"D" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq4.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "T1" "B3";
+"T1" or "B1" "B2";
+"X" seq "B1" "B2" "B3";
+"B1" lambda=0.5 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;

resources/examples/testfiles/dft/seq5.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "T1" "T2";
+"T1" pand "B1" "B2"; 
+"T2" pand "B3" "B4";
+"X" seq "B4" "B3";
+"B1" lambda=0.7 dorm=0.3;
+"B2" lambda=0.5 dorm=0.3;
+"B3" lambda=0.5 dorm=0.3;
+"B4" lambda=0.7 dorm=0.3;

resources/examples/testfiles/dft/spare.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" wsp "I" "M";
+"I" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare2.dft

@@ -0,0 +1,8 @@
+toplevel "A";
+"A" or "B" "C";
+"B" wsp "I" "J";
+"C" wsp "M" "J";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare3.dft

@@ -0,0 +1,10 @@
+toplevel "A";
+"A" or "B" "C" "D";
+"B" wsp "I" "M";
+"C" wsp "J" "M";
+"D" wsp "K" "M";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare4.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "B" "C";
+"B" wsp "I" "J" "K";
+"C" wsp "M" "J";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+"M" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/spare5.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" wsp "I" "B";
+"B" or "C" "J";
+"C" or "K" "L";
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0;
+"K" lambda=0.5 dorm=0;
+"L" lambda=0.5 dorm=0;
+

resources/examples/testfiles/dft/spare6.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" or "I" "B";
+"B" wsp "J" "M";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=0.5 dorm=0.5;
+"M" lambda=0.5 dorm=0.5;
+

resources/examples/testfiles/dft/spare7.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" wsp "K" "J" "I";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=1 dorm=0.5;
+"K" lambda=0.5 dorm=0.5;

resources/examples/testfiles/dft/spare8.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" wsp "I" "B";
+"B" wsp "J" "K";
+"I" lambda=0.5 dorm=0.3;
+"J" lambda=0.5 dorm=0.3;
+"K" lambda=0.5 dorm=0.3;
+

resources/examples/testfiles/dft/voting.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 1of3 "B" "C" "D";
+"B" lambda=0.1 dorm=0;
+"C" lambda=0.2 dorm=0;
+"D" lambda=0.3 dorm=0;

resources/examples/testfiles/dft/voting2.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 1of3 "B" "C" "D";
+"B" lambda=0.3 dorm=0;
+"C" lambda=0.4 dorm=0;
+"D" lambda=1 dorm=0;

resources/examples/testfiles/dft/voting3.dft

@@ -0,0 +1,5 @@
+toplevel "A";
+"A" 2of3 "B" "C" "D";
+"B" lambda=0.3 dorm=0;
+"C" lambda=0.4 dorm=0;
+"D" lambda=1 dorm=0;

resources/examples/testfiles/dft/voting4.dft

@@ -0,0 +1,6 @@
+toplevel "A";
+"A" 2of3 "B" "C" "D";
+"D" or "E";
+"B" lambda=1 dorm=0.0;
+"C" lambda=1 dorm=0.0;
+"E" lambda=1 dorm=0.0;

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

@@ -85,7 +85,87 @@ namespace {
 
     TYPED_TEST(DftModelCheckerTest, AndMTTF) {
         double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
-        EXPECT_FLOAT_EQ(result, 3.0);
+        EXPECT_FLOAT_EQ(result, 3);
+    }
+
+    TYPED_TEST(DftModelCheckerTest, OrMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/or.dft");
+        EXPECT_FLOAT_EQ(result, 1);
+    }
+
+    TYPED_TEST(DftModelCheckerTest, VotingMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting.dft");
+        EXPECT_FLOAT_EQ(result, 5/3);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft");
+        EXPECT_FLOAT_EQ(result, 10/17);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft");
+        EXPECT_FLOAT_EQ(result, 1.73562);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft");
+        EXPECT_FLOAT_EQ(result, 5/6);
+    }
+
+    TYPED_TEST(DftModelCheckerTest, PandMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
+        EXPECT_EQ(result, storm::utility::infinity<double>());
+    }
+
+    TYPED_TEST(DftModelCheckerTest, PorMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/por.dft");
+        EXPECT_EQ(result, storm::utility::infinity<double>());
+    }
+
+    TYPED_TEST(DftModelCheckerTest, FdepMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
+        EXPECT_FLOAT_EQ(result, 2/3);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft");
+        EXPECT_FLOAT_EQ(result, 2);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft");
+        EXPECT_FLOAT_EQ(result, 2.5);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
+        EXPECT_FLOAT_EQ(result, 1);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
+        EXPECT_FLOAT_EQ(result, 3);
+    }
+
+    TYPED_TEST(DftModelCheckerTest, PdepMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
+        EXPECT_FLOAT_EQ(result, 8/3);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
+        EXPECT_FLOAT_EQ(result, 38/15);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
+        EXPECT_FLOAT_EQ(result, 2.79167);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
+        EXPECT_EQ(result, storm::utility::infinity<double>());
+    }
+    TYPED_TEST(DftModelCheckerTest, SpareMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare.dft");
+        EXPECT_FLOAT_EQ(result, 3.53846);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft");
+        EXPECT_FLOAT_EQ(result, 1.86957);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft");
+        EXPECT_FLOAT_EQ(result, 1.27273);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft");
+        EXPECT_FLOAT_EQ(result, 4.8459);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
+        EXPECT_FLOAT_EQ(result, 8/3);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft");
+        EXPECT_FLOAT_EQ(result, 1.4);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft");
+        EXPECT_FLOAT_EQ(result, 3.67333);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft");
+        EXPECT_FLOAT_EQ(result, 4.78846); // DFTCalc says 4.33779
+    }
+    TYPED_TEST(DftModelCheckerTest, SeqMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");
+        EXPECT_FLOAT_EQ(result, 4);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft");
+        EXPECT_FLOAT_EQ(result, 6);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft");
+        EXPECT_FLOAT_EQ(result, 6);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft");
+        EXPECT_FLOAT_EQ(result, 6);
+        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft");
+        EXPECT_EQ(result, storm::utility::infinity<double>());
     }
 
 }