Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-dft/api/storm-dft.h"
5#include "storm-parsers/api/storm-parsers.h"
6
7namespace {
8
9// Configurations for DFT analysis
10struct DftAnalysisConfig {
11 bool useSR;
12 bool useMod;
13 bool useDC;
14};
15
16class NoOptimizationsConfig {
17 public:
18 typedef double ValueType;
19
20 static DftAnalysisConfig createConfig() {
21 return DftAnalysisConfig{false, false, false};
22 }
23};
24
25class DontCareOnlyConfig {
26 public:
27 typedef double ValueType;
28
29 static DftAnalysisConfig createConfig() {
30 return DftAnalysisConfig{false, false, true};
31 }
32};
33
34class ModularisationOnlyConfig {
35 public:
36 typedef double ValueType;
37
38 static DftAnalysisConfig createConfig() {
39 return DftAnalysisConfig{false, true, false};
40 }
41};
42
43class SymmetryReductionOnlyConfig {
44 public:
45 typedef double ValueType;
46
47 static DftAnalysisConfig createConfig() {
48 return DftAnalysisConfig{true, false, false};
49 }
50};
51
52class ModularisationConfig {
53 public:
54 typedef double ValueType;
55
56 static DftAnalysisConfig createConfig() {
57 return DftAnalysisConfig{false, true, true};
58 }
59};
60
61class SymmetryReductionConfig {
62 public:
63 typedef double ValueType;
64
65 static DftAnalysisConfig createConfig() {
66 return DftAnalysisConfig{true, false, true};
67 }
68};
69
70class AllOptimizationsConfig {
71 public:
72 typedef double ValueType;
73
74 static DftAnalysisConfig createConfig() {
75 return DftAnalysisConfig{true, true, true};
76 }
77};
78
79// General base class for testing of DFT model checking
80template<typename TestType>
81class DftModelCheckerTest : public ::testing::Test {
82 public:
83 typedef typename TestType::ValueType ValueType;
84
85 DftModelCheckerTest() : config(TestType::createConfig()) {}
86
87 DftAnalysisConfig const& getConfig() const {
88 return config;
89 }
90
91 double analyze(std::string const& file, std::string const& property) {
92 // Load, build and prepare DFT
93 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
94 storm::dft::api::prepareForMarkovAnalysis<double>(*(storm::dft::api::loadDFTGalileoFile<double>(file)));
95 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
96
97 // Create property
98 std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
99
100 // Create relevant names
101 std::vector<std::string> relevantNames;
102 if (!config.useDC) {
103 relevantNames.push_back("all");
104 }
105 storm::dft::utility::RelevantEvents relevantEvents = storm::dft::api::computeRelevantEvents(properties, relevantNames);
106
107 // Perform model checking
108 typename storm::dft::modelchecker::DFTModelChecker<double>::dft_results results =
109 storm::dft::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, relevantEvents, false);
110 return boost::get<double>(results[0]);
111 }
112
113 double analyzeMTTF(std::string const& file) {
114 std::string property = "Tmin=? [F \"failed\"]";
115 return analyze(file, property);
116 }
117
118 double analyzeReliability(std::string const& file, double bound) {
119 std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
120 return analyze(file, property);
121 }
122
123 double analyzeReachability(std::string const& file) {
124 std::string property = "Pmin=? [F \"failed\"]";
125 return analyze(file, property);
126 }
127
128 double precision() {
129 return 1e-12;
130 }
131
132 double precisionReliability() {
133 return 1e-10;
134 }
135
136 private:
137 DftAnalysisConfig config;
138};
139
140typedef ::testing::Types<NoOptimizationsConfig, DontCareOnlyConfig, ModularisationOnlyConfig, SymmetryReductionOnlyConfig, ModularisationConfig,
141 SymmetryReductionConfig, AllOptimizationsConfig>
142 TestingTypes;
143
144TYPED_TEST_SUITE(DftModelCheckerTest, TestingTypes, );
145
146TYPED_TEST(DftModelCheckerTest, AndMTTF) {
147 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
148 EXPECT_NEAR(result, 3, this->precision());
149}
150
151TYPED_TEST(DftModelCheckerTest, OrMTTF) {
152 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/or.dft");
153 EXPECT_NEAR(result, 1, this->precision());
154}
155
156TYPED_TEST(DftModelCheckerTest, VotingMTTF) {
157 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting.dft");
158 EXPECT_NEAR(result, 5 / 3.0, this->precision());
159 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft");
160 EXPECT_NEAR(result, 10 / 17.0, this->precision());
161 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft");
162 EXPECT_NEAR(result, 2685 / 1547.0, this->precision());
163 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft");
164 EXPECT_NEAR(result, 5 / 6.0, this->precision());
165}
166
167TYPED_TEST(DftModelCheckerTest, PandMTTF) {
168 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
169 EXPECT_EQ(result, storm::utility::infinity<double>());
170}
171
172TYPED_TEST(DftModelCheckerTest, PorMTTF) {
173 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/por.dft");
174 EXPECT_EQ(result, storm::utility::infinity<double>());
175}
176
177TYPED_TEST(DftModelCheckerTest, FdepMTTF) {
178 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft");
179 EXPECT_NEAR(result, 2, this->precision());
180 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft");
181 EXPECT_NEAR(result, 5 / 2.0, this->precision());
182 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep7.dft");
183 EXPECT_NEAR(result, 5 / 12.0, this->precision());
184
185 if (this->getConfig().useMod) {
186 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"), storm::exceptions::NotSupportedException);
187 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"), storm::exceptions::NotSupportedException);
188 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException);
189 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft"), storm::exceptions::NotSupportedException);
190 } else {
191 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
192 EXPECT_NEAR(result, 2 / 3.0, this->precision());
193 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
194 EXPECT_NEAR(result, 1, this->precision());
195 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
196 EXPECT_NEAR(result, 3, this->precision());
197 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft");
198 EXPECT_NEAR(result, 9 / 56.0, this->precision());
199 }
200}
201
202TYPED_TEST(DftModelCheckerTest, PdepMTTF) {
203 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
204 EXPECT_NEAR(result, 8 / 3.0, this->precision());
205 if (this->getConfig().useMod && !this->getConfig().useDC) {
206 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft"), storm::exceptions::NotSupportedException);
207 } else {
208 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
209 EXPECT_NEAR(result, 38 / 15.0, this->precision());
210 }
211 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
212 EXPECT_NEAR(result, 67 / 24.0, this->precision());
213
214 if (this->getConfig().useMod) {
215 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"), storm::exceptions::NotSupportedException);
216 } else {
217 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
218 EXPECT_EQ(result, storm::utility::infinity<double>());
219 }
220}
221
222TYPED_TEST(DftModelCheckerTest, SpareMTTF) {
223 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare.dft");
224 EXPECT_NEAR(result, 46 / 13.0, this->precision());
225 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft");
226 EXPECT_NEAR(result, 43 / 23.0, this->precision());
227 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft");
228 EXPECT_NEAR(result, 14 / 11.0, this->precision());
229 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft");
230 EXPECT_NEAR(result, 18836 / 3887.0, this->precision());
231 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
232 EXPECT_NEAR(result, 8 / 3.0, this->precision());
233 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft");
234 EXPECT_NEAR(result, 7 / 5.0, this->precision());
235 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft");
236 EXPECT_NEAR(result, 551 / 150.0, this->precision());
237 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft");
238 EXPECT_NEAR(result, 249 / 52.0, this->precision()); // DFTCalc has result of 4.33779 due to different semantics of nested spares
239 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare_dc.dft");
240 EXPECT_NEAR(result, 78311 / 182700.0, this->precision());
241 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/modules3.dft");
242 EXPECT_NEAR(result, 7 / 6.0, this->precision());
243 // Spare gate is part of spare module. As a result it is not activated.
244 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare_contains_spare.dft");
245 EXPECT_NEAR(result, 1, this->precision());
246}
247
248TYPED_TEST(DftModelCheckerTest, SeqMTTF) {
249 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");
250 EXPECT_NEAR(result, 4, this->precision());
251 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft");
252 EXPECT_NEAR(result, 6, this->precision());
253 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft");
254 EXPECT_NEAR(result, 6, this->precision());
255 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft");
256 EXPECT_NEAR(result, 6, this->precision());
257 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft");
258 EXPECT_EQ(result, storm::utility::infinity<double>());
259 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft");
260 EXPECT_NEAR(result, 30000, this->precision());
261
262 if (this->getConfig().useMod) {
263 STORM_SILENT_EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq7.dft"), storm::exceptions::NotSupportedException);
264 } else {
265 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq7.dft");
266 EXPECT_EQ(result, storm::utility::infinity<double>());
267 }
268 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/seq7.dft", 1.0);
269 EXPECT_NEAR(result, 0.08, this->precision());
270 result = this->analyzeReachability(STORM_TEST_RESOURCES_DIR "/dft/seq7.dft");
271 EXPECT_NEAR(result, 0.08, this->precision());
272 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq8.dft");
273 EXPECT_NEAR(result, 11 / 8.0, this->precision());
274}
275
276TYPED_TEST(DftModelCheckerTest, Mutex) {
277 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft");
278 EXPECT_NEAR(result, 1 / 2.0, this->precision());
279 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft", 1.0);
280 EXPECT_NEAR(result, 0.8646647168, this->precisionReliability());
281 result = this->analyzeReachability(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft");
282 EXPECT_NEAR(result, 1, this->precision());
283
284 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft");
285 EXPECT_EQ(result, storm::utility::infinity<double>());
286 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft", 1.0);
287 EXPECT_NEAR(result, 0, this->precision());
288 result = this->analyzeReachability(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft");
289 EXPECT_NEAR(result, 0, this->precision());
290
291 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
292 EXPECT_EQ(result, storm::utility::infinity<double>());
293 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft", 1.0);
294 EXPECT_NEAR(result, 0, this->precision());
295 result = this->analyzeReachability(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft");
296 EXPECT_NEAR(result, 0, this->precision());
297
298 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/mutex4.dft");
299 EXPECT_EQ(result, storm::utility::infinity<double>());
300 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/mutex4.dft", 1.0);
301 EXPECT_NEAR(result, 0.5842978146, this->precisionReliability());
302 result = this->analyzeReachability(STORM_TEST_RESOURCES_DIR "/dft/mutex4.dft");
303 EXPECT_NEAR(result, 5 / 8.0, this->precision());
304}
305
306TYPED_TEST(DftModelCheckerTest, Symmetry) {
307 double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft");
308 EXPECT_NEAR(result, 2804183 / 2042040.0, this->precision());
309 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1.0);
310 EXPECT_NEAR(result, 0.3421934224, this->precisionReliability());
311
312 result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep_symmetry.dft");
313 EXPECT_NEAR(result, 6553 / 5376.0, this->precision());
314 result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/pdep_symmetry.dft", 1.0);
315 EXPECT_NEAR(result, 0.4223514414, this->precisionReliability());
316}
317
318TYPED_TEST(DftModelCheckerTest, HecsReliability) {
319 if (!this->getConfig().useDC) {
320 // Skip configurations because it takes too long
321 GTEST_SKIP();
322 return;
323 }
324 double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
325 EXPECT_NEAR(result, 0.00021997582, this->precisionReliability());
326}
327} // namespace
storm::dft::modelchecker::DFTModelChecker::dft_results
std::vector< boost::variant< ValueType, approximation_result > > dft_results
Definition DFTModelChecker.h:21
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::dft::api::computeRelevantEvents
storm::dft::utility::RelevantEvents computeRelevantEvents(std::vector< std::shared_ptr< storm::logic::Formula const > > const &properties, std::vector< std::string > const &additionalRelevantEventNames)
Get relevant event ids from given relevant event names and labels in properties.
Definition storm-dft.cpp:266
storm::dft::modelchecker::ValueType
SFTBDDChecker::ValueType ValueType
Definition SFTBDDChecker.cpp:13
TYPED_TEST
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:49
TYPED_TEST_SUITE
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
TestingTypes
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:46
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104