Added test for hecs-DFT

resources/examples/testfiles/dft/hecs_2_2.dft

@@ -0,0 +1,40 @@
+toplevel "System";
+"System" or "System_1" "System_2";
+"System_1" or "PSF_1" "MSF_1" "BSF_1" "IF_1";
+"PSF_1" and "P_11" "P_12";
+"P_11" wsp "A_11" "A_1S";
+"P_12" wsp "A_12" "A_1S";
+"MSF_1" 3of5 "M_1_1" "M_1_2" "M_1_3" "M_1_4" "M_1_5";
+"BSF_1" and "BUS_11" "BUS_12";
+"IF_1" or "HW_1" "SW_1";
+"System_2" or "PSF_2" "MSF_2" "BSF_2" "IF_2";
+"PSF_2" and "P_21" "P_22";
+"P_21" wsp "A_21" "A_2S";
+"P_22" wsp "A_22" "A_2S";
+"MSF_2" 3of5 "M_2_1" "M_2_2" "M_2_3" "M_2_4" "M_2_5";
+"BSF_2" and "BUS_21" "BUS_22";
+"IF_2" or "HW_2" "SW_2";
+"A_11" lambda=1.0e-4 dorm=0;
+"A_12" lambda=1.0e-4 dorm=0;
+"A_1S" lambda=1.0e-4 dorm=0;
+"M_1_1" lambda=6.0e-5 dorm=0;
+"M_1_2" lambda=6.0e-5 dorm=0;
+"M_1_3" lambda=6.0e-5 dorm=0;
+"M_1_4" lambda=6.0e-5 dorm=0;
+"M_1_5" lambda=6.0e-5 dorm=0;
+"BUS_11" lambda=1.0e-6 dorm=0;
+"BUS_12" lambda=1.0e-6 dorm=0;
+"HW_1" lambda=5.0e-5 dorm=0;
+"SW_1" lambda=6.0e-5 dorm=0;
+"A_21" lambda=1.0e-4 dorm=0;
+"A_22" lambda=1.0e-4 dorm=0;
+"A_2S" lambda=1.0e-4 dorm=0;
+"M_2_1" lambda=6.0e-5 dorm=0;
+"M_2_2" lambda=6.0e-5 dorm=0;
+"M_2_3" lambda=6.0e-5 dorm=0;
+"M_2_4" lambda=6.0e-5 dorm=0;
+"M_2_5" lambda=6.0e-5 dorm=0;
+"BUS_21" lambda=1.0e-6 dorm=0;
+"BUS_22" lambda=1.0e-6 dorm=0;
+"HW_2" lambda=5.0e-5 dorm=0;
+"SW_2" lambda=6.0e-5 dorm=0;

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

@@ -71,6 +71,17 @@ namespace {
             return boost::get<double>(results[0]);
         }
 
+        double analyzeReliability(std::string const &file, double bound) {
+            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
+            std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(
+                    storm::api::parseProperties(property));
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(
+                    *dft, properties, config.useSR, config.useMod, config.useDC, false);
+            return boost::get<double>(results[0]);
+        }
+
     private:
         DftAnalysisConfig config;
     };
@@ -184,4 +195,8 @@ namespace {
         EXPECT_EQ(result, storm::utility::infinity<double>());
     }
 
+    TYPED_TEST(DftModelCheckerTest, HecsMTTF) {
+        double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
+        EXPECT_FLOAT_EQ(result, 0.00021997582);
+    }
 }