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

fix unabbreviate

Browse source 
This is a bug:

    % ltlfilt -f 'a W b' --unabbreviate=WR
    a U (b | (a W b))

* src/tl/unabbrev.cc: Here.
* src/tests/unabbrevwm.test: Harden test case.
* wrap/python/tests/randltl.ipynb: Adjust expected output.
* NEWS: Mention the fix.
This commit is contained in:
Alexandre Duret-Lutz 2015-10-19 10:22:59 +02:00
parent 43a5187ab4
commit e1ddf97862
4 changed files with 14 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
NEWS
View file

@ -61,6 +61,7 @@ New in spot 1.99.4a (not yet released)
* "randaut -Q0 1" used to segfault. * "randaut -Q0 1" used to segfault.
* "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns.
* "ltlgrind --help" did not document FORMAT. * "ltlgrind --help" did not document FORMAT.
* unabbreviate could easily use forbidden operators
New in spot 1.99.4 (2015-10-01) New in spot 1.99.4 (2015-10-01)

5
src/tests/unabbrevwm.test
View file

@ -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 i in 'GFa' 'a R b' 'a W b' 'a M b'; do
for fg in '' F G GF; do for fg in '' F G GF; do
for rwm in '' R W M RW RM WM RWM; 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 done
done done
true

6
src/tl/unabbrev.cc
View file

@ -205,7 +205,7 @@ namespace spot
auto gf2 = formula::G(f2); auto gf2 = formula::G(f2);
if (re_g_) if (re_g_)
gf2 = run(gf2); gf2 = run(gf2);
out = formula::U(f2, formula::Or({f12, out})); out = formula::U(f2, formula::Or({f12, gf2}));
break; break;
} }
case op::W: case op::W:
@ -225,8 +225,8 @@ namespace spot
} }
auto gf1 = formula::G(f1); auto gf1 = formula::G(f1);
if (re_g_) if (re_g_)
gf1 = rec(gf1); gf1 = run(gf1);
out = formula::U(f1, formula::Or({f2, out})); out = formula::U(f1, formula::Or({f2, gf1}));
break; break;
} }
case op::M: case op::M:

12
wrap/python/tests/randltl.ipynb
View file

@ -18,7 +18,7 @@
"version": "3.4.3+" "version": "3.4.3+"
}, },
"name": "", "name": "",
"signature": "sha256:b69bb80f870979f9654dbf2c1bcc0f26f652956e1f1ea4189d5c8078caa067c6" "signature": "sha256:c1de5aacd024bbec64b75f61a13e53562185c906051312d9ce5067236b7899d4"
}, },
"nbformat": 3, "nbformat": 3,
"nbformat_minor": 0, "nbformat_minor": 0,
@ -648,13 +648,13 @@
"text": [ "text": [
"0\n", "0\n",
"!(1 U !p1)\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 ((p0 U ((p0 & p1) | !(1 U !p0))) | !(1 U !((1 U !p1) & (1 U p1))))\n",
"1 U (!p2 U ((p0 & !p2) | (p0 R !p2)))\n", "1 U (!p2 U ((p0 & !p2) | !(1 U p2)))\n",
"(!p1 U (((1 U !(1 U !p1)) R !p1) | (!p1 & (1 U !(1 U !p1))))) | !(1 U !(p0 | (1 U p1)))\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 | (p2 W !p0))))\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", "(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 !((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" "p2 & Xp0\n"
] ]
} }