From 2c9f6294a45a97ee90eca6e2fc97666dbf2e8ebe Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 16 Mar 2018 18:51:24 +0100
Subject: [PATCH] Started on DFT regression tests

---
 resources/examples/testfiles/dft/and.dft |  4 ++
 src/test/CMakeLists.txt                  |  3 +-
 src/test/storm-dft/CMakeLists.txt        | 23 +++++++++
 src/test/storm-dft/api/DftApiTest.cpp    | 63 ++++++++++++++++++++++++
 src/test/storm-dft/storm-test.cpp        |  8 +++
 5 files changed, 100 insertions(+), 1 deletion(-)
 create mode 100644 resources/examples/testfiles/dft/and.dft
 create mode 100644 src/test/storm-dft/CMakeLists.txt
 create mode 100644 src/test/storm-dft/api/DftApiTest.cpp
 create mode 100644 src/test/storm-dft/storm-test.cpp

diff --git a/resources/examples/testfiles/dft/and.dft b/resources/examples/testfiles/dft/and.dft
new file mode 100644
index 000000000..2b06cbe95
--- /dev/null
+++ b/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;
diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt
index d870d2b21..a693be0a0 100644
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@@ -1,2 +1,3 @@
 add_subdirectory(storm)
-add_subdirectory(storm-pars)
\ No newline at end of file
+add_subdirectory(storm-pars)
+add_subdirectory(storm-dft)
diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt
new file mode 100644
index 000000000..d461c2f9d
--- /dev/null
+++ b/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 ()
diff --git a/src/test/storm-dft/api/DftApiTest.cpp b/src/test/storm-dft/api/DftApiTest.cpp
new file mode 100644
index 000000000..93dffb5b8
--- /dev/null
+++ b/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) {
+    }
+}
diff --git a/src/test/storm-dft/storm-test.cpp b/src/test/storm-dft/storm-test.cpp
new file mode 100644
index 000000000..cf9106876
--- /dev/null
+++ b/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();
+}