From 09797dae5a5c883de0903c46afc844b83b81131d Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 30 May 2018 17:17:31 +0200
Subject: [PATCH] SMT encoding for SEQ gate

---
 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 56e7671b5..de653752d 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -544,8 +544,18 @@ namespace storm {
                         break;
                     }
                     case storm::storage::DFTElementType::SEQ:
-                        STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of SEQs is not implemented yet.");
+                    {
+                        // Constraint for SEQ gate (constraint 4)
+                        // As the restriction is not a gate we have to enumerate its children here
+                        auto seq = std::static_pointer_cast<storm::storage::DFTRestriction<double> const>(element);
+                        for (auto const& child : seq->children()) {
+                            childVarIndices.push_back(timePointVariables.at(child->id()));
+                        }
+
+                        constraints.push_back(std::make_shared<Sorted>(childVarIndices));
+                        constraints.back()->setDescription("SEQ gate " + element->name());
                         break;
+                    }
                     case storm::storage::DFTElementType::SPARE:
                     {
                         auto spare = std::static_pointer_cast<storm::storage::DFTSpare<double> const>(element);