From 002e6ed96b6315e026db8f578ab7978fccae554b Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 26 Sep 2017 17:30:54 +0200
Subject: [PATCH] formula: fix building of {a->c[*]}
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #285, reported by Florian Perlié-Long.

* NEWS: Mention the issue.
* spot/tl/formula.cc: Fix it.
* tests/core/kind.test: Document it.
* THANKS: Add Florian.
---
 NEWS                 | 3 +++
 THANKS               | 1 +
 spot/tl/formula.cc   | 3 ++-
 tests/core/kind.test | 5 +++--
 4 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/NEWS b/NEWS
index 492cc8706..722fa7bba 100644
--- a/NEWS
+++ b/NEWS
@@ -81,6 +81,9 @@ New in spot 2.4.0.dev (not yet released)
 
   Bugs fixed:
 
+  - The formula class failed to build {a->c[*]} althought it is
+    alowed in our grammar.
+
   - spot::scc_info::determine_unknown_acceptance() incorrectly
     considered some rejecting SCC as accepting.
 
diff --git a/THANKS b/THANKS
index 7a4d7d938..7a235bdc6 100644
--- a/THANKS
+++ b/THANKS
@@ -11,6 +11,7 @@ Ernesto Posse
 Étienne Renault
 Fabrice Kordon
 Felix Klaedtke
+Florian Perlié-Long
 František Blahoudek
 Gerard J. Holzmann
 Heikki Tauriainen
diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc
index 0b0dced0f..2a5238a95 100644
--- a/spot/tl/formula.cc
+++ b/spot/tl/formula.cc
@@ -1281,7 +1281,8 @@ namespace spot
         props = children[0]->props & children[1]->props;
         is_.eventual = false;
         is_.universal = false;
-        is_.sere_formula = is_.boolean;
+        is_.sere_formula = (children[0]->is_boolean()
+                            && children[1]->is_sere_formula());
         is_.sugar_free_boolean = false;
         is_.in_nenoform = false;
         is_.syntactic_safety = (children[0]->is_syntactic_guarantee()
diff --git a/tests/core/kind.test b/tests/core/kind.test
index b0733bc2d..416eb0c1d 100755
--- a/tests/core/kind.test
+++ b/tests/core/kind.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2010, 2011, 2012, 2015, 2017 Laboratoire de Recherche
+# et Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -133,6 +133,7 @@ Fa  M b,&!xLPgopra
 {p[+]:p[+]},&!xfPsoprla
 (!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
 {b[+][:*0..3]},&!fPsopra
+{a->c[*]},fPsopra
 EOF
 
 run 0 ../kind input