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

gfguarantee: fix handling of true/false languages

Browse source 
Fixes #546 (again).

* spot/twaalgos/gfguarantee.cc (g_f_terminal_inplace): Detect
true/false languages early, so that we do not tag them as
non-inherently-weak.
* tests/core/ltlcross.test: Improve test case.
This commit is contained in:
Alexandre Duret-Lutz 2023-11-14 15:40:24 +01:00
parent 13f66e55af
commit 997f7ec7fb
2 changed files with 15 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
tests/core/ltlcross.test
View file

@ -70,4 +70,6 @@ ltlcross --verbose ltl2tgba ltl2tgba \
ltlcross ltl2tgba -f '!(X(v3 | G!v5) | ((Xv5 & !(v5 & !X!v3)) U !v5))'
# Issue #546.
ltlcross 'ltl2tgba --medium -p' 'ltl2tgba -p' -f 'a | FGa | GF(!b | Gb)'
ltlcross 'ltl2tgba --medium -p' 'ltl2tgba -p' 'ltl2tgba --medium -D -p' \
-f 'a | FGa | GF(!b | Gb)' \
-f '(~ v1 U ~ v5) | G(F v9 & F G v1) | G F(~ v7 | G v7 | G v3)'