diff --git a/resources/examples/testfiles/dft/fdep.dft b/resources/examples/testfiles/dft/fdep.dft new file mode 100644 index 000000000..e597c46ce --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/fdep2.dft b/resources/examples/testfiles/dft/fdep2.dft new file mode 100644 index 000000000..a444ed4be --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/fdep3.dft b/resources/examples/testfiles/dft/fdep3.dft new file mode 100644 index 000000000..3815c9973 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/fdep4.dft b/resources/examples/testfiles/dft/fdep4.dft new file mode 100644 index 000000000..7e3c5642a --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/fdep5.dft b/resources/examples/testfiles/dft/fdep5.dft new file mode 100644 index 000000000..2e0625dfb --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/or.dft b/resources/examples/testfiles/dft/or.dft new file mode 100644 index 000000000..b1003da11 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/pand.dft b/resources/examples/testfiles/dft/pand.dft new file mode 100644 index 000000000..d752517b4 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/pdep.dft b/resources/examples/testfiles/dft/pdep.dft new file mode 100644 index 000000000..f8cb0382b --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/pdep2.dft b/resources/examples/testfiles/dft/pdep2.dft new file mode 100644 index 000000000..ab1c7a9b8 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/pdep3.dft b/resources/examples/testfiles/dft/pdep3.dft new file mode 100644 index 000000000..a9a73f472 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/pdep4.dft b/resources/examples/testfiles/dft/pdep4.dft new file mode 100644 index 000000000..eace91847 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/por.dft b/resources/examples/testfiles/dft/por.dft new file mode 100644 index 000000000..020687f62 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/seq.dft b/resources/examples/testfiles/dft/seq.dft new file mode 100644 index 000000000..8f5459fd2 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/seq2.dft b/resources/examples/testfiles/dft/seq2.dft new file mode 100644 index 000000000..408d4c26d --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/seq3.dft b/resources/examples/testfiles/dft/seq3.dft new file mode 100644 index 000000000..b22b9e8b6 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/seq4.dft b/resources/examples/testfiles/dft/seq4.dft new file mode 100644 index 000000000..60bf149af --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/seq5.dft b/resources/examples/testfiles/dft/seq5.dft new file mode 100644 index 000000000..77b13ddeb --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/spare.dft b/resources/examples/testfiles/dft/spare.dft new file mode 100644 index 000000000..4c5d44ff4 --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare2.dft b/resources/examples/testfiles/dft/spare2.dft new file mode 100644 index 000000000..21b40cf73 --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare3.dft b/resources/examples/testfiles/dft/spare3.dft new file mode 100644 index 000000000..ba0ac01d4 --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare4.dft b/resources/examples/testfiles/dft/spare4.dft new file mode 100644 index 000000000..a217c6e43 --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare5.dft b/resources/examples/testfiles/dft/spare5.dft new file mode 100644 index 000000000..0cd15bf0e --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare6.dft b/resources/examples/testfiles/dft/spare6.dft new file mode 100644 index 000000000..d5f2b270b --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/spare7.dft b/resources/examples/testfiles/dft/spare7.dft new file mode 100644 index 000000000..a16429e6f --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/spare8.dft b/resources/examples/testfiles/dft/spare8.dft new file mode 100644 index 000000000..c67eaf022 --- /dev/null +++ b/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; + diff --git a/resources/examples/testfiles/dft/voting.dft b/resources/examples/testfiles/dft/voting.dft new file mode 100644 index 000000000..5c648d424 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/voting2.dft b/resources/examples/testfiles/dft/voting2.dft new file mode 100644 index 000000000..9cdf299f3 --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/voting3.dft b/resources/examples/testfiles/dft/voting3.dft new file mode 100644 index 000000000..107408fce --- /dev/null +++ b/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; diff --git a/resources/examples/testfiles/dft/voting4.dft b/resources/examples/testfiles/dft/voting4.dft new file mode 100644 index 000000000..412df12e5 --- /dev/null +++ b/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; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index a2fdd4610..8c57795d6 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/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()); + } + + TYPED_TEST(DftModelCheckerTest, PorMTTF) { + double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/por.dft"); + EXPECT_EQ(result, storm::utility::infinity()); + } + + 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()); + } + 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()); } }