Storm
A Modern Probabilistic Model Checker
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
DftSimulatorTest.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-dft/generator/DftNextStateGenerator.h"
6#include "storm-dft/simulator/DFTTraceSimulator.h"
7#include "storm-dft/storage/DftSymmetries.h"
8
9namespace {
10
11// Helper functions
12std::pair<double, double> simulateDft(std::string const& file, double timebound, size_t noRuns) {
13 // Load, build and prepare DFT
14 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
15 storm::dft::api::prepareForMarkovAnalysis<double>(*(storm::dft::api::loadDFTGalileoFile<double>(file)));
16 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
17
18 // Set relevant events
19 storm::dft::utility::RelevantEvents relevantEvents = storm::dft::api::computeRelevantEvents({}, {});
20 dft->setRelevantEvents(relevantEvents, false);
21
22 // Find symmetries
23 storm::dft::storage::DftSymmetries symmetries;
24 storm::dft::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries));
25
26 // Init random number generator
27 // storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
28 boost::mt19937 gen(5u);
29 storm::dft::simulator::DFTTraceSimulator<double> simulator(*dft, stateGenerationInfo, gen);
30
31 size_t count = 0;
32 size_t invalid = 0;
33 storm::dft::simulator::SimulationTraceResult res;
34 for (size_t i = 0; i < noRuns; ++i) {
35 res = simulator.simulateCompleteTrace(timebound);
36 if (res == storm::dft::simulator::SimulationTraceResult::SUCCESSFUL) {
37 ++count;
38 } else if (res == storm::dft::simulator::SimulationTraceResult::INVALID) {
39 // Discard invalid traces
40 ++invalid;
41 }
42 }
43 return std::make_pair(count, invalid);
44}
45
46double simulateDftProb(std::string const& file, double timebound, size_t noRuns) {
47 size_t count;
48 size_t invalid;
49 std::tie(count, invalid) = simulateDft(file, timebound, noRuns);
50 EXPECT_EQ(invalid, 0ul);
51 return (double)count / noRuns;
52}
53
54TEST(DftSimulatorTest, AndUnreliability) {
55 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/and.dft", 2, 10000);
56 EXPECT_NEAR(result, 0.3995764009, 0.01);
57}
58
59TEST(DftSimulatorTest, OrUnreliability) {
60 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/or.dft", 1, 10000);
61 EXPECT_NEAR(result, 0.6321205588, 0.01);
62}
63
64TEST(DftSimulatorTest, VotingUnreliability) {
65 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting.dft", 1, 10000);
66 EXPECT_NEAR(result, 0.4511883639, 0.01);
67 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft", 1, 10000);
68 EXPECT_NEAR(result, 0.8173164759, 0.01);
69 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft", 1, 10000);
70 EXPECT_NEAR(result, 0.3496529873, 0.01);
71 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft", 1, 10000);
72#if BOOST_VERSION > 106400
73 EXPECT_NEAR(result, 0.693568287, 0.01);
74#else
75 // Older Boost versions yield different value
76 EXPECT_NEAR(result, 0.693568287, 0.015);
77#endif
78}
79
80TEST(DftSimulatorTest, PandUnreliability) {
81 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pand.dft", 1, 10000);
82 EXPECT_NEAR(result, 0.05434443602, 0.01);
83}
84
85TEST(DftSimulatorTest, PorUnreliability) {
86 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/por.dft", 1, 10000);
87 EXPECT_NEAR(result, 0.2753355179, 0.01);
88}
89
90TEST(DftSimulatorTest, FdepUnreliability) {
91 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft", 1, 10000);
92 EXPECT_NEAR(result, 0.7768698399, 0.01);
93 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft", 1, 10000);
94 EXPECT_NEAR(result, 0.3934693403, 0.01);
95 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft", 1, 10000);
96 EXPECT_NEAR(result, 0.329679954, 0.01);
97 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft", 1, 10000);
98 EXPECT_NEAR(result, 0.601280086, 0.01);
99 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft", 1, 10000);
100 EXPECT_NEAR(result, 0.1548181217, 0.01);
101 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/fdep6.dft", 1, 10000);
102 EXPECT_NEAR(result, 0.9985116987, 0.01);
103}
104
105TEST(DftSimulatorTest, PdepUnreliability) {
106 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft", 1, 10000);
107 EXPECT_NEAR(result, 0.2017690905, 0.01);
108 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft", 1, 10000);
109 EXPECT_NEAR(result, 0.2401091405, 0.01);
110 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft", 1, 10000);
111 EXPECT_NEAR(result, 0.2259856274, 0.01);
112 // Example pdep4 contains non-determinism which is not handled in simulation
113 // result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft", 1, 10000);
114 // EXPECT_NEAR(result, 0.008122157897, 0.01);
115}
116
117TEST(DftSimulatorTest, SpareUnreliability) {
118 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare.dft", 1, 10000);
119 EXPECT_NEAR(result, 0.1118530638, 0.01);
120 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft", 1, 10000);
121 EXPECT_NEAR(result, 0.2905027469, 0.01);
122 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft", 1, 10000);
123 EXPECT_NEAR(result, 0.4660673246, 0.01);
124 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft", 1, 10000);
125 EXPECT_NEAR(result, 0.01273070783, 0.01);
126 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft", 1, 10000);
127 EXPECT_NEAR(result, 0.2017690905, 0.01);
128 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft", 1, 10000);
129 EXPECT_NEAR(result, 0.4693712702, 0.01);
130 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft", 1, 10000);
131 EXPECT_NEAR(result, 0.06108774525, 0.01);
132 result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft", 1, 10000);
133 EXPECT_NEAR(result, 0.02686144489, 0.01);
134}
135
136TEST(DftSimulatorTest, SeqUnreliability) {
137 size_t count;
138 size_t invalid;
139 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq.dft", 1, 10000);
140 EXPECT_EQ(invalid, 0ul);
141 double result = (double)count / 10000;
142 EXPECT_NEAR(result, 0.09020401043, 0.01);
143 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq2.dft", 1, 10000);
144 EXPECT_EQ(invalid, 0ul);
145 result = (double)count / 10000;
146 EXPECT_NEAR(result, 0.01438767797, 0.01);
147 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq3.dft", 1, 10000);
148 EXPECT_EQ(invalid, 0ul);
149 result = (double)count / 10000;
150 EXPECT_NEAR(result, 0.01438767797, 0.01);
151 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq4.dft", 1, 10000);
152 EXPECT_EQ(invalid, 0ul);
153 result = (double)count / 10000;
154 EXPECT_NEAR(result, 0.01438767797, 0.01);
155 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq5.dft", 1, 10000);
156 EXPECT_EQ(invalid, 0ul);
157 result = (double)count / 10000;
158 EXPECT_EQ(result, 0);
159 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/seq6.dft", 1, 10000);
160 EXPECT_EQ(invalid, 0ul);
161 result = (double)count / 10000;
162 EXPECT_NEAR(result, 2.499875004e-09, 0.01);
163}
164
165TEST(DftSimulatorTest, MutexUnreliability) {
166 size_t count;
167 size_t invalid;
168 // Invalid states are currently not supported
169 STORM_SILENT_EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex.dft", 1, 10000), storm::exceptions::NotSupportedException);
170 // EXPECT_GE(invalid, 0);
171 // double result = (double) count / (10000 - invalid);
172 // EXPECT_NEAR(result, 0.8646647168, 0.01);
173 STORM_SILENT_EXPECT_THROW(simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex2.dft", 1, 10000), storm::exceptions::NotSupportedException);
174 // EXPECT_EQ(invalid, 10000);
175 // EXPECT_EQ(count, 0);
176 std::tie(count, invalid) = simulateDft(STORM_TEST_RESOURCES_DIR "/dft/mutex3.dft", 1, 10000);
177 EXPECT_EQ(invalid, 0ul);
178 EXPECT_EQ(count, 0ul);
179}
180
181TEST(DftSimulatorTest, SymmetryUnreliability) {
182 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/symmetry6.dft", 1, 10000);
183 EXPECT_NEAR(result, 0.3421934224, 0.01);
184}
185
186TEST(DftSimulatorTest, HecsUnreliability) {
187 double result = simulateDftProb(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1, 10000);
188 EXPECT_NEAR(result, 0.00021997582, 0.001);
189}
190
191} // namespace
TEST
TEST(OrderTest, Simple)
Definition OrderTest.cpp:8
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::simulator::SimulationTraceResult
SimulationTraceResult
Result of a simulation trace.
Definition DFTTraceSimulator.h:23
storm::pomdp::count
std::pair< storm::RationalNumber, storm::RationalNumber > count(std::vector< storm::storage::BitVector > const &origSets, std::vector< storm::storage::BitVector > const &intersects, std::vector< storm::storage::BitVector > const &intersectsInfo, storm::RationalNumber val, bool plus, uint64_t remdepth)
Definition WinningRegion.cpp:175
storm_gtest.h
STORM_SILENT_EXPECT_THROW
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)
Definition storm_gtest.h:104