alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

fix eventual/universal properties for ->/<->/xor

Browse source 
* spot/tl/formula.cc: Correctly set eventual and universal properties
for ->, <->, and xor.  This wasn't really relevant before, but there
are now situation where those are not rewritten.
* tests/core/kind.test: Adjust expected output.
* tests/core/ltl2tgba2.test: New test case, reported by Florian
Renkin.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2021-02-03 12:20:42 +01:00
parent 93d8f43285
commit c06e15e085
4 changed files with 24 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -186,6 +186,9 @@ New in spot 2.9.6.dev (not yet released)
- tgba_determinize() could create parity automata using more colors - tgba_determinize() could create parity automata using more colors
than necessary. (Related to issue #298) than necessary. (Related to issue #298)
- Some formulas using ->, <->, or xor were not properly detected as
purely universal or pure eventualities.
New in spot 2.9.6 (2021-01-18) New in spot 2.9.6 (2021-01-18)
Build: Build:

14
spot/tl/formula.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2019 Laboratoire de Recherche et Développement // Copyright (C) 2015-2019, 2021 Laboratoire de Recherche et
// de l'Epita (LRDE). // 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.
// //
@ -1283,8 +1283,8 @@ namespace spot
case op::Xor: case op::Xor:
case op::Equiv: case op::Equiv:
props = children[0]->props & children[1]->props; props = children[0]->props & children[1]->props;
is_.eventual = false; // Preserve suspendable property
is_.universal = false; is_.eventual = is_.universal = is_.eventual && is_.universal;
is_.sere_formula = is_.boolean; is_.sere_formula = is_.boolean;
is_.sugar_free_boolean = false; is_.sugar_free_boolean = false;
is_.in_nenoform = false; is_.in_nenoform = false;
@ -1310,8 +1310,10 @@ namespace spot
break; break;
case op::Implies: case op::Implies:
props = children[0]->props & children[1]->props; props = children[0]->props & children[1]->props;
is_.eventual = false; is_.eventual =
is_.universal = false; children[0]->is_universal() && children[1]->is_eventual();
is_.universal =
children[0]->is_eventual() && children[1]->is_universal();
is_.sere_formula = (children[0]->is_boolean() is_.sere_formula = (children[0]->is_boolean()
&& children[1]->is_sere_formula()); && children[1]->is_sere_formula());
is_.sugar_free_boolean = false; is_.sugar_free_boolean = false;

8
tests/core/kind.test
View file

@ -1,7 +1,7 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2010-2012, 2015, 2017, 2019 Laboratoire de Recherche # Copyright (C) 2010-2012, 2015, 2017, 2019, 2021 Laboratoire de
# et Développement de l'Epita (LRDE). # Recherche 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.
# #
@ -47,8 +47,8 @@ a U (b U (c U d)),&!xfLPgopra
a W (b W (c W d)),&!xfLPsopra a W (b W (c W d)),&!xfLPsopra
a M (b M (c M d)),&!xfLPgopra a M (b M (c M d)),&!xfLPgopra
Fa -> Fb,xLPopra Fa -> Fb,xLPopra
Ga -> Fb,xLPgopra Ga -> Fb,xLPegopra
Fa -> Gb,xLPsopra Fa -> Gb,xLPusopra
(Ga|Fc) -> Fb,xLPopra (Ga|Fc) -> Fb,xLPopra
(Ga|Fa) -> Gb,xLPopra (Ga|Fa) -> Gb,xLPopra
{a;c*;b}|->!Xb,&fPsopra {a;c*;b}|->!Xb,&fPsopra

9
tests/core/ltl2tgba2.test
View file

@ -507,3 +507,12 @@ med.hoa:4,14
high.hoa:4,14 high.hoa:4,14
EOF EOF
diff exp out diff exp out
# This used to fail because ltl-split would not detect
# the (GFa <-> (GFb & GFc & GFd & GFe & GFf & GFg & GFh)) part
# as suspendable.
f='G((a -> X((!a U b) | G!a)) & (a -> X(G!a | (!a U c))) & (a -> X(G!a
| (!a U d))) & (a -> X(G!a | (!a U e))) & (a -> X(G!a | (!a U f))) &
(a -> X(G!a | (!a U g))) & (a -> X(G!a | (!a U h)))) & (GFa <-> (GFb &
GFc & GFd & GFe & GFf & GFg & GFh))'
test 128 = `ltl2tgba -G -D "$f" --stats=%s`