Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
DFTSpare.h
Go to the documentation of this file.
1#pragma once
2
3#include "DFTGate.h"
4
5namespace storm::dft {
6namespace storage {
7namespace elements {
8
12template<typename ValueType>
13class DFTSpare : public DFTGate<ValueType> {
14 public:
21 DFTSpare(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {})
22 : DFTGate<ValueType>(id, name, children) {
23 // Intentionally left empty.
24 }
25
26 std::shared_ptr<DFTElement<ValueType>> clone() const override {
27 return std::shared_ptr<DFTElement<ValueType>>(new DFTSpare<ValueType>(this->id(), this->name(), {}));
28 }
29
33
34 bool isSpareGate() const override {
35 return true;
36 }
37
42
47
50 // Check children as claiming shared children might make a difference
51 for (std::shared_ptr<DFTElement<ValueType>> const& child : this->children()) {
52 if (state.isOperational(child->id())) {
53 // Check if operational child is shared by another SPARE
54 for (std::shared_ptr<DFTGate<ValueType>> const& parent : child->parents()) {
55 if (parent->id() != this->id() && parent->isSpareGate()) {
56 // Child could be claimed by another SPARE -> do not set to DC yet
57 return false;
58 }
59 }
60 }
61 }
62 // Perform regular check
64 state.finalizeUses(this->mId);
65 return true;
66 }
67 return false;
68 }
69
71 if (state.isOperational(this->mId)) {
72 size_t uses = state.uses(this->mId);
73 if (!state.isOperational(uses)) {
74 bool claimingSuccessful = state.claimNew(this->mId, uses, this->children());
75 if (!claimingSuccessful) {
76 this->fail(state, queues);
77 }
78 }
79 }
80 }
81
83 if (state.isOperational(this->mId)) {
84 if (state.isFailsafe(state.uses(this->mId))) {
85 this->failsafe(state, queues);
86 this->childrenDontCare(queues);
87 }
88 }
89 }
90
91 std::vector<size_t> independentSubDft(bool blockParents, bool sparesAsLeaves = false) const override {
92 auto prelRes = DFTElement<ValueType>::independentSubDft(blockParents);
93 if (prelRes.empty()) {
94 // No elements (especially not this->id) in the prelimanry result, so we know already that it is not a subdft.
95 return prelRes;
96 }
97 std::set<size_t> unit(prelRes.begin(), prelRes.end());
98 std::vector<size_t> pids = this->parentIds();
99 if (!sparesAsLeaves) {
100 for (auto const& child : this->children()) {
101 child->extendSubDft(unit, pids, blockParents, sparesAsLeaves);
102 if (unit.empty()) {
103 // Parent in the subdft, ie it is *not* a subdft
104 break;
105 }
106 }
107 }
108 return std::vector<size_t>(unit.begin(), unit.end());
109 }
110
111 void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
112 if (elemsInSubtree.count(this->id()) > 0)
113 return;
114 DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
115 if (elemsInSubtree.empty()) {
116 // Parent in the subdft, ie it is *not* a subdft
117 return;
118 }
119 if (!sparesAsLeaves) {
120 for (auto const& child : this->children()) {
121 child->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
122 if (elemsInSubtree.empty()) {
123 // Parent in the subdft, ie it is *not* a subdft
124 return;
125 }
126 }
127 }
128 }
129};
130
131} // namespace elements
132} // namespace storage
133} // namespace storm::dft
bool claimNew(size_t spareId, size_t currentlyUses, std::vector< std::shared_ptr< storm::dft::storage::elements::DFTElement< ValueType > > > const &children)
Claim a new spare child for the given spare gate.
Definition DFTState.cpp:530
uint_fast64_t uses(size_t id) const
This method returns the id of the used child for a spare.
Definition DFTState.cpp:431
void finalizeUses(size_t spareId)
Sets the use for the spare to a default value to gain consistent states after failures.
Definition DFTState.cpp:463
bool isOperational(size_t id) const
Definition DFTState.cpp:150
bool isFailsafe(size_t id) const
Definition DFTState.cpp:165
DFTElementVector const & children() const
Get children.
Definition DFTChildren.h:45
Abstract base class for DFT elements.
Definition DFTElement.h:39
virtual size_t id() const
Get id.
Definition DFTElement.h:73
virtual std::string const & name() const
Get name.
Definition DFTElement.h:89
std::vector< size_t > parentIds() const
Return Ids of parents.
Definition DFTElement.h:241
virtual void extendSubDft(std::set< size_t > &elemsInSubtree, std::vector< size_t > const &parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const
Helper to the independent subtree computation.
virtual std::vector< size_t > independentSubDft(bool blockParents, bool sparesAsLeaves=false) const
Computes independent subtrees starting with this element (this), that is, all elements (x) which are ...
Abstract base class for gates.
Definition DFTGate.h:13
void failsafe(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Definition DFTGate.h:72
void childrenDontCare(storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const
Propagate Don't Care to children.
Definition DFTGate.h:86
void fail(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Definition DFTGate.h:59
void fail(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Definition DFTSpare.h:38
void failsafe(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Definition DFTSpare.h:43
std::shared_ptr< DFTElement< ValueType > > clone() const override
Create a shallow copy of the element.
Definition DFTSpare.h:26
void checkFails(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Check failed status.
Definition DFTSpare.h:70
void checkFailsafe(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Check failsafe status.
Definition DFTSpare.h:82
DFTSpare(size_t id, std::string const &name, std::vector< std::shared_ptr< DFTElement< ValueType > > > const &children={})
Constructor.
Definition DFTSpare.h:21
storm::dft::storage::elements::DFTElementType type() const override
Get type.
Definition DFTSpare.h:30
bool checkDontCareAnymore(storm::dft::storage::DFTState< ValueType > &state, storm::dft::storage::DFTStateSpaceGenerationQueues< ValueType > &queues) const override
Definition DFTSpare.h:48
std::vector< size_t > independentSubDft(bool blockParents, bool sparesAsLeaves=false) const override
Computes independent subtrees starting with this element (this), that is, all elements (x) which are ...
Definition DFTSpare.h:91
void extendSubDft(std::set< size_t > &elemsInSubtree, std::vector< size_t > const &parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override
Helper to the independent subtree computation.
Definition DFTSpare.h:111
bool isSpareGate() const override
Check whether the element is a SPARE gate.
Definition DFTSpare.h:34
DFTElementType
Element types in a DFT.