Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftBETest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include <boost/math/distributions/weibull.hpp>
5
13
14namespace {
15
16TEST(DftBETest, FailureConstant) {
18 EXPECT_TRUE(be.failed());
19 EXPECT_TRUE(be.canFail());
20
21 EXPECT_EQ(1, be.getUnreliability(0));
22 EXPECT_EQ(1, be.getUnreliability(10));
23
25 EXPECT_FALSE(be2.failed());
26 EXPECT_FALSE(be2.canFail());
27
28 EXPECT_EQ(0, be2.getUnreliability(0));
29 EXPECT_EQ(0, be2.getUnreliability(8));
30}
31
32TEST(DftBETest, FailureProbability) {
34
35 EXPECT_TRUE(be.canFail());
36 EXPECT_EQ(0.2, be.passiveFailureProbability());
37
38 EXPECT_EQ(0.4, be.getUnreliability(0.4));
39 EXPECT_EQ(0.4, be.getUnreliability(0.5));
40 EXPECT_EQ(0.4, be.getUnreliability(1));
41 EXPECT_EQ(0.4, be.getUnreliability(5));
42}
43
44TEST(DftBETest, FailureExponential) {
46
47 EXPECT_TRUE(be.canFail());
48 EXPECT_EQ(1.5, be.passiveFailureRate());
49
50 EXPECT_EQ(0, be.getUnreliability(0));
51 EXPECT_NEAR(0.7768698399, be.getUnreliability(0.5), 1e-10);
52 EXPECT_NEAR(0.9502129316, be.getUnreliability(1), 1e-10);
53 EXPECT_NEAR(0.9975212478, be.getUnreliability(2), 1e-10);
54}
55
56TEST(DftBETest, FailureErlang) {
57 // Single phase
59
60 EXPECT_TRUE(be.canFail());
61 EXPECT_EQ(3, be.passiveFailureRate());
62
63 EXPECT_EQ(0, be.getUnreliability(0));
64 EXPECT_NEAR(0.7768698399, be.getUnreliability(0.5), 1e-10);
65 EXPECT_NEAR(0.9502129316, be.getUnreliability(1), 1e-10);
66 EXPECT_NEAR(0.9975212478, be.getUnreliability(2), 1e-10);
67
68 // Multiple phases
70
71 EXPECT_TRUE(be2.canFail());
72 EXPECT_EQ(3, be2.passiveFailureRate());
73
74 EXPECT_EQ(0, be2.getUnreliability(0));
75 EXPECT_NEAR(0.0656424544, be2.getUnreliability(0.5), 1e-10);
76 EXPECT_NEAR(0.3527681112, be2.getUnreliability(1), 1e-10);
77 EXPECT_NEAR(0.6577040442, be2.getUnreliability(1.5), 1e-10);
78 EXPECT_NEAR(0.8487961172, be2.getUnreliability(2), 1e-10);
79 EXPECT_NEAR(0.9997886215, be2.getUnreliability(5), 1e-10);
80}
81
82TEST(DftBETest, FailureWeibullExponential) {
83 // Reduces to exponential distribution
84 storm::dft::storage::elements::BEWeibull<double> be(0, "TestBE", 1, 1.0 / 3.0);
85
86 EXPECT_TRUE(be.canFail());
87
88 EXPECT_EQ(0, be.getUnreliability(0));
89 EXPECT_NEAR(0.7768698399, be.getUnreliability(0.5), 1e-10);
90 EXPECT_NEAR(0.9502129316, be.getUnreliability(1), 1e-10);
91 EXPECT_NEAR(0.9975212478, be.getUnreliability(2), 1e-10);
92
93 // Compare with boost results
94 boost::math::weibull_distribution<double> dist(1, 1.0 / 3.0);
95 for (double t = 0; t <= 5.0; t += 0.25) {
96 EXPECT_NEAR(boost::math::cdf(dist, t), be.getUnreliability(t), 1e-10);
97 }
98
99 // Increasing failure rate
101
102 EXPECT_TRUE(be2.canFail());
103
104 EXPECT_EQ(0, be2.getUnreliability(0));
105 EXPECT_NEAR(0.0605869372, be2.getUnreliability(0.5), 1e-10);
106 EXPECT_NEAR(0.2211992169, be2.getUnreliability(1), 1e-10);
107 EXPECT_NEAR(0.6321205588, be2.getUnreliability(2), 1e-10);
108 EXPECT_NEAR(0.9980695458, be2.getUnreliability(5), 1e-10);
109
110 // Compare with boost results
111 boost::math::weibull_distribution<double> dist2(2, 2);
112 for (double t = 0; t <= 5.0; t += 0.25) {
113 EXPECT_NEAR(boost::math::cdf(dist2, t), be2.getUnreliability(t), 1e-10);
114 }
115
116 // Decreasing failure rate
118
119 EXPECT_TRUE(be3.canFail());
120
121 EXPECT_EQ(0, be3.getUnreliability(0));
122 EXPECT_NEAR(0.4369287910, be3.getUnreliability(0.5), 1e-10);
123 EXPECT_NEAR(0.5313308906, be3.getUnreliability(1), 1e-10);
124 EXPECT_NEAR(0.6321205588, be3.getUnreliability(2), 1e-10);
125 EXPECT_NEAR(0.7637110612, be3.getUnreliability(5), 1e-10);
126
127 // Compare with boost results
128 boost::math::weibull_distribution<double> dist3(0.4, 2);
129 for (double t = 0; t <= 5.0; t += 0.25) {
130 EXPECT_NEAR(boost::math::cdf(dist3, t), be3.getUnreliability(t), 1e-10);
131 }
132}
133
134TEST(DftBETest, FailureLogNormal) {
135 // First distribution
137
138 EXPECT_TRUE(be.canFail());
139
140 EXPECT_EQ(0, be.getUnreliability(0));
141 EXPECT_NEAR(0.0828285190, be.getUnreliability(0.5), 1e-10);
142 EXPECT_NEAR(0.5, be.getUnreliability(1), 1e-10);
143 EXPECT_NEAR(0.9171714810, be.getUnreliability(2), 1e-10);
144 EXPECT_NEAR(0.9993565290, be.getUnreliability(5), 1e-10);
145
146 // Second distribution
148
149 EXPECT_TRUE(be2.canFail());
150
151 EXPECT_EQ(0, be2.getUnreliability(0));
152 EXPECT_NEAR(6.32491e-12, be2.getUnreliability(0.5), 1e-17);
153 EXPECT_NEAR(3.167124183e-5, be2.getUnreliability(1), 1e-14);
154 EXPECT_NEAR(0.1098340249, be2.getUnreliability(2), 1e-10);
155 EXPECT_NEAR(0.9926105382, be2.getUnreliability(5), 1e-10);
156}
157
158TEST(DftBETest, FailureSamples) {
159 // Weibull distribution with shape 5 and scale 1
160 std::map<double, double> samples = {{0.0, 0.0},
161 {0.25, 0.0009760858180243304},
162 {0.5, 0.03076676552365587},
163 {0.75, 0.21124907114638225},
164 {1.0, 0.6321205588285577},
165 {1.25, 0.9527242505937095},
166 {1.5, 0.9994964109502631},
167 {1.75, 0.999999925546118},
168 {2.0, 0.9999999999999873}};
170
171 EXPECT_TRUE(be.canFail());
172
173 // Compare with boost results
174 boost::math::weibull_distribution<double> dist(5, 1);
175 for (double t = 0; t <= 2.0; t += 0.25) {
176 EXPECT_NEAR(boost::math::cdf(dist, t), be.getUnreliability(t), 1e-10);
177 }
178}
179
180} // namespace
TEST(OrderTest, Simple)
Definition OrderTest.cpp:15
BE which is either constant failed or constant failsafe.
Definition BEConst.h:14
BE with Erlang failure distribution.
Definition BEErlang.h:13
BE with exponential failure distribution.
BE with log-normal failure distribution.
Definition BELogNormal.h:13
BE with constant (Bernoulli) failure probability distribution.
BE where the failure distribution is defined by samples.
Definition BESamples.h:16
BE with Weibull failure distribution.
Definition BEWeibull.h:13