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