Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TestBdd.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-dft/adapters/SFTBDDPropertyFormulaAdapter.h"
5#include "storm-dft/api/storm-dft.h"
6#include "storm-dft/modelchecker/SFTBDDChecker.h"
7#include "storm-dft/transformations/SftToBddTransformator.h"
8#include "storm-dft/utility/MTTFHelper.h"
9#include "storm-parsers/api/properties.h"
10
11namespace {
12
13struct SftTestData {
14 std::string testname;
15 std::string filepath;
16 std::string bddHash;
17 double probabilityAtTimeboundOne;
18 double mttf;
19 std::vector<double> birnbaum;
20 std::vector<double> CIF;
21 std::vector<double> DIF;
22 std::vector<double> RAW;
23 std::vector<double> RRW;
24
25 friend std::ostream &operator<<(std::ostream &os, SftTestData const &data) {
26 auto printVector = [&os](std::vector<double> const &arr) {
27 os << ", {";
28 for (auto const &i : arr) {
29 os << i;
30 // will leave trailing ", " but its simpler
31 // and would still be a valid initializer
32 os << ", ";
33 }
34 os << '}';
35 };
36
37 os << "{\"" << data.testname << '"';
38 os << ", \"" << data.filepath << '"';
39 os << ", \"" << data.bddHash << '"';
40 os << ", " << data.probabilityAtTimeboundOne;
41 os << ", " << data.mttf;
42 printVector(data.birnbaum);
43 printVector(data.CIF);
44 printVector(data.DIF);
45 printVector(data.RAW);
46 printVector(data.RRW);
47 os << '}';
48 return os;
49 }
50};
51
52class SftBddTest : public testing::TestWithParam<SftTestData> {
53 protected:
54 void SetUp() override {
55 auto const &param{TestWithParam::GetParam()};
56 auto dft{storm::dft::api::loadDFTGalileoFile<double>(param.filepath)};
57 checker = std::make_shared<storm::dft::modelchecker::SFTBDDChecker>(dft);
58 }
59
60 std::shared_ptr<storm::dft::modelchecker::SFTBDDChecker> checker;
61};
62
63TEST_P(SftBddTest, bddHash) {
64 auto const &param{TestWithParam::GetParam()};
65 EXPECT_EQ(checker->getTransformator()->transformTopLevel().GetShaHash(), param.bddHash);
66}
67
68TEST_P(SftBddTest, ProbabilityAtTimeOne) {
69 auto const &param{TestWithParam::GetParam()};
70 EXPECT_NEAR(checker->getProbabilityAtTimebound(1), param.probabilityAtTimeboundOne, 1e-6);
71}
72
73TEST_P(SftBddTest, MTTF) {
74 auto const &param{TestWithParam::GetParam()};
75 EXPECT_NEAR(storm::dft::utility::MTTFHelperProceeding(checker->getDFT()), param.mttf, 1e-5);
76 EXPECT_NEAR(storm::dft::utility::MTTFHelperVariableChange(checker->getDFT()), param.mttf, 1e-5);
77}
78
79template<typename T1, typename T2>
80void expectVectorNear(T1 const &v1, T2 const &v2, double const precision = 1e-6) {
81 ASSERT_EQ(v1.size(), v2.size());
82 for (size_t i{0}; i < v1.size(); ++i) {
83 if (!std::isinf(v1[i])) {
84 EXPECT_NEAR(v1[i], v2[i], precision);
85 } else {
86 EXPECT_EQ(v1[i], v2[i]);
87 }
88 }
89}
90
91TEST_P(SftBddTest, Birnbaum) {
92 auto const &param{TestWithParam::GetParam()};
93 expectVectorNear(checker->getAllBirnbaumFactorsAtTimebound(1), param.birnbaum);
94}
95
96TEST_P(SftBddTest, CIF) {
97 auto const &param{TestWithParam::GetParam()};
98 expectVectorNear(checker->getAllCIFsAtTimebound(1), param.CIF);
99}
100
101TEST_P(SftBddTest, DIF) {
102 auto const &param{TestWithParam::GetParam()};
103 expectVectorNear(checker->getAllDIFsAtTimebound(1), param.DIF);
104}
105
106TEST_P(SftBddTest, RAW) {
107 auto const &param{TestWithParam::GetParam()};
108 expectVectorNear(checker->getAllRAWsAtTimebound(1), param.RAW);
109}
110
111TEST_P(SftBddTest, RRW) {
112 auto const &param{TestWithParam::GetParam()};
113 expectVectorNear(checker->getAllRRWsAtTimebound(1), param.RRW);
114}
115
116static std::vector<SftTestData> sftTestData{
117 {
118 "And",
119 STORM_TEST_RESOURCES_DIR "/dft/bdd/AndTest.dft",
120 "07251c962e40a962c342b8673fd18b45a1461ebd917f83f6720aa106cf277f9f",
121 0.25,
122 2.164042561,
123 {0.5, 0.5},
124 {1, 1},
125 {1, 1},
126 {2, 2},
127 {INFINITY, INFINITY},
128 },
129 {
130 "Or",
131 STORM_TEST_RESOURCES_DIR "/dft/bdd/OrTest.dft",
132 "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d",
133 0.75,
134 0.7213475204,
135 {0.5, 0.5},
136 {0.3333333333, 0.3333333333},
137 {0.666667, 0.666667},
138 {1.333333333, 1.333333333},
139 {1.5, 1.5},
140 },
141 {
142 "AndOr",
143 STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft",
144 "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae",
145 0.5625,
146 1.082021281,
147 {0.375, 0.375, 0.375, 0.375},
148 {0.3333333333, 0.3333333333, 0.3333333333, 0.3333333333},
149 {0.666667, 0.666667, 0.666667, 0.666667},
150 {1.333333333, 1.333333333, 1.333333333, 1.333333333},
151 {1.5, 1.5, 1.5, 1.5},
152 },
153 {
154 "Vot",
155 STORM_TEST_RESOURCES_DIR "/dft/bdd/VotTest.dft",
156 "c005a8d6ad70cc497e1efa3733b0dc52e94c465572d3f1fc5de4983ddd178094",
157 0.6875,
158 0.8415721072,
159 {0.375, 0.375, 0.375, 0.375},
160 {0.27272727, 0.27272727, 0.27272727, 0.27272727},
161 {0.636364, 0.636364, 0.636364, 0.636364},
162 {1.27272727, 1.27272727, 1.27272727, 1.27272727},
163 {1.375, 1.375, 1.375, 1.375},
164 },
165 {
166 "Importance",
167 STORM_TEST_RESOURCES_DIR "/dft/bdd/ImportanceTest.dft",
168 "38221c1eb557dd6f15cf33faf61e18c4e426fab2fb909c56ac0d5f4ff0be499f",
169 0.2655055433,
170 1.977074913,
171 {0.531011, 0.368041, 0.224763, 0.0596235, 0.0543206, 0.0810368, 0},
172 {1, 0.693094, 0.153453, 0.112283, 0.09231, 0.192934, 0},
173 {1, 0.846547, 0.306906, 0.556142, 0.501849, 0.703097, 0.5},
174 {2, 1.693094106, 1.693094106, 1.112283035, 1.112283035, 1.112283035, 1},
175 {INFINITY, 3.25832778, 1.18127, 1.126485175, 1.1016977, 1.23905588, 1},
176 },
177};
178INSTANTIATE_TEST_SUITE_P(SFTs, SftBddTest, testing::ValuesIn(sftTestData), [](auto const &info) { return info.param.testname; });
179
180TEST(TestBdd, AndOrRelevantEvents) {
181 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft");
182 auto manager = std::make_shared<storm::dft::storage::SylvanBddManager>();
183 storm::dft::utility::RelevantEvents relevantEvents{"F", "F1", "F2", "x1"};
184 storm::dft::transformations::SftToBddTransformator<double> transformer{dft, manager, relevantEvents};
185
186 auto const result = transformer.transformRelevantEvents();
187
188 EXPECT_EQ(result.size(), 4ul);
189
190 EXPECT_EQ(result.at("F").GetShaHash(), "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae");
191 EXPECT_EQ(result.at("F1").GetShaHash(), "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d");
192 EXPECT_EQ(result.at("F2").GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59");
193 EXPECT_EQ(result.at("x1").GetShaHash(), "b0d991484e405a391b6d3d241fed9c00d4a2e5bf6f57300512394d819253893d");
194}
195
196TEST(TestBdd, AndOrRelevantEventsChecked) {
197 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft");
198 auto manager{std::make_shared<storm::dft::storage::SylvanBddManager>()};
199 storm::dft::utility::RelevantEvents relevantEvents{"F", "F1", "F2", "x1"};
200 auto transformator{std::make_shared<storm::dft::transformations::SftToBddTransformator<double>>(dft, manager, relevantEvents)};
201
202 storm::dft::modelchecker::SFTBDDChecker checker{transformator};
203
204 auto relevantEventsBdds = transformator->transformRelevantEvents();
205
206 EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["F"], 1), 0.5625, 1e-6);
207
208 EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["F1"], 1), 0.75, 1e-6);
209 EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["F2"], 1), 0.75, 1e-6);
210
211 EXPECT_NEAR(checker.getProbabilityAtTimebound(relevantEventsBdds["x1"], 1), 0.5, 1e-6);
212}
213
214TEST(TestBdd, AndOrFormulaFail) {
215 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft");
216 auto const props{storm::api::extractFormulasFromProperties(storm::api::parseProperties("P=? [F < 1 !\"F2_failed\"];"))};
217 storm::dft::adapters::SFTBDDPropertyFormulaAdapter checker{dft, props};
218
219 STORM_SILENT_EXPECT_THROW(checker.check(), storm::exceptions::NotSupportedException);
220}
221
222TEST(TestBdd, AndOrFormula) {
223 auto dft = storm::dft::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/bdd/AndOrTest.dft");
224 auto const props{
225 storm::api::extractFormulasFromProperties(storm::api::parseProperties("P=? [F <= 1 \"failed\"];"
226 "P=? [F <= 1 \"F_failed\"];"
227 "P=? [F <= 1 \"F1_failed\" & \"F2_failed\"];"
228 "P=? [F = 1 !\"failed\"];"
229 "P=? [F = 1 !\"F1_failed\"];"
230 "P=? [F = 1 !\"F2_failed\"];"
231 "P=? [F <= 1 \"F1_failed\"];"
232 "P=? [F <= 1 \"F2_failed\"];"))};
233 storm::dft::adapters::SFTBDDPropertyFormulaAdapter checker{dft, props};
234
235 auto const resultProbs{checker.check()};
236 auto const result{checker.formulasToBdd()};
237
238 EXPECT_EQ(result.size(), 8ul);
239
240 EXPECT_EQ(resultProbs[0], resultProbs[1]);
241 EXPECT_EQ(resultProbs[1], resultProbs[2]);
242 EXPECT_NEAR(resultProbs[0], 0.5625, 1e-6);
243
244 EXPECT_NEAR(resultProbs[3], 1 - resultProbs[0], 1e-6);
245
246 EXPECT_EQ(resultProbs[6], resultProbs[7]);
247 EXPECT_NEAR(resultProbs[6], 0.75, 1e-6);
248
249 EXPECT_EQ(resultProbs[4], resultProbs[5]);
250 EXPECT_NEAR(resultProbs[4], 1 - resultProbs[6], 1e-6);
251
252 EXPECT_EQ(result[0], result[1]);
253 EXPECT_EQ(result[1], result[2]);
254 EXPECT_EQ(result[2], result[0]);
255
256 EXPECT_EQ(result[0].GetBDD(), result[1].GetBDD());
257 EXPECT_EQ(result[1].GetBDD(), result[2].GetBDD());
258 EXPECT_EQ(result[2].GetBDD(), result[0].GetBDD());
259
260 EXPECT_EQ(result[0].GetBDD(), (!result[3]).GetBDD());
261 EXPECT_NE(result[0].GetBDD(), result[3].GetBDD());
262
263 EXPECT_EQ(result[6].GetBDD(), (!result[4]).GetBDD());
264 EXPECT_NE(result[6].GetBDD(), result[4].GetBDD());
265
266 EXPECT_EQ(result[7].GetBDD(), (!result[5]).GetBDD());
267 EXPECT_NE(result[7].GetBDD(), result[5].GetBDD());
268
269 EXPECT_NE(result[3].GetBDD(), result[4].GetBDD());
270
271 EXPECT_EQ(result[0].GetShaHash(), "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae");
272 EXPECT_EQ(result[1].GetShaHash(), "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae");
273 EXPECT_EQ(result[2].GetShaHash(), "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae");
274 EXPECT_EQ(result[3].GetShaHash(), "fc1e9a418e3c207e81ffa7fde7768f027b6996732c4216c1ed5de6861dbc86ae");
275 EXPECT_EQ(result[4].GetShaHash(), "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d");
276 EXPECT_EQ(result[5].GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59");
277 EXPECT_EQ(result[6].GetShaHash(), "c5cf2304417926961c3e1ce1d876fc2886ece1365fd946bfd3e1abd71401696d");
278 EXPECT_EQ(result[7].GetShaHash(), "a4f129fa27c6cd32625b088811d4b12f8059ae0547ee035c083deed9ef9d2c59");
279}
280
281} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
storm::dft::adapters::SFTBDDPropertyFormulaAdapter::check
std::vector< ValueType > check(size_t const chunksize=0)
Calculate the properties specified by the formulas.
Definition SFTBDDPropertyFormulaAdapter.h:75
storm::dft::modelchecker::SFTBDDChecker
Main class for the SFTBDDChecker.
Definition SFTBDDChecker.h:22
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::counterexamples::operator<<
std::ostream & operator<<(std::ostream &out, Counterexample const &counterexample)
Definition Counterexample.cpp:6
storm::dft::utility::MTTFHelperVariableChange
double MTTFHelperVariableChange(std::shared_ptr< storm::dft::storage::DFT< double > > const dft, double const stepsize)
Tries to numerically approximate the mttf of the given dft by integrating 1 - cdf(dft) by changing th...
Definition MTTFHelper.cpp:65
storm::dft::utility::MTTFHelperProceeding
double MTTFHelperProceeding(std::shared_ptr< storm::dft::storage::DFT< double > > const dft, double const stepsize, double const precision)
Tries to numerically approximate the mttf of the given dft by integrating 1 - cdf(dft) with Simpson's...
Definition MTTFHelper.cpp:24
storm::settings::manager
SettingsManager const & manager()
Retrieves the settings manager.
Definition SettingsManager.cpp:662
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104