From 2ebac862e27c75900130e44af3b0ca288d60df40 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 19 Mar 2019 14:46:25 +0100 Subject: [PATCH] Added test cases for DFT approximation --- .../examples/testfiles/dft/hecs_3_2_2_np.dft | 71 ++++++++++++ .../storm-dft/api/DftApproximationTest.cpp | 103 ++++++++++++++++++ 2 files changed, 174 insertions(+) create mode 100644 resources/examples/testfiles/dft/hecs_3_2_2_np.dft create mode 100644 src/test/storm-dft/api/DftApproximationTest.cpp diff --git a/resources/examples/testfiles/dft/hecs_3_2_2_np.dft b/resources/examples/testfiles/dft/hecs_3_2_2_np.dft new file mode 100644 index 000000000..f1c73a649 --- /dev/null +++ b/resources/examples/testfiles/dft/hecs_3_2_2_np.dft @@ -0,0 +1,71 @@ +toplevel "n58"; +"n58" 2of3 "n1" "n48" "n60"; +"n60" or "n233" "n308" "n263" "n57"; +"n308" wsp "n310" "n45"; +"n48" or "n235" "n287" "n271" "n64"; +"n287" wsp "n289" "n66"; +"n64" 3of5 "n248" "n254" "n252" "n255" "n246"; +"n254" or "n59" "n6"; +"n255" or "n24" "n70"; +"n246" or "n22" "n62"; +"n62" and "n6" "n70"; +"n263" wsp "n261" "n306" "n5"; +"n271" wsp "n269" "n302" "n34"; +"n57" 3of5 "n250" "n253" "n260" "n249" "n257"; +"n249" or "n8" "n0"; +"n257" or "n15" "n40"; +"n40" and "n0" "n23"; +"n250" or "n61" "n23"; +"n260" or "n46" "n0"; +"n248" or "n9" "n6"; +"n1" or "n234" "n296" "n267" "n68"; +"n267" wsp "n265" "n294" "n3"; +"n296" wsp "n298" "n69"; +"n68" 3of5 "n247" "n251" "n256" "n259" "n258"; +"n251" or "n47" "n53"; +"n247" or "n49" "n53"; +"n258" or "n20" "n4"; +"n4" and "n67" "n53"; +"n256" or "n10" "n67"; +"n253" or "n36" "n23"; +"n259" or "n78" "n67"; +"n252" or "n33" "n70"; +"n233" lambda=0.0010999999999999998 dorm=0.0; +"n45" lambda=1.0E-5 dorm=0.0; +"n310" lambda=2.0E-5 dorm=0.0; +"n235" lambda=0.0010999999999999998 dorm=0.0; +"n24" lambda=6.0E-4 dorm=0.0; +"n22" lambda=6.0E-4 dorm=0.0; +"n5" lambda=0.001 dorm=0.0; +"n306" lambda=0.002 dorm=0.0; +"n261" lambda=0.002 dorm=0.0; +"n34" lambda=0.001 dorm=0.0; +"n302" lambda=0.002 dorm=0.0; +"n8" lambda=6.0E-4 dorm=0.0; +"n15" lambda=6.0E-4 dorm=0.0; +"n61" lambda=6.0E-4 dorm=0.0; +"n269" lambda=0.002 dorm=0.0; +"n59" lambda=6.0E-4 dorm=0.0; +"n289" lambda=2.0E-5 dorm=0.0; +"n46" lambda=6.0E-4 dorm=0.0; +"n0" lambda=5.0E-4 dorm=0.0; +"n6" lambda=5.0E-4 dorm=0.0; +"n9" lambda=6.0E-4 dorm=0.0; +"n234" lambda=0.0010999999999999998 dorm=0.0; +"n3" lambda=0.001 dorm=0.0; +"n265" lambda=0.002 dorm=0.0; +"n298" lambda=2.0E-5 dorm=0.0; +"n47" lambda=6.0E-4 dorm=0.0; +"n49" lambda=6.0E-4 dorm=0.0; +"n53" lambda=5.0E-4 dorm=0.0; +"n10" lambda=6.0E-4 dorm=0.0; +"n23" lambda=5.0E-4 dorm=0.0; +"n36" lambda=6.0E-4 dorm=0.0; +"n78" lambda=6.0E-4 dorm=0.0; +"n67" lambda=5.0E-4 dorm=0.0; +"n66" lambda=1.0E-5 dorm=0.0; +"n20" lambda=6.0E-4 dorm=0.0; +"n69" lambda=1.0E-5 dorm=0.0; +"n70" lambda=5.0E-4 dorm=0.0; +"n33" lambda=6.0E-4 dorm=0.0; +"n294" lambda=0.002 dorm=0.0; diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp new file mode 100644 index 000000000..f552fa608 --- /dev/null +++ b/src/test/storm-dft/api/DftApproximationTest.cpp @@ -0,0 +1,103 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" +#include "storm-parsers/api/storm-parsers.h" + +namespace { + + // Configurations for DFT approximation + struct DftAnalysisConfig { + storm::builder::ApproximationHeuristic heuristic; + bool useSR; + }; + + class ApproxDepthConfig { + public: + typedef double ValueType; + static DftAnalysisConfig createConfig() { + return DftAnalysisConfig {storm::builder::ApproximationHeuristic::DEPTH, false}; + } + }; + class ApproxProbabilityConfig { + public: + typedef double ValueType; + static DftAnalysisConfig createConfig() { + return DftAnalysisConfig {storm::builder::ApproximationHeuristic::PROBABILITY, false}; + } + }; + class ApproxBoundDifferenceConfig { + public: + typedef double ValueType; + static DftAnalysisConfig createConfig() { + return DftAnalysisConfig {storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE, false}; + } + }; + + // General base class for testing of DFT approximation + template + class DftApproximationTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + + DftApproximationTest() : config(TestType::createConfig()) { + } + + DftApproximationTest const& getConfig() const { + return config; + } + + std::pair analyzeMTTF(std::string const& file, double errorBound) { + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::string property = "T=? [F \"failed\"]"; + std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFTApprox(*dft, properties, config.useSR, false, true, errorBound, config.heuristic, false); + return boost::get::approximation_result>(results[0]); + } + + std::pair analyzeTimebound(std::string const& file, double timeBound, double errorBound) { + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::stringstream propertyStream; + propertyStream << "P=? [F<=" << timeBound << " \"failed\"]"; + std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str())); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFTApprox(*dft, properties, config.useSR, false, true, errorBound, config.heuristic, false); + return boost::get::approximation_result>(results[0]); + } + + private: + DftAnalysisConfig config; + }; + + typedef ::testing::Types< + ApproxDepthConfig, + ApproxProbabilityConfig, + ApproxBoundDifferenceConfig + > TestingTypes; + + TYPED_TEST_CASE(DftApproximationTest, TestingTypes); + + TYPED_TEST(DftApproximationTest, HecsMTTF) { + double errorBound = 2; + std::pair approxResult = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/hecs_3_2_2_np.dft", errorBound); + EXPECT_LE(approxResult.first, 417.9436693); + EXPECT_GE(approxResult.second, 417.9436693); + EXPECT_LE(2*(approxResult.second - approxResult.first) / (approxResult.first + approxResult.second), errorBound); + // Ensure results are not equal -> not exact values were computed + EXPECT_GE(approxResult.second - approxResult.first, errorBound * approxResult.first / 10); + } + + TYPED_TEST(DftApproximationTest, HecsTimebound) { + //double errorBound = 0.01; + double errorBound = 0.5; + double timeBound = 100; + std::pair approxResult = this->analyzeTimebound(STORM_TEST_RESOURCES_DIR "/dft/hecs_3_2_2_np.dft", timeBound, errorBound); + EXPECT_LE(approxResult.first, 0.0410018417); + EXPECT_GE(approxResult.second, 0.0410018417); + EXPECT_LE(approxResult.second - approxResult.first, errorBound); + // Ensure results are not equal -> not exact values were computed + EXPECT_GE(approxResult.second - approxResult.first, errorBound / 10); + } + +}