diff --git a/NEWS b/NEWS index da2211029..1a309583c 100644 --- a/NEWS +++ b/NEWS @@ -61,6 +61,7 @@ New in spot 1.99.4a (not yet released) * "randaut -Q0 1" used to segfault. * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. * "ltlgrind --help" did not document FORMAT. + * unabbreviate could easily use forbidden operators New in spot 1.99.4 (2015-10-01) diff --git a/src/tests/unabbrevwm.test b/src/tests/unabbrevwm.test index fff7c357f..a41b9c880 100755 --- a/src/tests/unabbrevwm.test +++ b/src/tests/unabbrevwm.test @@ -40,7 +40,10 @@ test `uniq out | wc -l` = 1 for i in 'GFa' 'a R b' 'a W b' 'a M b'; do for fg in '' F G GF; do for rwm in '' R W M RW RM WM RWM; do - $ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" + $ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out + test -n "$rwm" && grep "[$rwm]" out && exit 1 done done done + +true diff --git a/src/tl/unabbrev.cc b/src/tl/unabbrev.cc index c1a25c72c..d0bf6cd91 100644 --- a/src/tl/unabbrev.cc +++ b/src/tl/unabbrev.cc @@ -205,7 +205,7 @@ namespace spot auto gf2 = formula::G(f2); if (re_g_) gf2 = run(gf2); - out = formula::U(f2, formula::Or({f12, out})); + out = formula::U(f2, formula::Or({f12, gf2})); break; } case op::W: @@ -225,8 +225,8 @@ namespace spot } auto gf1 = formula::G(f1); if (re_g_) - gf1 = rec(gf1); - out = formula::U(f1, formula::Or({f2, out})); + gf1 = run(gf1); + out = formula::U(f1, formula::Or({f2, gf1})); break; } case op::M: diff --git a/wrap/python/tests/randltl.ipynb b/wrap/python/tests/randltl.ipynb index dca0ebc00..7b69fe532 100644 --- a/wrap/python/tests/randltl.ipynb +++ b/wrap/python/tests/randltl.ipynb @@ -18,7 +18,7 @@ "version": "3.4.3+" }, "name": "", - "signature": "sha256:b69bb80f870979f9654dbf2c1bcc0f26f652956e1f1ea4189d5c8078caa067c6" + "signature": "sha256:c1de5aacd024bbec64b75f61a13e53562185c906051312d9ce5067236b7899d4" }, "nbformat": 3, "nbformat_minor": 0, @@ -648,13 +648,13 @@ "text": [ "0\n", "!(1 U !p1)\n", - "1 U ((p0 U ((p0 & p1) | (p1 R p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n", - "1 U (!p2 U ((p0 & !p2) | (p0 R !p2)))\n", - "(!p1 U (((1 U !(1 U !p1)) R !p1) | (!p1 & (1 U !(1 U !p1))))) | !(1 U !(p0 | (1 U p1)))\n", - "X(p2 & X(p2 U (!p0 | (p2 W !p0))))\n", + "1 U ((p0 U ((p0 & p1) | !(1 U !p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n", + "1 U (!p2 U ((p0 & !p2) | !(1 U p2)))\n", + "(!p1 U ((!p1 & (1 U !(1 U !p1))) | !(1 U p1))) | !(1 U !(p0 | (1 U p1)))\n", + "X(p2 & X(p2 U (!p0 | !(1 U !p2))))\n", "(1 U p2) | (X(!p2 | !(1 U !p2)) U ((1 U p2) U (!p1 & (1 U p2))))\n", "XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n", - "XX(1 U (p1 U ((p0 & p1) | (p0 R p1))))\n", + "XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))\n", "p2 & Xp0\n" ] }