From b57fdcb6844e7630795e5d0fe82d930968d8e913 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 5 Nov 2009 14:12:47 +0100
Subject: [PATCH] * src/tgbatest/ltlcounter.test (run): Only construct small
 formulae (i.e. n<=2) under valgrind.  The test case is too slow otherwise.

---
 ChangeLog                    |  6 ++++++
 src/tgbatest/ltlcounter.test | 14 +++++++++++---
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index de0dc5b7a..cdb33c9b7 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2009-11-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	* src/tgbatest/ltlcounter.test (run): Only construct small
+	formulae (i.e. n<=2) under valgrind.  The test case is too
+	slow otherwise.
+
 2009-11-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix spurious failure of style.test.
diff --git a/src/tgbatest/ltlcounter.test b/src/tgbatest/ltlcounter.test
index b1fb2df0f..cd2583ec0 100755
--- a/src/tgbatest/ltlcounter.test
+++ b/src/tgbatest/ltlcounter.test
@@ -31,13 +31,15 @@ lcl=$lcdir/LTLcounterLinear.pl
 lcc=$lcdir/LTLcounterCarry.pl
 lccl=$lcdir/LTLcounterCarryLinear.pl
 
+run='run 0'
+
 check_formula()
 {
   # First, check the satisfiability of the formula with Spot
-  run 0 ../ltl2tgba -e -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -x -f "$1" >/dev/null
   # Also check the satisfiability of the degeneralized formula
-  run 0 ../ltl2tgba -e -D -x -f "$1" >/dev/null
-  run 0 ../ltl2tgba -e -DS -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -D -x -f "$1" >/dev/null
+  $run ../ltl2tgba -e -DS -x -f "$1" >/dev/null
 }
 
 # Kristin Y. Rozier reported that the formulae with n=10 were badly
@@ -59,4 +61,10 @@ do
   check_formula "$f"
   f=`"$lccl" $i`
   check_formula "$f"
+  
+  # Only run the first two formulae under valgrind, 
+  # it is too slow otherwise.
+  if test $i = 2; then
+     run=:
+  fi
 done