Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
BEDistributionTest.cpp
Go to the documentation of this file.
1#include "test/storm_gtest.h"
2
3#include "storm-dft/api/storm-dft.h"
4#include "storm-dft/modelchecker/SFTBDDChecker.h"
5#include "storm-parsers/api/storm-parsers.h"
6
7namespace {
8
9TEST(BEDistributionTest, ConstantFail) {
10 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_fail.dft");
11 double timebound = 0.8;
12
13 // Perform BDD-based analysis on FT
14 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
15 double resultBDD = checker->getProbabilityAtTimebound(timebound);
16 EXPECT_NEAR(resultBDD, 0.3296799540, 1e-10);
17
18 // Perform Markovian analysis on FT
19 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
20 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
21 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
22 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
23 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
24 EXPECT_NEAR(resultBDD, resultMC, 1e-10);
25}
26
27TEST(BEDistributionTest, ConstantNonFail) {
28 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_constant.dft");
29 double timebound = 0.8;
30
31 // Perform BDD-based analysis on FT
32 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
33 double resultBDD = checker->getProbabilityAtTimebound(timebound);
34 EXPECT_NEAR(resultBDD, 0.9592377960, 1e-10);
35
36 // Perform Markovian analysis on FT
37 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
38 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
39 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
40 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
41 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
42 EXPECT_NEAR(resultBDD, resultMC, 1e-10);
43}
44
45TEST(BEDistributionTest, ConstantNonFail2) {
46 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_nonfail2.dft");
47 double timebound = 0.8;
48
49 // Perform BDD-based analysis on FT
50 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
51 double resultBDD = checker->getProbabilityAtTimebound(timebound);
52 EXPECT_EQ(resultBDD, 0);
53
54 // Perform Markovian analysis on FT
55 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
56 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
57 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
58 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
59 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
60 EXPECT_EQ(resultBDD, resultMC);
61}
62
63TEST(BEDistributionTest, Probability) {
64 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_probabilistic.dft");
65 double timebound = 0.8;
66
67 // Perform BDD-based analysis on FT
68 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
69 double resultBDD = checker->getProbabilityAtTimebound(timebound);
70 EXPECT_NEAR(resultBDD, 0.1095403852, 1e-10);
71
72 // Perform Markovian analysis on FT
73 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
74 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
75 std::string property = "Pmax=? [F<=" + std::to_string(timebound) + " \"failed\"]";
76 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
77 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
78 EXPECT_NEAR(resultBDD, resultMC, 1e-10);
79}
80
81TEST(BEDistributionTest, Exponential) {
82 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
83 double timebound = 0.8;
84
85 // Perform BDD-based analysis on FT
86 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
87 double resultBDD = checker->getProbabilityAtTimebound(timebound);
88 EXPECT_NEAR(resultBDD, 0.108688872, 1e-10);
89
90 // Perform Markovian analysis on FT
91 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
92 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
93 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
94 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
95 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
96 EXPECT_NEAR(resultBDD, resultMC, 1e-10);
97}
98
99TEST(BEDistributionTest, Erlang) {
100 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_erlang.dft");
101 double timebound = 0.8;
102
103 // Perform BDD-based analysis on FT
104 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
105 double resultBDD = checker->getProbabilityAtTimebound(timebound);
106 EXPECT_NEAR(resultBDD, 0.4949009834, 1e-10);
107
108 // Perform Markovian analysis on FT
109 auto dft2 = storm::dft::api::prepareForMarkovAnalysis<double>(*dft);
110 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft2).first);
111 std::string property = "P=? [F<=" + std::to_string(timebound) + " \"failed\"]";
112 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
113 double resultMC = boost::get<double>(storm::dft::api::analyzeDFT<double>(*dft2, properties)[0]);
114 EXPECT_NEAR(resultBDD, resultMC, 1e-10);
115}
116
117TEST(BEDistributionTest, Weibull) {
118 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_weibull.dft");
119 double timebound = 2;
120
121 // Perform BDD-based analysis on FT
122 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
123 double resultBDD = checker->getProbabilityAtTimebound(timebound);
124 EXPECT_NEAR(resultBDD, 0.0382982486, 1e-10);
125}
126
127TEST(BEDistributionTest, LogNormal) {
128 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/be_lognormal.dft");
129 double timebound = 0.8;
130
131 // Perform BDD-based analysis on FT
132 auto checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
133 double resultBDD = checker->getProbabilityAtTimebound(timebound);
134 EXPECT_NEAR(resultBDD, 0.2336675428, 1e-10);
135}
136
137} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
storm::api::parseProperties
std::vector< storm::jani::Property > parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional< std::set< std::string > > const &propertyFilter)
Definition properties.cpp:27
storm::api::extractFormulasFromProperties
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
Definition properties.cpp:64
storm::dft::api::isWellFormed
std::pair< bool, std::string > isWellFormed(storm::dft::storage::DFT< ValueType > const &dft, bool validForMarkovianAnalysis=true)
Check whether the DFT is well-formed.
Definition storm-dft.h:64
storm_gtest.h