Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
DftToGspnTransformator.cpp
Go to the documentation of this file.
1#include "DftToGspnTransformator.h"
2#include <memory>
3#include "storm/exceptions/NotImplementedException.h"
4
5namespace storm::dft {
6namespace transformations {
7
8// Prevent some magic constants
9static constexpr const uint64_t defaultCapacity = 1;
10
11template<typename ValueType>
12DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::dft::storage::DFT<ValueType> const &dft) : mDft(dft) {
13 // Intentionally left empty.
14}
15
16template<typename ValueType>
17void DftToGspnTransformator<ValueType>::transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart,
18 bool mergeDCFailed, bool extendPriorities) {
19 this->priorities = priorities;
20 this->dontCareElements = dontCareElements;
21 this->smart = smart;
22 this->mergedDCFailed = mergeDCFailed;
23 this->dontCarePriority = 1;
24 this->extendedPriorities = extendPriorities;
25 builder.setGspnName("DftToGspnTransformation");
26
27 // Translate all GSPN elements
28 translateGSPNElements();
29
30 // Create initial template
31 // TODO
32}
33
34template<typename ValueType>
35std::map<uint64_t, uint64_t> DftToGspnTransformator<ValueType>::computePriorities(bool extendedPrio) {
36 std::map<uint64_t, uint64_t> priorities;
37 if (!extendedPrio) {
38 // Set priority for PDEP and FDEP according to Monolithic MA semantics
39 uint64_t dependency_priority = 2;
40 for (std::size_t i = 0; i < mDft.nrElements(); i++) {
41 if (mDft.getElement(i)->type() == storm::dft::storage::elements::DFTElementType::PDEP)
42 priorities[i] = dependency_priority;
43 else
44 priorities[i] = (-(mDft.getElement(i)->rank()) + mDft.maxRank()) * 2 + 5;
45 }
46 } else {
47 // Define some variables
48 u_int64_t maxNrOfChildren = 0;
49 u_int64_t maxNrDependentEvents = 0;
50 // Iterate over all elements of the DFT and sort them into the list
51 std::list<size_t> elementList;
52 for (std::size_t i = 0; i < mDft.nrElements(); i++) {
53 if (mDft.getElement(i)->type() == storm::dft::storage::elements::DFTElementType::PDEP) {
54 // For dependencies, get the maximal number of dependent events
55 auto dependency = std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType> const>(mDft.getElement(i));
56 uint64_t nrDependentEvents = (dependency->dependentEvents()).size();
57 if (nrDependentEvents > maxNrDependentEvents) {
58 maxNrDependentEvents = nrDependentEvents;
59 }
60 }
61 // Get the maximum number of children/ SPAREs need additional transitions
62
63 u_int64_t nrChildren = mDft.getElement(i)->nrChildren();
64 if (mDft.getElement(i)->type() == storm::dft::storage::elements::DFTElementType::SPARE) {
65 nrChildren *= 4;
66 }
67 if (maxNrOfChildren < nrChildren) {
68 maxNrOfChildren = nrChildren;
69 }
70 // Organize the elements according to their rank
71 if (!elementList.empty()) {
72 std::list<size_t>::iterator it = elementList.begin();
73 // Make sure dependencies are always in the front
74 while ((mDft.getElement(*it)->rank()) < (mDft.getElement(i)->rank()) ||
75 mDft.getElement(*it)->type() == storm::dft::storage::elements::DFTElementType::PDEP) {
76 it++;
77 }
78 elementList.insert(it, i);
79 } else {
80 elementList.push_back(i);
81 }
82 }
83 // Get the necessary length for priority intervals
84 // Note that additional priorities are necessary
85 u_int64_t priorityIntervalLength = std::max(maxNrDependentEvents, maxNrOfChildren) + 4;
86
87 // Define a running variable for the current priority
88 // Initialize it with an offset for the DC priorities + first interval length as prios give upper interval limit
89 u_int64_t currentPrio = mDft.nrElements() + priorityIntervalLength;
90 // TODO Dependencies have to have same priority
91 for (std::list<size_t>::iterator it = elementList.begin(); it != elementList.end(); ++it) {
92 priorities[*it] = currentPrio;
93 currentPrio += priorityIntervalLength;
94 }
95 }
96
97 return priorities;
98}
99
100template<typename ValueType>
101uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
102 STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist.");
103 return failedPlaces.at(mDft.getTopLevelIndex());
104}
105
106template<typename ValueType>
107gspn::GSPN *DftToGspnTransformator<ValueType>::obtainGSPN() {
108 return builder.buildGspn();
109}
110
111template<typename ValueType>
112void DftToGspnTransformator<ValueType>::translateGSPNElements() {
113 // Loop through every DFT element and create its corresponding GSPN template.
114 for (std::size_t i = 0; i < mDft.nrElements(); i++) {
115 auto dftElement = mDft.getElement(i);
116
117 // Check which type the element is and call the corresponding translate-function.
118 switch (dftElement->type()) {
119 case storm::dft::storage::elements::DFTElementType::BE:
120 translateBE(std::static_pointer_cast<storm::dft::storage::elements::DFTBE<ValueType> const>(dftElement));
121 break;
122 case storm::dft::storage::elements::DFTElementType::AND:
123 translateAND(std::static_pointer_cast<storm::dft::storage::elements::DFTAnd<ValueType> const>(dftElement));
124 break;
125 case storm::dft::storage::elements::DFTElementType::OR:
126 translateOR(std::static_pointer_cast<storm::dft::storage::elements::DFTOr<ValueType> const>(dftElement));
127 break;
128 case storm::dft::storage::elements::DFTElementType::VOT:
129 translateVOT(std::static_pointer_cast<storm::dft::storage::elements::DFTVot<ValueType> const>(dftElement));
130 break;
131 case storm::dft::storage::elements::DFTElementType::PAND:
132 translatePAND(std::static_pointer_cast<storm::dft::storage::elements::DFTPand<ValueType> const>(dftElement),
133 std::static_pointer_cast<storm::dft::storage::elements::DFTPand<ValueType> const>(dftElement)->isInclusive());
134 break;
135 case storm::dft::storage::elements::DFTElementType::POR:
136 translatePOR(std::static_pointer_cast<storm::dft::storage::elements::DFTPor<ValueType> const>(dftElement),
137 std::static_pointer_cast<storm::dft::storage::elements::DFTPor<ValueType> const>(dftElement)->isInclusive());
138 break;
139 case storm::dft::storage::elements::DFTElementType::SPARE:
140 translateSPARE(std::static_pointer_cast<storm::dft::storage::elements::DFTSpare<ValueType> const>(dftElement));
141 break;
142 case storm::dft::storage::elements::DFTElementType::PDEP:
143 translatePDEP(std::static_pointer_cast<storm::dft::storage::elements::DFTDependency<ValueType> const>(dftElement));
144 break;
145 case storm::dft::storage::elements::DFTElementType::SEQ:
146 translateSeq(std::static_pointer_cast<storm::dft::storage::elements::DFTSeq<ValueType> const>(dftElement));
147 break;
148 default:
149 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "DFT type '" << dftElement->type() << "' not known.");
150 break;
151 }
152 }
153}
154
155template<typename ValueType>
156void DftToGspnTransformator<ValueType>::translateBE(std::shared_ptr<storm::dft::storage::elements::DFTBE<ValueType> const> dftBE) {
157 switch (dftBE->beType()) {
158 case storm::dft::storage::elements::BEType::CONSTANT:
159 translateBEConst(std::static_pointer_cast<storm::dft::storage::elements::BEConst<ValueType> const>(dftBE));
160 break;
161 case storm::dft::storage::elements::BEType::EXPONENTIAL:
162 translateBEExponential(std::static_pointer_cast<storm::dft::storage::elements::BEExponential<ValueType> const>(dftBE));
163 break;
164 default:
165 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE type '" << dftBE->beType() << "' not known.");
166 break;
167 }
168}
169
170template<typename ValueType>
171void DftToGspnTransformator<ValueType>::translateBEExponential(std::shared_ptr<storm::dft::storage::elements::BEExponential<ValueType> const> dftBE) {
172 double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
173 double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
174
175 uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
176
177 uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
178 activePlaces.emplace(dftBE->id(), activePlace);
179 builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter));
180 uint64_t tActive = builder.addTimedTransition(getFailPriority(dftBE), dftBE->activeFailureRate(), dftBE->name() + "_activeFailing");
181 builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
182 builder.addInputArc(activePlace, tActive);
183 builder.addInhibitionArc(failedPlace, tActive);
184 builder.addOutputArc(tActive, activePlace);
185 builder.addOutputArc(tActive, failedPlace);
186
187 uint64_t tPassive = builder.addTimedTransition(getFailPriority(dftBE), dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing");
188 builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
189 builder.addInhibitionArc(activePlace, tPassive);
190 builder.addInhibitionArc(failedPlace, tPassive);
191 builder.addOutputArc(tPassive, failedPlace);
192
193 if (dontCareElements.count(dftBE->id()) && dftBE->id() != mDft.getTopLevelIndex()) {
194 u_int64_t tDontCare = addDontcareTransition(dftBE, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter));
195 if (!mergedDCFailed) {
196 uint64_t dontCarePlace = builder.addPlace(1, 0, dftBE->name() + STR_DONTCARE);
197 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0));
198 builder.addInhibitionArc(dontCarePlace, tDontCare);
199 builder.addOutputArc(tDontCare, dontCarePlace);
200
201 builder.addInhibitionArc(dontCarePlace, tActive);
202 builder.addInhibitionArc(dontCarePlace, tPassive);
203
204 // Propagation for dependencies
205 if (!smart || dftBE->hasIngoingDependencies()) {
206 uint64_t dependencyPropagationPlace = builder.addPlace(1, 0, dftBE->name() + "_dependency_prop");
207 dependencyPropagationPlaces.emplace(dftBE->id(), dependencyPropagationPlace);
208 builder.setPlaceLayoutInfo(dependencyPropagationPlace, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 5.0));
209 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftBE->name() + "_prop_fail");
210 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter));
211 builder.addInhibitionArc(dependencyPropagationPlace, tPropagationFailed);
212 builder.addInputArc(failedPlace, tPropagationFailed);
213 builder.addOutputArc(tPropagationFailed, failedPlace);
214 builder.addOutputArc(tPropagationFailed, dependencyPropagationPlace);
215 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftBE->name() + "_prop_dontCare");
216 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter));
217 builder.addInhibitionArc(dependencyPropagationPlace, tPropagationDontCare);
218 builder.addInputArc(dependencyPropagationPlace, tPropagationDontCare);
219 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
220 builder.addOutputArc(tPropagationDontCare, dependencyPropagationPlace);
221 }
222 } else {
223 builder.addInhibitionArc(failedPlace, tDontCare);
224 builder.addOutputArc(tDontCare, failedPlace);
225 }
226 }
227
228 if (!smart || dftBE->nrRestrictions() > 0) {
229 uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter - 9.0, ycenter));
230 builder.addInhibitionArc(disabledPlace, tActive);
231 builder.addInhibitionArc(disabledPlace, tPassive);
232 }
233
234 if (!smart || mDft.isRepresentative(dftBE->id())) {
235 uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter));
236 builder.addOutputArc(tActive, unavailablePlace);
237 builder.addOutputArc(tPassive, unavailablePlace);
238 }
239
240 if (extendedPriorities)
241 dontCarePriority++;
242}
243
244template<typename ValueType>
245void DftToGspnTransformator<ValueType>::translateBEConst(std::shared_ptr<storm::dft::storage::elements::BEConst<ValueType> const> dftConst) {
246 double xcenter = mDft.getElementLayoutInfo(dftConst->id()).x;
247 double ycenter = mDft.getElementLayoutInfo(dftConst->id()).y;
248
249 if (dftConst->failed()) {
250 // Constant failed BE
251 addFailedPlace(dftConst, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0), true);
252
253 if (!smart || mDft.isRepresentative(dftConst->id())) {
254 addUnavailablePlace(dftConst, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0), false);
255 }
256 } else {
257 // Constant failsafe BE
258 size_t capacity = 0; // It cannot contain a token, because it cannot fail.
259 uint64_t failedPlace = builder.addPlace(capacity, 0, dftConst->name() + STR_FAILED);
260 assert(failedPlaces.size() == dftConst->id());
261 failedPlaces.push_back(failedPlace);
262 builder.setPlaceLayoutInfo(failedPlace, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
263
264 if (!smart || mDft.isRepresentative(dftConst->id())) {
265 uint64_t unavailablePlace = builder.addPlace(capacity, 0, dftConst->name() + "_unavail");
266 unavailablePlaces.emplace(dftConst->id(), unavailablePlace);
267 builder.setPlaceLayoutInfo(unavailablePlace, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
268 }
269 }
270}
271
272template<typename ValueType>
273void DftToGspnTransformator<ValueType>::translateAND(std::shared_ptr<storm::dft::storage::elements::DFTAnd<ValueType> const> dftAnd) {
274 double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
275 double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
276
277 uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
278
279 uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING);
280 builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
281 builder.addInhibitionArc(failedPlace, tFailed);
282 builder.addOutputArc(tFailed, failedPlace);
283
284 if (dontCareElements.count(dftAnd->id())) {
285 if (dftAnd->id() != mDft.getTopLevelIndex()) {
286 u_int64_t tDontCare = addDontcareTransition(dftAnd, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
287 if (!mergedDCFailed) {
288 uint64_t dontCarePlace = builder.addPlace(1, 0, dftAnd->name() + STR_DONTCARE);
289 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
290 builder.addInhibitionArc(dontCarePlace, tDontCare);
291 builder.addOutputArc(tDontCare, dontCarePlace);
292 // Propagation
293 uint64_t propagationPlace = builder.addPlace(1, 0, dftAnd->name() + "_prop");
294 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
295 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftAnd->name() + "_prop_fail");
296 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
297 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
298 builder.addInputArc(failedPlace, tPropagationFailed);
299 builder.addOutputArc(tPropagationFailed, failedPlace);
300 builder.addOutputArc(tPropagationFailed, propagationPlace);
301 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftAnd->name() + "_prop_dontCare");
302 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
303 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
304 builder.addInputArc(dontCarePlace, tPropagationDontCare);
305 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
306 builder.addOutputArc(tPropagationDontCare, propagationPlace);
307 for (auto const &child : dftAnd->children()) {
308 if (dontCareElements.count(child->id())) {
309 u_int64_t childDontCare = dontcareTransitions.at(child->id());
310 builder.addInputArc(propagationPlace, childDontCare);
311 builder.addOutputArc(childDontCare, propagationPlace);
312 }
313 }
314 } else {
315 builder.addInhibitionArc(failedPlace, tDontCare);
316 builder.addOutputArc(tDontCare, failedPlace);
317 for (auto const &child : dftAnd->children()) {
318 if (dontCareElements.count(child->id())) {
319 u_int64_t childDontCare = dontcareTransitions.at(child->id());
320 builder.addInputArc(failedPlace, childDontCare);
321 builder.addOutputArc(childDontCare, failedPlace);
322 }
323 }
324 }
325 } else {
326 // If AND is TLE, simple failure propagation suffices
327 for (auto const &child : dftAnd->children()) {
328 if (dontCareElements.count(child->id())) {
329 u_int64_t childDontCare = dontcareTransitions.at(child->id());
330 builder.addInputArc(failedPlace, childDontCare);
331 builder.addOutputArc(childDontCare, failedPlace);
332 }
333 }
334 }
335 }
336
337 if (!smart || mDft.isRepresentative(dftAnd->id())) {
338 uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
339 builder.addOutputArc(tFailed, unavailablePlace);
340 }
341
342 for (auto const &child : dftAnd->children()) {
343 builder.addInputArc(getFailedPlace(child), tFailed);
344 builder.addOutputArc(tFailed, getFailedPlace(child));
345 }
346 if (extendedPriorities)
347 dontCarePriority++;
348}
349
350template<typename ValueType>
351void DftToGspnTransformator<ValueType>::translateOR(std::shared_ptr<storm::dft::storage::elements::DFTOr<ValueType> const> dftOr) {
352 double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x;
353 double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y;
354
355 uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
356
357 if (dontCareElements.count(dftOr->id())) {
358 if (dftOr->id() != mDft.getTopLevelIndex()) {
359 u_int64_t tDontCare = addDontcareTransition(dftOr, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
360 if (!mergedDCFailed) {
361 uint64_t dontCarePlace = builder.addPlace(1, 0, dftOr->name() + STR_DONTCARE);
362 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
363 builder.addInhibitionArc(dontCarePlace, tDontCare);
364 builder.addOutputArc(tDontCare, dontCarePlace);
365 // Propagation
366 uint64_t propagationPlace = builder.addPlace(1, 0, dftOr->name() + "_prop");
367 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
368 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftOr->name() + "_prop_fail");
369 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
370 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
371 builder.addInputArc(failedPlace, tPropagationFailed);
372 builder.addOutputArc(tPropagationFailed, failedPlace);
373 builder.addOutputArc(tPropagationFailed, propagationPlace);
374 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftOr->name() + "_prop_dontCare");
375 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
376 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
377 builder.addInputArc(dontCarePlace, tPropagationDontCare);
378 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
379 builder.addOutputArc(tPropagationDontCare, propagationPlace);
380 for (auto const &child : dftOr->children()) {
381 if (dontCareElements.count(child->id())) {
382 u_int64_t childDontCare = dontcareTransitions.at(child->id());
383 builder.addInputArc(propagationPlace, childDontCare);
384 builder.addOutputArc(childDontCare, propagationPlace);
385 }
386 }
387 } else {
388 builder.addInhibitionArc(failedPlace, tDontCare);
389 builder.addOutputArc(tDontCare, failedPlace);
390 for (auto const &child : dftOr->children()) {
391 if (dontCareElements.count(child->id())) {
392 u_int64_t childDontCare = dontcareTransitions.at(child->id());
393 builder.addInputArc(failedPlace, childDontCare);
394 builder.addOutputArc(childDontCare, failedPlace);
395 }
396 }
397 }
398 } else {
399 // If OR is TLE, simple failure propagation suffices
400 for (auto const &child : dftOr->children()) {
401 if (dontCareElements.count(child->id())) {
402 u_int64_t childDontCare = dontcareTransitions.at(child->id());
403 builder.addInputArc(failedPlace, childDontCare);
404 builder.addOutputArc(childDontCare, failedPlace);
405 }
406 }
407 }
408 }
409
410 bool isRepresentative = mDft.isRepresentative(dftOr->id());
411 uint64_t unavailablePlace = 0;
412 if (!smart || isRepresentative) {
413 unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
414 }
415
416 for (size_t i = 0; i < dftOr->nrChildren(); ++i) {
417 auto const &child = dftOr->children().at(i);
418 uint64_t tFailed = 0;
419 if (extendedPriorities)
420 tFailed = builder.addImmediateTransition(getFailPriority(dftOr) + i, 0.0, dftOr->name() + STR_FAILING + std::to_string(i));
421 else
422 tFailed = builder.addImmediateTransition(getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i));
423 builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
424 builder.addInhibitionArc(failedPlace, tFailed);
425 builder.addOutputArc(tFailed, failedPlace);
426 if (!smart || isRepresentative) {
427 builder.addOutputArc(tFailed, unavailablePlace);
428 }
429 builder.addInputArc(getFailedPlace(child), tFailed);
430 builder.addOutputArc(tFailed, getFailedPlace(child));
431 }
432 if (extendedPriorities)
433 dontCarePriority++;
434}
435
436template<typename ValueType>
437void DftToGspnTransformator<ValueType>::translateVOT(std::shared_ptr<storm::dft::storage::elements::DFTVot<ValueType> const> dftVot) {
438 // TODO: finish layouting
439
440 double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x;
441 double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y;
442
443 uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
444
445 uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
446 builder.addOutputArc(tFailed, failedPlace);
447 builder.addInhibitionArc(failedPlace, tFailed);
448
449 if (!smart || mDft.isRepresentative(dftVot->id())) {
450 uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
451 builder.addOutputArc(tFailed, unavailablePlace);
452 }
453
454 uint64_t collectorPlace = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector");
455 builder.setPlaceLayoutInfo(collectorPlace, storm::gspn::LayoutInfo(xcenter, ycenter));
456 builder.addInputArc(collectorPlace, tFailed, dftVot->threshold());
457
458 for (size_t i = 0; i < dftVot->nrChildren(); ++i) {
459 auto const &child = dftVot->children().at(i);
460 uint64_t childNextPlace = builder.addPlace(defaultCapacity, 1, dftVot->name() + "_child_next" + std::to_string(i));
461 uint64_t tCollect;
462 if (extendedPriorities)
463 tCollect = builder.addImmediateTransition(getFailPriority(dftVot) + i, 0.0, dftVot->name() + "_child_collect" + std::to_string(i));
464 else
465 tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i));
466 builder.addOutputArc(tCollect, collectorPlace);
467 builder.addInputArc(childNextPlace, tCollect);
468 builder.addInputArc(getFailedPlace(child), tCollect);
469 builder.addOutputArc(tCollect, getFailedPlace(child));
470 }
471
472 if (dontCareElements.count(dftVot->id())) {
473 if (dftVot->id() != mDft.getTopLevelIndex()) {
474 u_int64_t tDontCare = addDontcareTransition(dftVot, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
475 if (!mergedDCFailed) {
476 uint64_t dontCarePlace = builder.addPlace(1, 0, dftVot->name() + STR_DONTCARE);
477 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
478 builder.addInhibitionArc(dontCarePlace, tDontCare);
479 builder.addOutputArc(tDontCare, dontCarePlace);
480 // Propagation
481 uint64_t propagationPlace = builder.addPlace(1, 0, dftVot->name() + "_prop");
482 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
483 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftVot->name() + "_prop_fail");
484 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
485 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
486 builder.addInputArc(failedPlace, tPropagationFailed);
487 builder.addOutputArc(tPropagationFailed, failedPlace);
488 builder.addOutputArc(tPropagationFailed, propagationPlace);
489 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftVot->name() + "_prop_dontCare");
490 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
491 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
492 builder.addInputArc(dontCarePlace, tPropagationDontCare);
493 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
494 builder.addOutputArc(tPropagationDontCare, propagationPlace);
495 for (auto const &child : dftVot->children()) {
496 if (dontCareElements.count(child->id())) {
497 u_int64_t childDontCare = dontcareTransitions.at(child->id());
498 builder.addInputArc(propagationPlace, childDontCare);
499 builder.addOutputArc(childDontCare, propagationPlace);
500 }
501 }
502 } else {
503 builder.addInhibitionArc(failedPlace, tDontCare);
504 builder.addOutputArc(tDontCare, failedPlace);
505 for (auto const &child : dftVot->children()) {
506 if (dontCareElements.count(child->id())) {
507 u_int64_t childDontCare = dontcareTransitions.at(child->id());
508 builder.addInputArc(failedPlace, childDontCare);
509 builder.addOutputArc(childDontCare, failedPlace);
510 }
511 }
512 }
513 } else {
514 // If VOT is TLE, simple failure propagation suffices
515 for (auto const &child : dftVot->children()) {
516 if (dontCareElements.count(child->id())) {
517 u_int64_t childDontCare = dontcareTransitions.at(child->id());
518 builder.addInputArc(failedPlace, childDontCare);
519 builder.addOutputArc(childDontCare, failedPlace);
520 }
521 }
522 }
523 }
524 if (extendedPriorities)
525 dontCarePriority++;
526}
527
528template<typename ValueType>
529void DftToGspnTransformator<ValueType>::translatePAND(std::shared_ptr<storm::dft::storage::elements::DFTPand<ValueType> const> dftPand, bool inclusive) {
530 // TODO Layouting
531 double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x;
532 double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y;
533
534 uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
535
536 // Set priority lower if the PAND is exclusive
537 uint64_t tFailed = builder.addImmediateTransition(
538 /*inclusive ? getFailPriority(dftPand) : */ getFailPriority(dftPand) - 1, 0.0, dftPand->name() + STR_FAILING);
539 builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
540 builder.addInhibitionArc(failedPlace, tFailed);
541 builder.addOutputArc(tFailed, failedPlace);
542
543 if (!smart || mDft.isRepresentative(dftPand->id())) {
544 uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
545 builder.addOutputArc(tFailed, unavailablePlace);
546 }
547
548 uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
549 builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter - 3.0));
550
551 builder.addInhibitionArc(failSafePlace, tFailed);
552
553 // Transitions for failed place
554 for (auto const &child : dftPand->children()) {
555 builder.addInputArc(getFailedPlace(child), tFailed);
556 builder.addOutputArc(tFailed, getFailedPlace(child));
557 }
558 // Transitions for fail-safe place
559 for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) {
560 auto const &child = dftPand->children().at(i);
561 uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(i));
562 builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter - 6.0 + i * 3.0, ycenter + 3.0));
563
564 if (inclusive) {
565 builder.addInputArc(getFailedPlace(child), tFailSafe);
566 builder.addOutputArc(tFailSafe, getFailedPlace(child));
567 builder.addInhibitionArc(getFailedPlace(dftPand->children().at(i - 1)), tFailSafe);
568 builder.addOutputArc(tFailSafe, failSafePlace);
569 builder.addInhibitionArc(failSafePlace, tFailSafe);
570 } else {
571 // Delay mechanism for exclusive PAND
572 auto const &previousChild = dftPand->children().at(i - 1);
573 uint64_t delayPlace = builder.addPlace(1, 0, dftPand->name() + "_delay_" + previousChild->name());
574 builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0 + (i - 1) * 3.0, ycenter + 5.0));
575 // Priority of delayTransitions needs to be lower than for failsafeTransitions
576 uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPand) - 1, 0.0, child->name() + "_" + dftPand->name() + "_delayTransition");
577 builder.setTransitionLayoutInfo(tDelay, storm::gspn::LayoutInfo(xcenter - 5.0 + (i - 1) * 3.0, ycenter + 3.0));
578 builder.addInputArc(getFailedPlace(previousChild), tDelay);
579 builder.addOutputArc(tDelay, getFailedPlace(dftPand->children().at(i - 1)));
580 builder.addOutputArc(tDelay, delayPlace);
581 builder.addInhibitionArc(delayPlace, tDelay);
582
583 builder.addInputArc(getFailedPlace(child), tFailSafe);
584 builder.addOutputArc(tFailSafe, getFailedPlace(child));
585 builder.addInhibitionArc(delayPlace, tFailSafe);
586 builder.addOutputArc(tFailSafe, failSafePlace);
587 builder.addInhibitionArc(failSafePlace, tFailSafe);
588 }
589 }
590 // Dont Care
591 if (dontCareElements.count(dftPand->id())) {
592 // Propagation
593 uint64_t propagationPlace = builder.addPlace(1, 0, dftPand->name() + "_prop");
594 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
595 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftPand->name() + "_prop_fail");
596 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
597 uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0, dftPand->name() + "_prop_failsafe");
598 builder.setTransitionLayoutInfo(tPropagationFailsafe, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0));
599 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
600 builder.addInputArc(failedPlace, tPropagationFailed);
601 builder.addOutputArc(tPropagationFailed, failedPlace);
602 builder.addOutputArc(tPropagationFailed, propagationPlace);
603
604 builder.addInhibitionArc(propagationPlace, tPropagationFailsafe);
605 builder.addInputArc(failSafePlace, tPropagationFailsafe);
606 builder.addOutputArc(tPropagationFailsafe, failSafePlace);
607 builder.addOutputArc(tPropagationFailsafe, propagationPlace);
608
609 // Connect children to propagation place
610 for (auto const &child : dftPand->children()) {
611 if (dontCareElements.count(child->id())) {
612 u_int64_t childDontCare = dontcareTransitions.at(child->id());
613 builder.addInputArc(propagationPlace, childDontCare);
614 builder.addOutputArc(childDontCare, propagationPlace);
615 }
616 }
617
618 if (dftPand->id() != mDft.getTopLevelIndex()) {
619 u_int64_t tDontCare = addDontcareTransition(dftPand, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
620 if (!mergedDCFailed) {
621 uint64_t dontCarePlace = builder.addPlace(1, 0, dftPand->name() + STR_DONTCARE);
622 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
623 builder.addInhibitionArc(dontCarePlace, tDontCare);
624 builder.addOutputArc(tDontCare, dontCarePlace);
625 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftPand->name() + "_prop_dontCare");
626 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
627 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
628 builder.addInputArc(dontCarePlace, tPropagationDontCare);
629 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
630 builder.addOutputArc(tPropagationDontCare, propagationPlace);
631
632 } else {
633 builder.addInhibitionArc(failedPlace, tDontCare);
634 builder.addOutputArc(tDontCare, failedPlace);
635 }
636 }
637 }
638 if (extendedPriorities)
639 dontCarePriority++;
640}
641
642template<typename ValueType>
643void DftToGspnTransformator<ValueType>::translatePOR(std::shared_ptr<storm::dft::storage::elements::DFTPor<ValueType> const> dftPor, bool inclusive) {
644 double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x;
645 double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y;
646
647 uint64_t delayPlace = 0;
648
649 uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
650
651 // Set priority lower if the POR is exclusive
652 uint64_t tFailed = builder.addImmediateTransition(
653 /*inclusive ? getFailPriority(dftPor) : */ getFailPriority(dftPor) - 1, 0.0, dftPor->name() + STR_FAILING);
654 builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
655 builder.addOutputArc(tFailed, failedPlace);
656 builder.addInhibitionArc(failedPlace, tFailed);
657
658 // Arcs from first child
659 builder.addInputArc(getFailedPlace(dftPor->children().front()), tFailed);
660 builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front()));
661
662 if (!smart || mDft.isRepresentative(dftPor->id())) {
663 uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
664 builder.addOutputArc(tFailed, unavailablePlace);
665 }
666
667 uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE);
668 builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter - 3.0));
669
670 builder.addInhibitionArc(failSafePlace, tFailed);
671
672 if (!inclusive) {
673 // Setup delay mechanism if necessary
674 delayPlace = builder.addPlace(1, 0, dftPor->name() + "_delay");
675 builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 5.0));
676
677 // priority of delayTransition has to be lower than other priorities
678 uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPor) - 1, 0.0, dftPor->name() + "_delayTransition");
679 builder.setTransitionLayoutInfo(tDelay, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 3.0));
680
681 builder.addInputArc(getFailedPlace(dftPor->children().front()), tDelay);
682 builder.addOutputArc(tDelay, getFailedPlace(dftPor->children().front()));
683 builder.addOutputArc(tDelay, delayPlace);
684 builder.addInhibitionArc(delayPlace, tDelay);
685 }
686
687 // For all children except the first one
688 for (size_t i = 1; i < dftPor->nrChildren(); ++i) {
689 auto const &child = dftPor->children().at(i);
690 uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(i));
691 builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter - 3.0 + i * 3.0, ycenter + 3.0));
692
693 builder.addInputArc(getFailedPlace(child), tFailSafe);
694 builder.addOutputArc(tFailSafe, getFailedPlace(child));
695 builder.addOutputArc(tFailSafe, failSafePlace);
696 builder.addInhibitionArc(failSafePlace, tFailSafe);
697 if (inclusive) {
698 builder.addInhibitionArc(getFailedPlace(dftPor->children().front()), tFailSafe);
699 } else {
700 builder.addInhibitionArc(delayPlace, tFailSafe);
701 }
702 }
703
704 // Dont Care
705 if (dontCareElements.count(dftPor->id())) {
706 // Propagation
707 uint64_t propagationPlace = builder.addPlace(1, 0, dftPor->name() + "_prop");
708 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
709 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftPor->name() + "_prop_fail");
710 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
711 uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0, dftPor->name() + "_prop_failsafe");
712 builder.setTransitionLayoutInfo(tPropagationFailsafe, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0));
713 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
714 builder.addInputArc(failedPlace, tPropagationFailed);
715 builder.addOutputArc(tPropagationFailed, failedPlace);
716 builder.addOutputArc(tPropagationFailed, propagationPlace);
717
718 builder.addInhibitionArc(propagationPlace, tPropagationFailsafe);
719 builder.addInputArc(failSafePlace, tPropagationFailsafe);
720 builder.addOutputArc(tPropagationFailsafe, failSafePlace);
721 builder.addOutputArc(tPropagationFailsafe, propagationPlace);
722
723 // Connect children to propagation place
724 for (auto const &child : dftPor->children()) {
725 if (dontCareElements.count(child->id())) {
726 u_int64_t childDontCare = dontcareTransitions.at(child->id());
727 builder.addInputArc(propagationPlace, childDontCare);
728 builder.addOutputArc(childDontCare, propagationPlace);
729 }
730 }
731
732 if (dftPor->id() != mDft.getTopLevelIndex()) {
733 u_int64_t tDontCare = addDontcareTransition(dftPor, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
734 if (!mergedDCFailed) {
735 uint64_t dontCarePlace = builder.addPlace(1, 0, dftPor->name() + STR_DONTCARE);
736 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
737 builder.addInhibitionArc(dontCarePlace, tDontCare);
738 builder.addOutputArc(tDontCare, dontCarePlace);
739 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftPor->name() + "_prop_dontCare");
740 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
741 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
742 builder.addInputArc(dontCarePlace, tPropagationDontCare);
743 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
744 builder.addOutputArc(tPropagationDontCare, propagationPlace);
745
746 } else {
747 builder.addInhibitionArc(failedPlace, tDontCare);
748 builder.addOutputArc(tDontCare, failedPlace);
749 }
750 }
751 }
752 if (extendedPriorities)
753 dontCarePriority++;
754}
755
756template<typename ValueType>
757void DftToGspnTransformator<ValueType>::translateSPARE(std::shared_ptr<storm::dft::storage::elements::DFTSpare<ValueType> const> dftSpare) {
758 double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x;
759 double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y;
760
761 u_int64_t prio = getFailPriority(dftSpare);
762
763 uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
764
765 bool isRepresentative = mDft.isRepresentative(dftSpare->id());
766 uint64_t unavailablePlace = 0;
767 if (!smart || isRepresentative) {
768 unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
769 }
770
771 uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
772 builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 20.0, ycenter - 12.0));
773 activePlaces.emplace(dftSpare->id(), activePlace);
774
775 std::vector<uint64_t> tNextClaims;
776 std::vector<uint64_t> tNextConsiders;
777 for (size_t i = 0; i < dftSpare->nrChildren(); ++i) {
778 auto const &child = dftSpare->children().at(i);
779 // Consider next child
780 size_t considerPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSpare->name() + "_consider_" + child->name());
781 builder.setPlaceLayoutInfo(considerPlace, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter - 8.0));
782
783 if (i > 0) {
784 // Set output transition from previous next_claim
785 builder.addOutputArc(tNextClaims.back(), considerPlace);
786 // Set output transition from previous cannot_claim
787 builder.addOutputArc(tNextConsiders.back(), considerPlace);
788 }
789
790 // Cannot claim child
791 uint64_t tConsiderNext = builder.addImmediateTransition(prio, 0.0, dftSpare->name() + "_cannot_claim_" + child->name());
792 prio++;
793 builder.setTransitionLayoutInfo(tConsiderNext, storm::gspn::LayoutInfo(xcenter - 7.0 + i * 14.0, ycenter - 8.0));
794 builder.addInputArc(considerPlace, tConsiderNext);
795 builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext);
796 builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id()));
797 tNextConsiders.push_back(tConsiderNext);
798
799 // Claimed child
800 size_t claimedPlace = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name());
801 builder.setPlaceLayoutInfo(claimedPlace, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter + 5.0));
802 uint64_t tClaim = builder.addImmediateTransition(prio, 0.0, dftSpare->name() + "_claim_" + child->name());
803 prio++;
804 builder.setTransitionLayoutInfo(tClaim, storm::gspn::LayoutInfo(xcenter - 15.0 + i * 14.0, ycenter));
805 builder.addInhibitionArc(unavailablePlaces.at(child->id()), tClaim);
806 builder.addInputArc(considerPlace, tClaim);
807 builder.addOutputArc(tClaim, claimedPlace);
808 builder.addOutputArc(tClaim, unavailablePlaces.at(child->id()));
809
810 // Claim next
811 uint64_t tClaimNext = builder.addImmediateTransition(prio, 0.0, dftSpare->name() + "_next_claim_" + std::to_string(i));
812 prio++;
813 builder.setTransitionLayoutInfo(tClaimNext, storm::gspn::LayoutInfo(xcenter - 7.0 + i * 14.0, ycenter + 5.0));
814 builder.addInputArc(claimedPlace, tClaimNext);
815 builder.addInputArc(getFailedPlace(child), tClaimNext);
816 builder.addOutputArc(tClaimNext, getFailedPlace(child));
817 tNextClaims.push_back(tClaimNext);
818
819 // Activate all elements in spare module
820 uint64_t l = 0;
821 for (uint64_t k : mDft.module(child->id()).getElements()) {
822 uint64_t tActivate = builder.addImmediateTransition(prio, 0.0, dftSpare->name() + "_activate_" + std::to_string(i) + "_" + std::to_string(k));
823 prio++;
824 builder.setTransitionLayoutInfo(tActivate, storm::gspn::LayoutInfo(xcenter - 18.0 + (i + l) * 3, ycenter - 12.0));
825 builder.addInhibitionArc(activePlaces.at(k), tActivate);
826 builder.addInputArc(claimedPlace, tActivate);
827 builder.addInputArc(activePlace, tActivate);
828 builder.addOutputArc(tActivate, claimedPlace);
829 builder.addOutputArc(tActivate, activePlace);
830 builder.addOutputArc(tActivate, activePlaces.at(k));
831 ++l;
832 }
833 }
834
835 // Set arcs to failed
836 builder.addOutputArc(tNextConsiders.back(), failedPlace);
837 builder.addOutputArc(tNextClaims.back(), failedPlace);
838 builder.addInhibitionArc(failedPlace, tNextConsiders.back());
839 builder.addInhibitionArc(failedPlace, tNextClaims.back());
840
841 // Don't Care Mechanism
842 if (dontCareElements.count(dftSpare->id())) {
843 if (dftSpare->id() != mDft.getTopLevelIndex()) {
844 u_int64_t tDontCare = addDontcareTransition(dftSpare, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
845 if (!mergedDCFailed) {
846 uint64_t dontCarePlace = builder.addPlace(1, 0, dftSpare->name() + STR_DONTCARE);
847 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
848 builder.addInhibitionArc(dontCarePlace, tDontCare);
849 builder.addOutputArc(tDontCare, dontCarePlace);
850 // Propagation
851 uint64_t propagationPlace = builder.addPlace(1, 0, dftSpare->name() + "_prop");
852 builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
853 uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, dftSpare->name() + "_prop_fail");
854 builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
855 builder.addInhibitionArc(propagationPlace, tPropagationFailed);
856 builder.addInputArc(failedPlace, tPropagationFailed);
857 builder.addOutputArc(tPropagationFailed, failedPlace);
858 builder.addOutputArc(tPropagationFailed, propagationPlace);
859 uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, dftSpare->name() + "_prop_dontCare");
860 builder.setTransitionLayoutInfo(tPropagationDontCare, storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
861 builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
862 builder.addInputArc(dontCarePlace, tPropagationDontCare);
863 builder.addOutputArc(tPropagationDontCare, dontCarePlace);
864 builder.addOutputArc(tPropagationDontCare, propagationPlace);
865 for (auto const &child : dftSpare->children()) {
866 if (dontCareElements.count(child->id())) {
867 u_int64_t childDontCare = dontcareTransitions.at(child->id());
868 builder.addInputArc(propagationPlace, childDontCare);
869 builder.addOutputArc(childDontCare, propagationPlace);
870 }
871 }
872 } else {
873 builder.addInhibitionArc(failedPlace, tDontCare);
874 builder.addOutputArc(tDontCare, failedPlace);
875 for (auto const &child : dftSpare->children()) {
876 if (dontCareElements.count(child->id())) {
877 u_int64_t childDontCare = dontcareTransitions.at(child->id());
878 builder.addInputArc(failedPlace, childDontCare);
879 builder.addOutputArc(childDontCare, failedPlace);
880 }
881 }
882 }
883 } else {
884 // If SPARE is TLE, simple failure propagation suffices
885 for (auto const &child : dftSpare->children()) {
886 if (dontCareElements.count(child->id())) {
887 u_int64_t childDontCare = dontcareTransitions.at(child->id());
888 builder.addInputArc(failedPlace, childDontCare);
889 builder.addOutputArc(childDontCare, failedPlace);
890 }
891 }
892 }
893 }
894
895 if (!smart || isRepresentative) {
896 builder.addOutputArc(tNextConsiders.back(), unavailablePlace);
897 builder.addOutputArc(tNextClaims.back(), unavailablePlace);
898 }
899 if (extendedPriorities)
900 dontCarePriority++;
901}
902
903template<typename ValueType>
904void DftToGspnTransformator<ValueType>::translatePDEP(std::shared_ptr<storm::dft::storage::elements::DFTDependency<ValueType> const> dftDependency) {
905 double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x;
906 double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;
907
908 uint64_t failedPlace = 0;
909 if (!smart) {
910 failedPlace = addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
911 addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
912 }
913
914 uint64_t forwardPlace = 0;
915 if (dftDependency->probability() < 1.0) {
916 // PDEP
917 forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward");
918 builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter + 1.0, ycenter + 2.0));
919
920 uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin");
921 builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 2.0));
922
923 uint64_t tStartFlip = builder.addImmediateTransition(getFailPriority(dftDependency), 0.0, dftDependency->name() + "_start_flip");
924 builder.addInputArc(coinPlace, tStartFlip);
925 builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip);
926 builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent()));
927
928 uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip");
929 builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter - 2.0, ycenter + 2.0));
930 builder.addOutputArc(tStartFlip, flipPlace);
931
932 uint64_t tWinFlip =
933 builder.addImmediateTransition(getFailPriority(dftDependency) + 1, dftDependency->probability(), dftDependency->name() + "_win_flip");
934 builder.addInputArc(flipPlace, tWinFlip);
935 builder.addOutputArc(tWinFlip, forwardPlace);
936
937 uint64_t tLooseFlip = builder.addImmediateTransition(
938 getFailPriority(dftDependency) + 1, storm::utility::one<ValueType>() - dftDependency->probability(), dftDependency->name() + "_lose_flip");
939 builder.addInputArc(flipPlace, tLooseFlip);
940 } else {
941 // FDEP
942 forwardPlace = getFailedPlace(dftDependency->triggerEvent());
943 }
944
945 // if the extended priorities option is set, set the priority for the forwarding transitions uniquely
946 uint64_t propagationPriority = getFailPriority(dftDependency);
947 for (auto const &child : dftDependency->dependentEvents()) {
948 uint64_t tForwardFailure = builder.addImmediateTransition(propagationPriority, 0.0, dftDependency->name() + "_propagate_" + child->name());
949
950 builder.addInputArc(forwardPlace, tForwardFailure);
951 builder.addOutputArc(tForwardFailure, forwardPlace);
952 builder.addOutputArc(tForwardFailure, getFailedPlace(child));
953 builder.addInhibitionArc(getFailedPlace(child), tForwardFailure);
954 if (!smart || child->nrRestrictions() > 0) {
955 builder.addInhibitionArc(disabledPlaces.at(child->id()), tForwardFailure);
956 }
957 if (!smart || mDft.isRepresentative(child->id())) {
958 builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id()));
959 }
960 propagationPriority--;
961 }
962
963 // Don't Care
964 if (dontCareElements.count(dftDependency->id())) {
965 u_int64_t tDontCare = addDontcareTransition(dftDependency, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
966 if (!mergedDCFailed) {
967 u_int64_t dontCarePlace = builder.addPlace(1, 0, dftDependency->name() + STR_DONTCARE);
968 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 4.0, ycenter));
969 builder.addInhibitionArc(dontCarePlace, tDontCare);
970 builder.addOutputArc(tDontCare, dontCarePlace);
971 // Add the arcs for the dependent events
972 for (auto const &dependentEvent : dftDependency->dependentEvents()) {
973 if (dontCareElements.count(dependentEvent->id())) {
974 u_int64_t dependentEventPropagation = dependencyPropagationPlaces.at(dependentEvent->id());
975 builder.addInputArc(dependentEventPropagation, tDontCare);
976 builder.addOutputArc(tDontCare, dependentEventPropagation);
977 }
978 }
979 // Add the arcs for the trigger
980 uint64_t triggerDontCare = dontcareTransitions.at(dftDependency->triggerEvent()->id());
981 builder.addInputArc(dontCarePlace, triggerDontCare);
982 builder.addOutputArc(triggerDontCare, dontCarePlace);
983 } else {
984 if (failedPlace == 0) {
985 failedPlace = addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 4.0, ycenter));
986 }
987 builder.addInhibitionArc(failedPlace, tDontCare);
988 builder.addOutputArc(tDontCare, failedPlace);
989
990 // Add the arcs for the dependent events
991 for (auto const &dependentEvent : dftDependency->dependentEvents()) {
992 if (dontCareElements.count(dependentEvent->id())) {
993 u_int64_t dependentEventFailed = failedPlaces.at(dependentEvent->id());
994 builder.addInputArc(dependentEventFailed, tDontCare);
995 builder.addOutputArc(tDontCare, dependentEventFailed);
996 }
997 }
998 // Add the arcs for the trigger
999 uint64_t triggerDontCare = dontcareTransitions.at(dftDependency->triggerEvent()->id());
1000 builder.addInputArc(failedPlace, triggerDontCare);
1001 builder.addOutputArc(triggerDontCare, failedPlace);
1002 }
1003 }
1004 if (failedPlace == 0) {
1005 failedPlaces.push_back(failedPlace);
1006 }
1007 if (extendedPriorities)
1008 dontCarePriority++;
1009}
1010
1011template<typename ValueType>
1012void DftToGspnTransformator<ValueType>::translateSeq(std::shared_ptr<storm::dft::storage::elements::DFTSeq<ValueType> const> dftSeq) {
1013 STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException,
1014 "Sequence enforcers with gates as children are currently not supported");
1015 double xcenter = mDft.getElementLayoutInfo(dftSeq->id()).x;
1016 double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y;
1017 u_int64_t failedPlace = 0;
1018 if (!smart) {
1019 failedPlace = addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
1020 addUnavailablePlace(dftSeq, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
1021 }
1022
1023 uint64_t tEnable = 0;
1024 uint64_t nextPlace = 0;
1025 for (size_t i = 0; i < dftSeq->nrChildren(); ++i) {
1026 auto const &child = dftSeq->children().at(i);
1027
1028 nextPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSeq->name() + "_next_" + child->name());
1029 builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter - 3.0));
1030
1031 if (i > 0) {
1032 builder.addOutputArc(tEnable, nextPlace);
1033 }
1034 tEnable = builder.addImmediateTransition(getFailPriority(dftSeq), 0.0, dftSeq->name() + "_unblock_" + child->name());
1035 builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
1036 builder.addInputArc(nextPlace, tEnable);
1037 builder.addInputArc(disabledPlaces.at(child->id()), tEnable);
1038 if (i > 0) {
1039 builder.addInputArc(getFailedPlace(dftSeq->children().at(i - 1)), tEnable);
1040 }
1041 }
1042 // Dont Care
1043 if (dontCareElements.count(dftSeq->id())) {
1044 if (!mergedDCFailed) {
1045 u_int64_t dontCarePlace = builder.addPlace(1, 0, dftSeq->name() + STR_DONTCARE);
1046 builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
1047 for (auto const &child : dftSeq->children()) {
1048 if (dontCareElements.count(child->id())) {
1049 u_int64_t childDontCare = dontcareTransitions.at(child->id());
1050 builder.addInputArc(dontCarePlace, childDontCare);
1051 }
1052 }
1053 } else {
1054 if (failedPlace == 0) {
1055 failedPlace = addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
1056 }
1057 for (auto const &child : dftSeq->children()) {
1058 if (dontCareElements.count(child->id())) {
1059 u_int64_t childDontCare = dontcareTransitions.at(child->id());
1060 builder.addInputArc(failedPlace, childDontCare);
1061 }
1062 }
1063 }
1064 }
1065}
1066
1067template<typename ValueType>
1068uint64_t DftToGspnTransformator<ValueType>::addFailedPlace(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement,
1069 storm::gspn::LayoutInfo const &layoutInfo, bool initialFailed) {
1070 uint64_t failedPlace = builder.addPlace(defaultCapacity, initialFailed ? 1 : 0, dftElement->name() + STR_FAILED);
1071 assert(failedPlaces.size() == dftElement->id());
1072 failedPlaces.push_back(failedPlace);
1073 builder.setPlaceLayoutInfo(failedPlace, layoutInfo);
1074 return failedPlace;
1075}
1076
1077template<typename ValueType>
1078uint64_t DftToGspnTransformator<ValueType>::addUnavailablePlace(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement,
1079 storm::gspn::LayoutInfo const &layoutInfo, bool initialAvailable) {
1080 unsigned int capacity = 2; // Unavailable place has capacity 2
1081 uint64_t unavailablePlace = builder.addPlace(capacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail");
1082 unavailablePlaces.emplace(dftElement->id(), unavailablePlace);
1083 builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo);
1084 return unavailablePlace;
1085}
1086
1087template<typename ValueType>
1088uint64_t DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::dft::storage::elements::DFTBE<ValueType>> dftBe,
1089 storm::gspn::LayoutInfo const &layoutInfo) {
1090 uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
1091 disabledPlaces.emplace(dftBe->id(), disabledPlace);
1092 builder.setPlaceLayoutInfo(disabledPlace, layoutInfo);
1093 return disabledPlace;
1094}
1095
1096template<typename ValueType>
1097uint64_t DftToGspnTransformator<ValueType>::addDontcareTransition(std::shared_ptr<const storm::dft::storage::elements::DFTElement<ValueType>> dftElement,
1098 storm::gspn::LayoutInfo const &layoutInfo) {
1099 uint64_t dontcareTransition;
1100 dontcareTransition = builder.addImmediateTransition(dontCarePriority, 0.0, dftElement->name() + STR_DONTCARE + "_transition");
1101 dontcareTransitions.emplace(dftElement->id(), dontcareTransition);
1102 builder.setTransitionLayoutInfo(dontcareTransition, layoutInfo);
1103 return dontcareTransition;
1104}
1105
1106template<typename ValueType>
1107bool DftToGspnTransformator<ValueType>::isActiveInitially(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement) {
1108 // If element is in the top module, return true.
1109 return !mDft.hasRepresentant(dftElement->id());
1110}
1111
1112template<typename ValueType>
1113uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType> const> dftElement) {
1114 // Return the value given in the field
1115 return priorities.at(dftElement->id());
1116}
1117
1118// Explicitly instantiate the class.
1119template class DftToGspnTransformator<double>;
1120
1121// template class DftToGspnTransformator<storm::RationalFunction>;
1122
1123} // namespace transformations
1124} // namespace storm::dft
storm::dft::storage::DFT
Represents a Dynamic Fault Tree.
Definition DFT.h:52
storm::dft::storage::elements::BEConst
BE which is either constant failed or constant failsafe.
Definition BEConst.h:14
storm::dft::storage::elements::BEExponential
BE with exponential failure distribution.
Definition BEExponential.h:13
storm::dft::storage::elements::DFTBE
Abstract base class for basic events (BEs) in DFTs.
Definition DFTBE.h:14
storm::dft::storage::elements::DFTDependency
Dependency gate with probability p.
Definition DFTDependency.h:20
storm::dft::storage::elements::DFTElement
Abstract base class for DFT elements.
Definition DFTElement.h:39
storm::dft::storage::elements::DFTPand
Priority AND (PAND) gate.
Definition DFTPand.h:17
storm::dft::storage::elements::DFTPor
Priority OR (POR) gate.
Definition DFTPor.h:17
storm::dft::storage::elements::DFTSeq
Sequence enforcer (SEQ).
Definition DFTSeq.h:15
storm::dft::storage::elements::DFTVot
VOT gate with threshold k.
Definition DFTVot.h:14
storm::dft::transformations::DftToGspnTransformator::transform
void transform(std::map< uint64_t, uint64_t > const &priorities, std::set< uint64_t > const &dontCareElements, bool smart=true, bool mergeDCFailed=true, bool extendPriorities=false)
Transform the DFT to a GSPN.
Definition DftToGspnTransformator.cpp:17
storm::dft::transformations::DftToGspnTransformator::toplevelFailedPlaceId
uint64_t toplevelFailedPlaceId()
Get failed place id of top level element.
Definition DftToGspnTransformator.cpp:101
storm::dft::transformations::DftToGspnTransformator::DftToGspnTransformator
DftToGspnTransformator(storm::dft::storage::DFT< ValueType > const &dft)
Constructor.
Definition DftToGspnTransformator.cpp:12
storm::dft::transformations::DftToGspnTransformator::computePriorities
std::map< uint64_t, uint64_t > computePriorities(bool extendedPrio)
Compute priorities used for GSPN transformation.
Definition DftToGspnTransformator.cpp:35
STORM_LOG_ASSERT
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
STORM_LOG_THROW
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
storm::dft::transformations::defaultCapacity
static constexpr const uint64_t defaultCapacity
Definition DftToGspnTransformator.cpp:9