Use different configurations in DFT tests

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

@@ -1,63 +0,0 @@
-#include "gtest/gtest.h"
-#include "storm-config.h"
-
-#include "storm-dft/api/storm-dft.h"
-
-namespace {
-
-    // Base holding information about test example
-    struct DftExample {
-        std::string file;
-        double expectedValue;
-    };
-    struct DftAnalysisConfig {
-        DftExample example;
-        bool useSR;
-        bool useMod;
-        bool useDC;
-    };
-
-    // Base test for regression test
-    class DftAnalysisTestCase : public ::testing::TestWithParam<std::tuple<DftExample, bool, bool, bool>>
-    {
-    protected:
-        DftAnalysisConfig analysisConfig {
-                std::get<0>(GetParam()),
-                std::get<1>(GetParam()),
-                std::get<2>(GetParam()),
-                std::get<3>(GetParam())
-        };
-    };
-
-    TEST_P(DftAnalysisTestCase, AnalyzeMTTF) {
-        std::stringstream stream;
-        stream << STORM_TEST_RESOURCES_DIR << "/dft/" << analysisConfig.example.file << ".dft";
-        std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(stream.str());
-
-        std::string property = "Tmin=? [F \"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, analysisConfig.useSR, analysisConfig.useMod, analysisConfig.useDC);
-        double result = boost::get<double>(results[0]);
-        EXPECT_FLOAT_EQ(result, analysisConfig.example.expectedValue);
-    }
-
-    TEST(DftApiTest, LoadFromGalileo) {
-        std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.dft";
-        std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
-    }
-
-    INSTANTIATE_TEST_CASE_P(RegularPolygon, DftAnalysisTestCase, ::testing::Combine(
-            testing::Values(
-                DftExample {"and", 3.0}
-            ),
-            ::testing::Bool(), // useSR
-            ::testing::Bool(), // useMod
-            ::testing::Bool() // useDC
-        )
-    );
-
-
-    TEST(DftApiTest, AnalyzeMTTF) {
-    }
-}

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

@@ -0,0 +1,91 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-dft/api/storm-dft.h"
+
+namespace {
+
+    // Configurations for DFT analysis
+    struct DftAnalysisConfig {
+        bool useSR;
+        bool useMod;
+        bool useDC;
+    };
+
+    class NoOptimizationsConfig {
+    public:
+        typedef double ValueType;
+        static DftAnalysisConfig createConfig() {
+            return DftAnalysisConfig {false, false, false};
+        }
+    };
+    class DontCareConfig {
+    public:
+        typedef double ValueType;
+        static DftAnalysisConfig createConfig() {
+            return DftAnalysisConfig {false, false, true};
+        }
+    };
+    class ModularisationConfig {
+    public:
+        typedef double ValueType;
+        static DftAnalysisConfig createConfig() {
+            return DftAnalysisConfig {false, true, false};
+        }
+    };
+    class SymmetryReductionConfig {
+    public:
+        typedef double ValueType;
+        static DftAnalysisConfig createConfig() {
+            return DftAnalysisConfig {true, false, false};
+        }
+    };
+    class AllOptimizationsConfig {
+    public:
+        typedef double ValueType;
+        static DftAnalysisConfig createConfig() {
+            return DftAnalysisConfig {true, true, true};
+        }
+    };
+
+    // General base class for testing of DFT model checking
+    template<typename TestType>
+    class DftModelCheckerTest : public ::testing::Test {
+    public:
+        typedef typename TestType::ValueType ValueType;
+
+        DftModelCheckerTest() : config(TestType::createConfig()) {
+        }
+
+        DftAnalysisConfig const& getConfig() const {
+            return config;
+        }
+
+        double analyzeMTTF(std::string const& file) {
+            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
+            std::string property = "Tmin=? [F \"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);
+            return boost::get<double>(results[0]);
+        }
+
+    private:
+        DftAnalysisConfig config;
+    };
+
+    typedef ::testing::Types<
+            NoOptimizationsConfig,
+            DontCareConfig,
+            ModularisationConfig,
+            SymmetryReductionConfig,
+            AllOptimizationsConfig
+        > TestingTypes;
+
+    TYPED_TEST_CASE(DftModelCheckerTest, TestingTypes);
+
+    TYPED_TEST(DftModelCheckerTest, AndMTTF) {
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
+        EXPECT_FLOAT_EQ(result, 3.0);
+    }
+
+}

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

@@ -0,0 +1,13 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "storm-dft/api/storm-dft.h"
+
+namespace {
+
+    TEST(DftParserTest, LoadFromGalileo) {
+        std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.dft";
+        std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
+    }
+
+}