Started on DFT regression tests

resources/examples/testfiles/dft/and.dft

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

src/test/CMakeLists.txt

@@ -1,2 +1,3 @@
 add_subdirectory(storm)
-add_subdirectory(storm-pars)
+add_subdirectory(storm-pars)
+add_subdirectory(storm-dft)

src/test/storm-dft/CMakeLists.txt

@@ -0,0 +1,23 @@
+# Base path for test files
+set(STORM_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/src/test/storm-dft")
+
+# Test Sources
+file(GLOB_RECURSE ALL_FILES ${STORM_TESTS_BASE_PATH}/*.h ${STORM_TESTS_BASE_PATH}/*.cpp)
+
+register_source_groups_from_filestructure("${ALL_FILES}" test)
+
+# Note that the tests also need the source files, except for the main file
+include_directories(${GTEST_INCLUDE_DIR})
+
+foreach (testsuite api)
+
+	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
+      add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
+	  target_link_libraries(test-dft-${testsuite} storm-dft)
+	  target_link_libraries(test-dft-${testsuite} ${STORM_TEST_LINK_LIBRARIES})
+
+	  add_dependencies(test-dft-${testsuite} test-resources)
+	  add_test(NAME run-test-dft-${testsuite} COMMAND $<TARGET_FILE:test-dft-${testsuite}>)
+      add_dependencies(tests test-dft-${testsuite})
+
+endforeach ()

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

@@ -0,0 +1,63 @@
+#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/storm-test.cpp

@@ -0,0 +1,8 @@
+#include "gtest/gtest.h"
+#include "storm-dft/settings/DftSettings.h"
+
+int main(int argc, char **argv) {
+  storm::settings::initializeDftSettings("Storm-dft (Functional) Testing Suite", "test-dft");
+  ::testing::InitGoogleTest(&argc, argv);
+  return RUN_ALL_TESTS();
+}