From f4e583d0786a28f72e64c545b4ba4ed2ba3acc54 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 4 Jan 2011 14:33:04 +0100
Subject: [PATCH] * 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.

---
 ChangeLog                  | 6 ++++++
 src/tgbatest/spotlbtt.test | 8 ++++++++
 2 files changed, 14 insertions(+)

diff --git a/ChangeLog b/ChangeLog
index 56313c32e..43070a7d8 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2011-01-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* 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  <adl@lrde.epita.fr>
 
 	* 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"