From dcd4644d427cda397c997b1c7655cf1ddae331a4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Jan 2013 11:30:16 +0100
Subject: [PATCH] eltl2tgba: slight cleanup of the tests.

* src/eltltest/acc.test, src/tgbatest/eltl2tgba.test: Simplify use of
here documents, and also test for ltl2tgba's -lo option with valgrind.
---
 src/eltltest/acc.test       | 37 +++++++++++++-------------
 src/tgbatest/eltl2tgba.test | 52 +++++++++++++++++++++----------------
 2 files changed, 48 insertions(+), 41 deletions(-)

diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test
index a90830920..192f4ce52 100755
--- a/src/eltltest/acc.test
+++ b/src/eltltest/acc.test
@@ -1,5 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2009 Laboratoire de Recherche et Développement
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2013 Laboratoire de Recherche et DĂ©veloppement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -20,18 +21,18 @@
 . ./defs || exit 1
 
 set -e
-cat >prelude <<EOF
+cat >prelude <<'EOF'
 X=(
-    0 1 \$0
+    0 1 $0
     accept 1
   )
 EOF
 
-cat >input <<EOF
+cat >input <<'EOF'
 include prelude
 A=(
-    0 1 \$2
-    1 2 \$0
+    0 1 $2
+    1 2 $0
     accept 0
   )
 %
@@ -39,11 +40,11 @@ A(1,a,a|b)&X(!f)
 EOF
 run 0 ../acc input || exit 1
 
-cat >input <<EOF
+cat >input <<'EOF'
 include prelude
 A=(
-    0 1 \$2
-    1 2 \$0
+    0 1 $2
+    1 2 $0
     accept 0
   )
 %
@@ -51,28 +52,28 @@ A(1,a)
 EOF
 run 1 ../acc input || exit 1
 
-cat >input <<EOF
+cat >input <<'EOF'
 X=(
     0 1 true
-    1 2 \$0
+    1 2 $0
     accept 2
   )
 U=(
-    0 0 \$0
-    0 1 \$1
+    0 0 $0
+    0 1 $1
     accept 1
   )
-F=U(true, \$0)
-R=!U(!\$0, !\$1)
+F=U(true, $0)
+R=!U(!$0, !$1)
 %
 a U b | a R b | F(true) | U(a,b) -> R(a,b)
 EOF
 run 0 ../acc input || exit 1
 
-cat >input <<EOF
+cat >input <<'EOF'
 U=(
-    0 0 \$0
-    0 1 \$1
+    0 0 $0
+    0 1 $1
     accept 1
   )
 T=U(true,true)
diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test
index 62c83cc20..201e40e32 100755
--- a/src/tgbatest/eltl2tgba.test
+++ b/src/tgbatest/eltl2tgba.test
@@ -1,6 +1,7 @@
 #!/bin/sh
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# -*- coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2013 Laboratoire de Recherche et
+# DĂ©veloppement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -38,24 +39,29 @@ check_false()
   run 1 ../ltl2tgba -CR -e -Poutput -f "$1"
 }
 
+for f in 'GFa' 'FGb' 'GFa->GFb'; do
+  run 0 ../ltl2tgba -lo -b "$f" > output
+  check_false "!($f)"
+done
+
 # Create the prelude file.
-cat >input1 <<EOF
+cat >input1 <<'EOF'
 X=(
     0 1 true
-    1 2 \$0
+    1 2 $0
     accept 2
   )
 U=(
-    0 0 \$0
-    0 1 \$1
+    0 0 $0
+    0 1 $1
     accept 1
   )
 G=(
-    0 0 \$0
+    0 0 $0
   )
-F=U(true, \$0)
-Strong=G(F(\$0))->G(F(\$1))
-R=!U(!\$0, !\$1)
+F=U(true, $0)
+Strong=G(F($0))->G(F($1))
+R=!U(!$0, !$1)
 EOF
 
 cat >input <<EOF
@@ -152,10 +158,10 @@ check_construct input
 check_true 'a R b'
 check_false '!(a R b)'
 
-cat >input <<EOF
+cat >input <<'EOF'
 T=(
     0 1 true
-    1 0 \$0
+    1 0 $0
   )
 %
 T(f)
@@ -163,14 +169,14 @@ EOF
 
 check_construct input
 
-cat >input <<EOF
+cat >input <<'EOF'
 include input1
 Fusion=
   (
-   0 1 \$0 & !finish(\$0)
-   1 1 !finish(\$0)
-   1 2 \$1 & finish(\$0)
-   0 2 \$0 & \$1 & finish(\$0)
+   0 1 $0 & !finish($0)
+   1 1 !finish($0)
+   1 2 $1 & finish($0)
+   0 2 $0 & $1 & finish($0)
    accept 2
   )
 %
@@ -179,14 +185,14 @@ EOF
 
 check_construct input
 
-cat >input <<EOF
+cat >input <<'EOF'
 Concat=
   (
-   0 1 \$0 & !finish(\$0)
-   1 1 !finish(\$0)
-   1 2 finish(\$0)
-   0 2 \$0 & finish(\$0)
-   2 3 \$1
+   0 1 $0 & !finish($0)
+   1 1 !finish($0)
+   1 2 finish($0)
+   0 2 $0 & finish($0)
+   2 3 $1
    accept 3
   )
 %