From fe7037e7fd7d151509ae186c0371bf242b21d22f Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 17 Mar 2016 10:47:50 +0100
Subject: [PATCH] Support for POR (priority or)
Former-commit-id: f0e782bcb1024ff36a6afcb3989fb132b8e56a6c
---
src/parser/DFTGalileoParser.cpp | 2 ++
src/storage/dft/elements/DFTPor.h | 20 ++++++++++++++++++--
2 files changed, 20 insertions(+), 2 deletions(-)
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<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 {