Browse Source

Support for POR (priority or)

Former-commit-id: f0e782bcb1
tempestpy_adaptions
Mavo 9 years ago
parent
commit
fe7037e7fd
  1. 2
      src/parser/DFTGalileoParser.cpp
  2. 20
      src/storage/dft/elements/DFTPor.h

2
src/parser/DFTGalileoParser.cpp

@ -100,6 +100,8 @@ namespace storm {
success = builder.addVotElement(name, threshold, childNames);
} else if (tokens[1] == "pand") {
success = builder.addPandElement(name, childNames);
} else if (tokens[1] == "por") {
success = builder.addPorElement(name, childNames);
} else if (tokens[1] == "wsp" || tokens[1] == "csp") {
success = builder.addSpareElement(name, childNames);
} else if (tokens[1] == "seq") {

20
src/storage/dft/elements/DFTPor.h

@ -11,11 +11,27 @@ namespace storm {
{}
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
assert(false);
if(state.isOperational(this->mId)) {
if (state.hasFailed(this->mChildren.front()->id())) {
// First child has failed before others
this->fail(state, queues);
} else {
for (size_t i = 1; i < this->nrChildren(); ++i) {
if (state.hasFailed(this->mChildren[i]->id())) {
// Child has failed before first child
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
}
}
}
}
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
assert(false);
if (state.isFailsafe(this->mChildren.front()->id())) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
}
}
virtual DFTElementType type() const override {

Loading…
Cancel
Save