diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 65ad82437..0a0aa5b32 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/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") { diff --git a/src/storage/dft/elements/DFTPor.h b/src/storage/dft/elements/DFTPor.h index 1aaa943b0..c37331354 100644 --- a/src/storage/dft/elements/DFTPor.h +++ b/src/storage/dft/elements/DFTPor.h @@ -11,11 +11,27 @@ namespace storm { {} void checkFails(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& 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& state, DFTStateSpaceGenerationQueues& 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 {