From 8cdc19671950167e1329191ff692c58dd1334a95 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 12 Nov 2009 16:46:04 +0100
Subject: [PATCH] Use -l wherever we where expecting ltl2tgba to default to
 LaCIM.

* bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations.
* src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/spotlbtt.test: Likewise.
---
 ChangeLog                  |  8 ++++++++
 bench/ltl2tgba/algorithms  |  8 ++++----
 src/tgbatest/dupexp.test   |  4 ++--
 src/tgbatest/emptchk.test  | 32 ++++++++++++++++----------------
 src/tgbatest/spotlbtt.test |  6 +++---
 5 files changed, 33 insertions(+), 25 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 3154adeb1..e22c8a4d9 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,11 @@
+2009-11-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Use -l wherever we where expecting ltl2tgba to default to LaCIM.
+
+	* bench/ltl2tgba/algorithms: Use -l for all LaCIM invocations.
+	* src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
+	src/tgbatest/spotlbtt.test: Likewise.
+
 2009-11-12  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Cleanup the help of ltl2tgba.
diff --git a/bench/ltl2tgba/algorithms b/bench/ltl2tgba/algorithms
index 5aa78d95a..ee688d806 100644
--- a/bench/ltl2tgba/algorithms
+++ b/bench/ltl2tgba/algorithms
@@ -3,7 +3,7 @@ Algorithm
 {
    Name = "LaCIM, degen"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -t -D -F'"
+   Parameters = "--spot '$LTL2TGBA -l -t -D -F'"
    Enabled = yes
 }
 
@@ -11,7 +11,7 @@ Algorithm
 {
    Name = "LaCIM, gen"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -t -F'"
+   Parameters = "--spot '$LTL2TGBA -l -t -F'"
    Enabled = yes
 }
 
@@ -19,7 +19,7 @@ Algorithm
 {
    Name = "LaCIM, degen, +pre"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -t -D -r4 -F'"
+   Parameters = "--spot '$LTL2TGBA -l -t -D -r4 -F'"
    Enabled = yes
 }
 
@@ -27,7 +27,7 @@ Algorithm
 {
    Name = "LaCIM, gen, +pre"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -t -r4 -F'"
+   Parameters = "--spot '$LTL2TGBA -l -t -r4 -F'"
    Enabled = yes
 }
 
diff --git a/src/tgbatest/dupexp.test b/src/tgbatest/dupexp.test
index de5ddc576..1bcff6f95 100755
--- a/src/tgbatest/dupexp.test
+++ b/src/tgbatest/dupexp.test
@@ -31,8 +31,8 @@ dorun()
   run 0 ../ltl2tgba -f -S "$1" >output2
   test `wc -l <output1` = `wc -l <output2`
 
-  run 0 ../ltl2tgba -s "$1" >output1
-  run 0 ../ltl2tgba -S "$1" >output2
+  run 0 ../ltl2tgba -l -s "$1" >output1
+  run 0 ../ltl2tgba -l -S "$1" >output2
   test `wc -l <output1` = `wc -l <output2`
 }
 
diff --git a/src/tgbatest/emptchk.test b/src/tgbatest/emptchk.test
index 270e05a0e..d6ab2151d 100755
--- a/src/tgbatest/emptchk.test
+++ b/src/tgbatest/emptchk.test
@@ -33,21 +33,21 @@ expect_ce_do()
 
 expect_ce()
 {
-  expect_ce_do -e "$1"
-  expect_ce_do -e -D "$1"
+  expect_ce_do -e -l "$1"
+  expect_ce_do -e -l -D "$1"
   expect_ce_do -e -f "$1"
   expect_ce_do -e -f -D "$1"
-  expect_ce_do -e'Cou99(shy)' "$1"
-  expect_ce_do -e'Cou99(shy)' -D "$1"
+  expect_ce_do -e'Cou99(shy)' -l "$1"
+  expect_ce_do -e'Cou99(shy)' -l -D "$1"
   expect_ce_do -e'Cou99(shy)' -f "$1"
   expect_ce_do -e'Cou99(shy)' -f -D "$1"
-  expect_ce_do -eCVWY90 "$1"
+  expect_ce_do -eCVWY90 -l "$1"
   expect_ce_do -eCVWY90 -f "$1"
-  run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -l "$1"
   run 0 ../ltl2tgba -e'CVWY90(bsh=10M)' -f "$1"
-  run 0 ../ltl2tgba -eSE05 "$1"
+  run 0 ../ltl2tgba -eSE05 -l "$1"
   run 0 ../ltl2tgba -eSE05 -f "$1"
-  run 0 ../ltl2tgba -e'SE05(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -e'SE05(bsh=10M)' -l "$1"
   run 0 ../ltl2tgba -e'SE05(bsh=10M)' -f "$1"
   run 0 ../ltl2tgba -eTau03_opt -f "$1"
   run 0 ../ltl2tgba -eGV04 -f "$1"
@@ -58,21 +58,21 @@ expect_ce()
 
 expect_no()
 {
-  run 0 ../ltl2tgba -E "$1"
-  run 0 ../ltl2tgba -E -D "$1"
+  run 0 ../ltl2tgba -E -l "$1"
+  run 0 ../ltl2tgba -E -l -D "$1"
   run 0 ../ltl2tgba -E -f "$1"
   run 0 ../ltl2tgba -E -f -D "$1"
-  run 0 ../ltl2tgba -E'Cou99(shy)' "$1"
-  run 0 ../ltl2tgba -E'Cou99(shy)' -D "$1"
+  run 0 ../ltl2tgba -E'Cou99(shy)' -l "$1"
+  run 0 ../ltl2tgba -E'Cou99(shy)' -l -D "$1"
   run 0 ../ltl2tgba -E'Cou99(shy)' -f "$1"
   run 0 ../ltl2tgba -E'Cou99(shy)' -f -D "$1"
-  run 0 ../ltl2tgba -ECVWY90 "$1"
+  run 0 ../ltl2tgba -ECVWY90 -l "$1"
   run 0 ../ltl2tgba -ECVWY90 -f "$1"
-  run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -l "$1"
   run 0 ../ltl2tgba -E'CVWY90(bsh=10M)' -f "$1"
-  run 0 ../ltl2tgba -ESE05 "$1"
+  run 0 ../ltl2tgba -ESE05 -l "$1"
   run 0 ../ltl2tgba -ESE05 -f "$1"
-  run 0 ../ltl2tgba -E'SE05(bsh=10M)' "$1"
+  run 0 ../ltl2tgba -E'SE05(bsh=10M)' -l "$1"
   run 0 ../ltl2tgba -E'SE05(bsh=10M)' -f "$1"
   run 0 ../ltl2tgba -ETau03_opt -f "$1"
   run 0 ../ltl2tgba -EGV04 -f "$1"
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 61e2dbaf6..9769a09fc 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -32,7 +32,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM)"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -t'"
+   Parameters = "--spot '../ltl2tgba -F -l -t'"
    Enabled = yes
 }
 
@@ -40,7 +40,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), reduction of formula"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -r4 -F -t'"
+   Parameters = "--spot '../ltl2tgba -r4 -l -F -t'"
    Enabled = yes
 }
 
@@ -48,7 +48,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), degeneralized"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -t -D'"
+   Parameters = "--spot '../ltl2tgba -l -F -t -D'"
    Enabled = yes
 }