Browse Source

Added test cases for DFT approximation

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
23233afe0b
  1. 71
      resources/examples/testfiles/dft/hecs_3_2_2_np.dft
  2. 103
      src/test/storm-dft/api/DftApproximationTest.cpp

71
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;

103
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<typename TestType>
class DftApproximationTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
DftApproximationTest() : config(TestType::createConfig()) {
}
DftApproximationTest const& getConfig() const {
return config;
}
std::pair<double, double> analyzeMTTF(std::string const& file, double errorBound) {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_TRUE(storm::api::isWellFormed(*dft));
std::string property = "T=? [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::analyzeDFTApprox<double>(*dft, properties, config.useSR, false, true, errorBound, config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::approximation_result>(results[0]);
}
std::pair<double, double> analyzeTimebound(std::string const& file, double timeBound, double errorBound) {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_TRUE(storm::api::isWellFormed(*dft));
std::stringstream propertyStream;
propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFTApprox<double>(*dft, properties, config.useSR, false, true, errorBound, config.heuristic, false);
return boost::get<storm::modelchecker::DFTModelChecker<double>::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<double, double> 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<double, double> 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);
}
}
Loading…
Cancel
Save