diff --git a/src/test/storm-dft/api/DftApiTest.cpp b/src/test/storm-dft/api/DftApiTest.cpp deleted file mode 100644 index 93dffb5b8..000000000 --- a/src/test/storm-dft/api/DftApiTest.cpp +++ /dev/null @@ -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> - { - 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> dft = storm::api::loadDFTGalileo(stream.str()); - - std::string property = "Tmin=? [F \"failed\"]"; - std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); - - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, analysisConfig.useSR, analysisConfig.useMod, analysisConfig.useDC); - double result = boost::get(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> dft = storm::api::loadDFTGalileo(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/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp new file mode 100644 index 000000000..a2fdd4610 --- /dev/null +++ b/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 + 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> dft = storm::api::loadDFTGalileo(file); + std::string property = "Tmin=? [F \"failed\"]"; + std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, config.useDC); + return boost::get(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); + } + +} diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp new file mode 100644 index 000000000..48a621ac1 --- /dev/null +++ b/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> dft = storm::api::loadDFTGalileo(file); + } + +}