Test case for symmetry reduction

resources/examples/testfiles/dft/symmetry6.dft

@@ -0,0 +1,24 @@
+toplevel "A";
+"A" or "B" "C";
+"B" and "J" "K" "L";
+"J" or "J1" "J2";
+"K" or "K1" "K2";
+"L" or "L1" "L2";
+"C" or "M" "N";
+"M" and "M1" "M2" "M3" "M4";
+"N" and "N1" "N2" "N3" "N4";
+"J1" lambda=0.5 dorm=0;
+"J2" lambda=0.5 dorm=0;
+"K1" lambda=0.5 dorm=0;
+"K2" lambda=0.5 dorm=0;
+"L1" lambda=0.5 dorm=0;
+"L2" lambda=0.5 dorm=0;
+"M1" lambda=0.5 dorm=0;
+"M2" lambda=0.5 dorm=0;
+"M3" lambda=1 dorm=0;
+"M4" lambda=1 dorm=0;
+"N1" lambda=0.5 dorm=0;
+"N2" lambda=0.5 dorm=0;
+"N3" lambda=1 dorm=0;
+"N4" lambda=1 dorm=0;
+

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

@@ -86,7 +86,7 @@ namespace {
             return boost::get<double>(results[0]);
         }
 
-        double analyzeReliability(std::string const &file, double bound) {
+        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\"]";
@@ -221,6 +221,13 @@ namespace {
         EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
     }
 
+    TYPED_TEST(DftModelCheckerTest, Symmetry) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft");
+        EXPECT_FLOAT_EQ(result, 1.373226284);
+        result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1.0);
+        EXPECT_FLOAT_EQ(result, 0.3421934224);
+    }
+
     TYPED_TEST(DftModelCheckerTest, HecsReliability) {
         double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
         EXPECT_FLOAT_EQ(result, 0.00021997582);