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