diff --git a/ChangeLog b/ChangeLog index 56313c32e..43070a7d8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,9 @@ +2011-01-04 Alexandre Duret-Lutz + + * src/tgbatest/spotlbtt.test: Add test for -l -R3b, showing many + failure because the minimization() algorithm is currently + incorrect when applied to non-weak automata. + 2011-01-04 Alexandre Duret-Lutz * src/tgbaalgos/scc.hh: Typo in documentation. diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 08c214e37..b3ef058e0 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -190,6 +190,14 @@ Algorithm Enabled = yes } +Algorithm +{ + Name = "Spot (Couvreur -- LaCIM), +pre +WDBA" + Path = "${LBTT_TRANSLATE}" + Parameters = "--spot '../ltl2tgba -r4 -R3b -Rm -F -l -t'" + Enabled = yes +} + Algorithm { Name = "Spot (Couvreur -- FM), pre + allpost reduction"