Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
DFTStateSpaceGenerationQueues.h
Go to the documentation of this file.
1#pragma once
2
3#include <deque>
4#include <list>
5#include <queue>
6#include <vector>
7
9
10namespace storm::dft {
11namespace storage {
12
13// Forward declarations
14namespace elements {
15
16template<typename ValueType>
17class DFTGate;
18template<typename ValueType>
19class DFTElement;
20template<typename ValueType>
21class DFTRestriction;
22
23} // namespace elements
24
25template<typename ValueType>
27 using DFTElementPointer = std::shared_ptr<storm::dft::storage::elements::DFTElement<ValueType>>;
28 using DFTElementVector = std::vector<DFTElementPointer>;
29 using DFTGatePointer = std::shared_ptr<storm::dft::storage::elements::DFTGate<ValueType>>;
30 using DFTGateVector = std::vector<DFTGatePointer>;
31 using DFTRestrictionPointer = std::shared_ptr<storm::dft::storage::elements::DFTRestriction<ValueType>>;
32 using DFTRestrictionVector = std::vector<DFTRestrictionPointer>;
33
34 std::priority_queue<DFTGatePointer, DFTGateVector, OrderElementsByRank<ValueType>> failurePropagation;
35 DFTGateVector failsafePropagation;
36 DFTElementVector dontcarePropagation;
37 DFTElementVector activatePropagation;
38 DFTRestrictionVector restrictionChecks;
39
40 public:
41 void propagateFailure(DFTGatePointer const& elem) {
42 failurePropagation.push(elem);
43 }
44
46 return failurePropagation.empty();
47 }
48
49 DFTGatePointer nextFailurePropagation() {
50 DFTGatePointer next = failurePropagation.top();
51 failurePropagation.pop();
52 return next;
53 }
54
55 bool restrictionChecksDone() const {
56 return restrictionChecks.empty();
57 }
58
59 DFTRestrictionPointer nextRestrictionCheck() {
60 STORM_LOG_ASSERT(!restrictionChecksDone(), "All restriction checks done already.");
61 DFTRestrictionPointer next = restrictionChecks.back();
62 restrictionChecks.pop_back();
63 return next;
64 }
65
66 void checkRestrictionLater(DFTRestrictionPointer const& restr) {
67 restrictionChecks.push_back(restr);
68 }
69
71 return failsafePropagation.empty();
72 }
73
74 void propagateFailsafe(DFTGatePointer const& gate) {
75 failsafePropagation.push_back(gate);
76 }
77
78 DFTGatePointer nextFailsafePropagation() {
79 DFTGatePointer next = failsafePropagation.back();
80 failsafePropagation.pop_back();
81 return next;
82 }
83
85 return dontcarePropagation.empty();
86 }
87
88 void propagateDontCare(DFTElementPointer const& elem) {
89 dontcarePropagation.push_back(elem);
90 }
91
92 void propagateDontCare(DFTElementVector const& elems) {
93 dontcarePropagation.insert(dontcarePropagation.end(), elems.begin(), elems.end());
94 }
95
96 DFTElementPointer nextDontCarePropagation() {
97 DFTElementPointer next = dontcarePropagation.back();
98 dontcarePropagation.pop_back();
99 return next;
100 }
101};
102
103} // namespace storage
104} // namespace storm::dft
void checkRestrictionLater(DFTRestrictionPointer const &restr)
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11