From 15fdac6059315eb42a4208bc01c8ad5e1d7e522a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 10 Mar 2018 20:30:14 +0100
Subject: [PATCH] acc: strengthen is_generalized_rabin() and
 is_generalized_streett()

* spot/twa/acc.cc: These functions were segfaulting on acceptance
conditions such as "Acceptance: 3 t" or "Acceptance: 3 f".
The issue was revealed on branch "next" by the change that print_dot()
display the acceptance condition by default, but we want the fix on
master as well.
* NEWS: Mention the issue.
---
 NEWS            |  6 ++++++
 spot/twa/acc.cc | 10 ++++++++--
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index cb068bce8..74e1765b7 100644
--- a/NEWS
+++ b/NEWS
@@ -11,6 +11,12 @@ New in spot 2.5.1.dev (not yet released)
     update an external structure that references states of the twa
     that we want to purge.
 
+  Bugs fixed:
+
+  - acc_cond::is_generalized_rabin() and
+    acc_cond::is_generalized_streett() would segfault on weird
+    acceptance conditions such as "3 t" or "3 f".
+
 New in spot 2.5.1 (2018-02-20)
 
   Library:
diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index c6df13210..1b94f802e 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -660,7 +660,10 @@ namespace spot
         pairs.resize(num_);
         return true;
       }
-    if (code_.is_t()
+    // "Acceptance: 0 f" is caught by is_generalized_rabin() above.
+    // Therefore is_f() below catches "Acceptance: n f" with n>0.
+    if (code_.is_f()
+        || code_.is_t()
         || code_.back().sub.op != acc_op::Or)
       return false;
 
@@ -741,7 +744,10 @@ namespace spot
         pairs.resize(num_);
         return true;
       }
-    if (code_.is_f()
+    // "Acceptance: 0 t" is caught by is_generalized_buchi() above.
+    // Therefore is_t() below catches "Acceptance: n t" with n>0.
+    if (code_.is_t()
+        || code_.is_f()
         || code_.back().sub.op != acc_op::And)
       return false;