formula: fix building of {a->c[*]}
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.
This commit is contained in:
parent
32087f29ad
commit
bef58b4169
4 changed files with 9 additions and 3 deletions
3
NEWS
3
NEWS
|
|
@ -2,6 +2,9 @@ New in spot 2.4.0.dev (not yet released)
|
||||||
|
|
||||||
Bugs fixed:
|
Bugs fixed:
|
||||||
|
|
||||||
|
- The formula class failed to build {a->c[*]} althought it is
|
||||||
|
alowed in our grammar.
|
||||||
|
|
||||||
- spot::scc_info::determine_unknown_acceptance() incorrectly
|
- spot::scc_info::determine_unknown_acceptance() incorrectly
|
||||||
considered some rejecting SCC as accepting.
|
considered some rejecting SCC as accepting.
|
||||||
|
|
||||||
|
|
|
||||||
1
THANKS
1
THANKS
|
|
@ -11,6 +11,7 @@ Ernesto Posse
|
||||||
Étienne Renault
|
Étienne Renault
|
||||||
Fabrice Kordon
|
Fabrice Kordon
|
||||||
Felix Klaedtke
|
Felix Klaedtke
|
||||||
|
Florian Perlié-Long
|
||||||
František Blahoudek
|
František Blahoudek
|
||||||
Gerard J. Holzmann
|
Gerard J. Holzmann
|
||||||
Heikki Tauriainen
|
Heikki Tauriainen
|
||||||
|
|
|
||||||
|
|
@ -1281,7 +1281,8 @@ namespace spot
|
||||||
props = children[0]->props & children[1]->props;
|
props = children[0]->props & children[1]->props;
|
||||||
is_.eventual = false;
|
is_.eventual = false;
|
||||||
is_.universal = 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_.sugar_free_boolean = false;
|
||||||
is_.in_nenoform = false;
|
is_.in_nenoform = false;
|
||||||
is_.syntactic_safety = (children[0]->is_syntactic_guarantee()
|
is_.syntactic_safety = (children[0]->is_syntactic_guarantee()
|
||||||
|
|
|
||||||
|
|
@ -1,7 +1,7 @@
|
||||||
#! /bin/sh
|
#! /bin/sh
|
||||||
# -*- coding: utf-8 -*-
|
# -*- coding: utf-8 -*-
|
||||||
# Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
|
# Copyright (C) 2010, 2011, 2012, 2015, 2017 Laboratoire de Recherche
|
||||||
# Développement de l'Epita (LRDE).
|
# et Développement de l'Epita (LRDE).
|
||||||
#
|
#
|
||||||
# This file is part of Spot, a model checking library.
|
# This file is part of Spot, a model checking library.
|
||||||
#
|
#
|
||||||
|
|
@ -133,6 +133,7 @@ Fa M b,&!xLPgopra
|
||||||
{p[+]:p[+]},&!xfPsoprla
|
{p[+]:p[+]},&!xfPsoprla
|
||||||
(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
|
(!p W Gp) | ({(!p[*];(p[+]:(p[*];!p[+])))[:*4][:+]}<>-> (!p W Gp)),&!xPpla
|
||||||
{b[+][:*0..3]},&!fPsopra
|
{b[+][:*0..3]},&!fPsopra
|
||||||
|
{a->c[*]},fPsopra
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
run 0 ../kind input
|
run 0 ../kind input
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue