Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftTraceGeneratorTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
9
10namespace {
11
12// Configurations for DFT traces
13struct DftTracesConfig {
14 bool useDC;
15 bool useSR;
16};
17
18class NoOptimizationsConfig {
19 public:
20 typedef double ValueType;
21
22 static DftTracesConfig createConfig() {
23 return DftTracesConfig{false, false};
24 }
25};
26
27class DontCareConfig {
28 public:
29 typedef double ValueType;
30
31 static DftTracesConfig createConfig() {
32 return DftTracesConfig{true, false};
33 }
34};
35
36class SymmetryReductionConfig {
37 public:
38 typedef double ValueType;
39
40 static DftTracesConfig createConfig() {
41 return DftTracesConfig{false, true};
42 }
43};
44
45class AllOptimizationsConfig {
46 public:
47 typedef double ValueType;
48
49 static DftTracesConfig createConfig() {
50 return DftTracesConfig{true, true};
51 }
52};
53
54// General base class for testing of generating DFT traces.
55template<typename TestType>
56class DftTraceGeneratorTest : public ::testing::Test {
57 public:
58 typedef typename TestType::ValueType ValueType;
59
60 DftTraceGeneratorTest() : config(TestType::createConfig()) {}
61
62 DftTracesConfig const& getConfig() const {
63 return config;
64 }
65
66 std::pair<std::shared_ptr<storm::dft::storage::DFT<double>>, storm::dft::storage::DFTStateGenerationInfo> prepareDFT(std::string const& file) {
67 // Load, build and prepare DFT
68 std::shared_ptr<storm::dft::storage::DFT<double>> dft =
69 storm::dft::api::prepareForMarkovAnalysis<double>(*(storm::dft::api::loadDFTGalileoFile<double>(file)));
70 EXPECT_TRUE(storm::dft::api::isWellFormed(*dft).first);
71
72 // Compute relevant events
73 std::vector<std::string> relevantNames;
74 if (!config.useDC) {
75 relevantNames.push_back("all");
76 }
78 dft->setRelevantEvents(relevantEvents, false);
79
80 // Find symmetries
82 if (config.useSR) {
84 }
85 storm::dft::storage::DFTStateGenerationInfo stateGenerationInfo(dft->buildStateGenerationInfo(symmetries));
86 return std::make_pair(dft, stateGenerationInfo);
87 }
88
89 private:
90 DftTracesConfig config;
91};
92
93typedef ::testing::Types<NoOptimizationsConfig, DontCareConfig, SymmetryReductionConfig, AllOptimizationsConfig> TestingTypes;
94
95TYPED_TEST_SUITE(DftTraceGeneratorTest, TestingTypes, );
96
97TYPED_TEST(DftTraceGeneratorTest, And) {
98 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
99 auto dft = pair.first;
100 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
101 storm::dft::generator::DftNextStateGenerator<double> generator(*dft, pair.second);
102
103 // Start with initial state
104 auto state = generator.createInitialState();
105 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
106
107 bool changed = state->orderBySymmetry();
108 EXPECT_FALSE(changed);
109
110 // Let C fail
111 auto iterFailable = state->getFailableElements().begin();
112 ASSERT_NE(iterFailable, state->getFailableElements().end());
113 ++iterFailable;
114 ASSERT_NE(iterFailable, state->getFailableElements().end());
115 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
116
117 auto nextBE = iterFailable.asBE(*dft);
118 EXPECT_EQ(nextBE->name(), "C");
119 state = generator.createSuccessorState(state, nextBE);
120 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
121 changed = state->orderBySymmetry();
122 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, changed);
123 if (this->getConfig().useSR && this->getConfig().useDC) {
124 EXPECT_TRUE(state->hasFailed(0));
125 } else {
126 EXPECT_TRUE(state->hasFailed(1));
127 }
128
129 // Let B fail
130 iterFailable = state->getFailableElements().begin();
131 ASSERT_NE(iterFailable, state->getFailableElements().end());
132 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
133
134 nextBE = iterFailable.asBE(*dft);
135 if (this->getConfig().useSR && this->getConfig().useDC) {
136 // TODO: Apply symmetry to failable elements as well
137 return;
138 EXPECT_EQ(nextBE->name(), "C");
139 } else {
140 EXPECT_EQ(nextBE->name(), "B");
141 }
142 state = generator.createSuccessorState(state, nextBE);
143 changed = state->orderBySymmetry();
144 EXPECT_FALSE(changed);
145 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
146}
147
148TYPED_TEST(DftTraceGeneratorTest, RandomStepsAnd) {
149 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
150 auto dft = pair.first;
151 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
152
153 // Init random number generator
154 boost::mt19937 gen(5u);
155 storm::dft::simulator::DFTTraceSimulator<double> simulator(*dft, pair.second, gen);
156
157 auto state = simulator.getCurrentState();
158 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
159
160 // First random step
161 storm::dft::simulator::SimulationStepResult res = simulator.randomStep();
163#if BOOST_VERSION > 106400
164 // Older Boost versions yield different value
165 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6);
166#endif
167 state = simulator.getCurrentState();
168 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
169
170 res = simulator.randomStep();
172#if BOOST_VERSION > 106400
173 // Older Boost versions yield different value
174 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6);
175#endif
176 state = simulator.getCurrentState();
177 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
178}
179
180TYPED_TEST(DftTraceGeneratorTest, Reset) {
181 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
182 auto dft = pair.first;
183 EXPECT_EQ(this->getConfig().useSR && this->getConfig().useDC, pair.second.hasSymmetries());
184
185 // Init random number generator
186 boost::mt19937 gen(5u);
187 storm::dft::simulator::DFTTraceSimulator<double> simulator(*dft, pair.second, gen);
188
189 auto state = simulator.getCurrentState();
190 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
191
192 // First random step
193 storm::dft::simulator::SimulationStepResult res = simulator.randomStep();
195#if BOOST_VERSION > 106400
196 // Older Boost versions yield different value
197 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079, 1e-6);
198#endif
199 auto stateStep1 = simulator.getCurrentState();
200 EXPECT_FALSE(stateStep1->hasFailed(dft->getTopLevelIndex()));
201
202 res = simulator.randomStep();
204#if BOOST_VERSION > 106400
205 // Older Boost versions yield different value
206 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214, 1e-6);
207#endif
208 state = simulator.getCurrentState();
209 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
210
211 // Reset to previous state
212 simulator.resetToState(stateStep1);
213 state = simulator.getCurrentState();
214 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
215
216 res = simulator.randomStep();
218#if BOOST_VERSION > 106400
219 // Older Boost versions yield different value
220 EXPECT_NEAR(simulator.getCurrentTime(), 0.522079 + 0.9497214 + 2.4686932, 1e-6);
221#endif
222 state = simulator.getCurrentState();
223 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
224}
225
226TYPED_TEST(DftTraceGeneratorTest, Fdep) {
227 auto pair = this->prepareDFT(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
228 auto dft = pair.first;
229
230 // Init random number generator. Will not be important as we are choosing the steps deterministically.
231 boost::mt19937 gen(5u);
232 storm::dft::simulator::DFTTraceSimulator<double> simulator(*dft, pair.second, gen);
233
234 // Start with initial state
235 auto state = simulator.getCurrentState();
236 EXPECT_FALSE(state->hasFailed(dft->getTopLevelIndex()));
237
238 // Let B_Power fail
239 auto iterFailable = state->getFailableElements().begin();
240 ASSERT_NE(iterFailable, state->getFailableElements().end());
241 ++iterFailable;
242 ASSERT_NE(iterFailable, state->getFailableElements().end());
243 ++iterFailable;
244 ASSERT_NE(iterFailable, state->getFailableElements().end());
245
246 EXPECT_FALSE(iterFailable.isFailureDueToDependency());
247 auto nextBE = iterFailable.asBE(*dft);
248 EXPECT_EQ(nextBE->name(), "B_Power");
249
250 storm::dft::simulator::SimulationStepResult res = simulator.step(iterFailable);
252 state = simulator.getCurrentState();
253 EXPECT_TRUE(state->hasFailed(4));
254
255 // Let B fail
256 iterFailable = state->getFailableElements().begin();
257 ASSERT_NE(iterFailable, state->getFailableElements().end());
258 ++iterFailable;
259 ASSERT_NE(iterFailable, state->getFailableElements().end());
260
261 EXPECT_TRUE(iterFailable.isFailureDueToDependency());
262 auto dependency = iterFailable.asDependency(*dft);
263 EXPECT_EQ(dependency->dependentEvents().front()->name(), "B");
264
265 res = simulator.step(iterFailable);
267 state = simulator.getCurrentState();
268 EXPECT_TRUE(state->hasFailed(dft->getTopLevelIndex()));
269}
270
271} // namespace
static storm::dft::storage::DftSymmetries findSymmetries(storm::dft::storage::DFT< ValueType > const &dft)
Find symmetries in the given DFT.
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:63
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.
SFTBDDChecker::ValueType ValueType
SimulationStepResult
Result of a single simulation step.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
Definition GraphTest.cpp:62
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
Definition GraphTest.cpp:59