diff --git a/ChangeLog b/ChangeLog
index f085a1b6b..1c6741f68 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,15 @@
+2011-06-06  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Remove Kristin Rozier's LTLcounter.pl scripts, now that we can
+	generate these formulae with "genltl".
+
+	* src/tgbatest/ltlcounter/: Remove this directory.
+	* src/tgbatest/Makefile.am: Adjust.
+	* src/tgbatest/ltlcounter.test, bench/ltlcounter/run: Use genltl
+	to generate the formulae.
+	* bench/ltlcounter/README: Do not mention src/tgbatest/ltlcounter/
+	anymore.
+
 2011-06-06  Alexandre Duret-Lutz  <adl@va-et-vient.net>
 
 	Better layout of the LTL formula parse tree.
diff --git a/bench/ltlcounter/README b/bench/ltlcounter/README
index 866cc4c61..aedfbb9bc 100644
--- a/bench/ltlcounter/README
+++ b/bench/ltlcounter/README
@@ -13,10 +13,12 @@ describing counters was used to stress many translators.
   publisher	= {Springer-Verlag}
 }
 
-This benchmark uses the ltlcounter scripts of Kristin Y. Rozier (See
-src/tgbatest/ltlcounter/) to plot the performance of the ltl2tgba_fm
-algorithm.  Studying the behaviour of ltl2tgba_fm on this class of
-formulae helped us to improve the translation.
+For a description of these formulae, you may also see
+http://ti.arc.nasa.gov/m/profile/kyrozier/benchmarking_scripts/node5.html
+
+This benchmark used this familly of formulae to plot the performance
+of the ltl2tgba_fm algorithm.  Studying the behaviour of ltl2tgba_fm
+on this class of formulae helped us to improve the translation.
 
 Execute "./run" to compute the raw numbers, then execture
 "gnuplot plot.gnu" to plot the figures.
diff --git a/bench/ltlcounter/run b/bench/ltlcounter/run
index 65f801f5f..767c0ea1c 100755
--- a/bench/ltlcounter/run
+++ b/bench/ltlcounter/run
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement de
 # l'EPITA (LRDE)
 #
 # This file is part of Spot, a model checking library.
@@ -22,7 +22,7 @@
 
 . ./defs
 
-lcdir=$srcdir/../../src/tgbatest/ltlcounter
+lcdir=../../src/ltltest
 
 echo "# Benching ltl2tgba_fm..."
 echo "# the following values are also saved to file 'results.fm'"
@@ -30,7 +30,7 @@ echo "# time1 = translation time"
 echo "# time2 = exploration time"
 echo "# n, states, transitions, user time1, system time1, wall time1, user time1, system time2, wall time2"
 for n in 1 2 3 4 5 6 7 8 9 10 11 12 13; do
-  $LTL2TGBA -T -ks -f "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
+  $LTL2TGBA -T -ks -f "`$lcdir/genltl 18 $n`" >out 2>&1
   states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
   transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
   time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
@@ -44,7 +44,7 @@ echo "# time1 = translation time"
 echo "# time2 = exploration time"
 echo "# n, states, transitions, user time1, system time1, wall time1, user time1, system time2, wall time2"
 for n in 1 2 3 4 5 6 7; do
-  $LTL2TGBA -T -ks "`$lcdir/LTLcounterLinear.pl $n`" >out 2>&1
+  $LTL2TGBA -T -ks "`$lcdir/genltl 18 $n`" >out 2>&1
   states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out`
   transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out`
   time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out`
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 111f46d1f..a68f8d637 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -106,10 +106,7 @@ TESTS = \
   spotlbtt.test \
   complementation.test
 
-EXTRA_DIST = $(TESTS) ltlcounter/LTLcounter.pl				\
-  ltlcounter/LTLcounterCarry.pl ltlcounter/LTLcounterCarryLinear.pl	\
-  ltlcounter/LTLcounterLinear.pl ltlcounter/README			\
-  ltlcounter/software_agreement.txt
+EXTRA_DIST = $(TESTS)
 
 distclean-local:
 	rm -rf $(TESTS:.test=.dir)
diff --git a/src/tgbatest/ltlcounter.test b/src/tgbatest/ltlcounter.test
index 05274b8a0..6e77bca33 100755
--- a/src/tgbatest/ltlcounter.test
+++ b/src/tgbatest/ltlcounter.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de
+# Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement de
 # l'EPITA (LRDE)
 #
 # This file is part of Spot, a model checking library.
@@ -25,11 +25,9 @@
 
 set -e
 
-lcdir=$srcdir/ltlcounter
-lc=$lcdir/LTLcounter.pl
-lcl=$lcdir/LTLcounterLinear.pl
-lcc=$lcdir/LTLcounterCarry.pl
-lccl=$lcdir/LTLcounterCarryLinear.pl
+pwd
+lcdir=../../ltltest
+lc="$lcdir/genltl"
 
 run='run 0'
 
@@ -53,13 +51,13 @@ check_formula()
 for n in 1 2 3 4 5 6 7 8 9 10 11
 do
   :;:;: "========== $n counters ==========" ;:;:  # only visible with "set -x"
-  f=`"$lc" $n`
+  f=`"$lc" 17 $n`
   check_formula "$f"
-  f=`"$lcl" $n`
+  f=`"$lc" 18 $n`
   check_formula "$f"
-  f=`"$lcc" $n`
+  f=`"$lc" 19 $n`
   check_formula "$f"
-  f=`"$lccl" $n`
+  f=`"$lc" 20 $n`
   check_formula "$f"
 
   # Only run the first two formulae under valgrind,
diff --git a/src/tgbatest/ltlcounter/LTLcounter.pl b/src/tgbatest/ltlcounter/LTLcounter.pl
deleted file mode 100755
index 4dd1430d6..000000000
--- a/src/tgbatest/ltlcounter/LTLcounter.pl
+++ /dev/null
@@ -1,123 +0,0 @@
-#!/usr/bin/perl
-
-# LTLcounter.pl
-#
-# Input: n = the number of bits in the counter
-# 
-# Output: an LTL formula describing an n-bit counter
-#
-# Usage: LTLcounter.pl n
-#
-
-# System Description
-#
-# - 3 variables: 
-#                m = marker
-#                b = bits
-#
-# - the counter represents a sequence of n-bit strings in 2 variables
-#   ex: n=4
-#       m = 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001
-#       b = 0000 0001 0010 0011 0100 0101 0110 0111 1000 1001 1010 1011 1100 1101
-#       m marks the least-significant bit
-#       b is the sequence of bit-strings representing the counter
-#
-# - reverse bit order: in our actual LTL formula, we represent each n-length string 
-#     in reverse order (left -> right : least -> most significant bit)
-#   - the example above for n=4 becomes:
-#       m = 1000 1000 1000 1000 1000 1000 1000 1000
-#       b = 0000 1000 0100 1100 0010 1010 0110 1110
-#
-# - the LTL formula produced is true if the values of the two variables over time 
-#     represent a proper n-bit counter
-
-
-
-#################### Argument Setup ####################
-
-#Check for correct number and type of command line arguments
-if ($ARGV[0] =~ /^-v?/) {
-    $verbose = 1;
-    shift(@ARGV);
-} #end if
-else {
-    $verbose = 0;
-} #end else
-
-if (@ARGV != 1) {
-    die "Usage: LTLcounter.pl n\n\tproduces a formula describing an n-bit counter\n\tUse flag -v for verbose, human-readable output.\n";
-} #end if
-
-$n = $ARGV[0];
-
-#################### Generation of the Formula ####################
-$pattern = ""; #make sure the pattern starts empty
-$ppattern = ""; #make sure the printable pattern starts empty
-
-#Here are the parts of the formula we know to be true:
-
-#1)  The marker consists of a repeated pattern of a 1 followed by n-1 0's
-$mpattern .= "(m) && ( [](m -> (";
-for ($i = 1; $i <= $n; $i++) {
-    if ($i == $n) { $nest = "m"; }
-    else { $nest = "!m"; }
-    for ($j = 0; $j < $i; $j++) {
-	$nest = "X($nest)";
-    } #end for
-    if ($i == $n) { $mpattern .= "$nest)))"; }
-    else { $mpattern .= "($nest) && ";}
-} #end for
-
-$ppattern .= "1. $mpattern\n"; #just for now: add a return for readability
-$pattern .= "($mpattern) && ";
-
-
-#2) The bit is initially n zeros
-$bpattern = "(!b)";
-for ($i = 1; $i < $n; $i++) {
-    $nest = "!b";
-    for ($j = 0; $j < $i; $j++) {
-	$nest = "X($nest)";
-    } #end for
-    $bpattern .= " && ($nest)";
-} #end for
-$ppattern .= "2. $bpattern\n"; #just for now: add a return for readability
-$pattern .= "($bpattern) && ";
-
-
-#3) If the least significant bit is 0, next time is is 1 and the other bits are the same
-$nestb0 = "!b";
-$nestb1 = "b";
-for ($i = 1; $i <= $n; $i++) {
-    $nestb0 = "X($nestb0)";
-    $nestb1 = "X($nestb1)";
-} #end for
-$ppattern .= "3. []( (m && !b) -> ( $nestb1 && X ( ( (!m) && (b -> $nestb1) && (!b -> $nestb0) ) U m ) ) )\n";
-#$pattern .= "([] (m -> ( (b -> ($nestb0)) && ((!b) -> ($nestb1)) ) ) ) && ";
-$pattern .= "([] ((m && (!b)) -> ( ($nestb1) && (X ( ( (!m) && (b -> ($nestb1)) && ((!b) -> ($nestb0)) ) U (m) ) ) ))) && ";
-
-
-#4) For every n-length string in b, all of the bits through the first 0 will be flipped n steps later and every bit after that will remain unchanged. (This is the add one.)
-$ppattern .= "4. [] ( (m && b) -> ($nestb0 && (X ( (b && !m && $nestb0) U (m || (!m && !b && $nestb1 && X( ( !m && (b -> $nestb1) && (!b -> $nestb0) ) U m ) ) ) ) ) )\n";
-$pattern .= "([]( (m && b) -> (($nestb0) && (X ( (b && (!m) && ($nestb0)) U (m || ((!m) && (!b) && ($nestb1) && ( X( ( (!m) && (b -> ($nestb1)) && ((!b) -> ($nestb0)) ) U m ) ) ) ) ) ) ) ) )";
-
-if ($verbose == 1) {
-#    print "1) The marker consists of a repeated pattern of a 1 followed by n-1 0's then another 1\n";
-    print "1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.\n";
-#    print "2) The bit is initially n 0's\n";
-    print "2) The first n bits are 0's.\n";
-#    print "3) If the least significant bit is 0, next time it is 1 and the other bits are the same.\n";
-    print "3) If the least significant bit is 0, then it is 1 n steps later 
-   and the other bits do not change.\n";
-#    print "4) For every n-length string in b, all of the bits through the first 0 will be flipped n steps later and every bit after that will remain unchanged. (This is the add one.)\n";
-    print "4) All of the bits before and including the first 0 in an n-bit block flip their values in the next block; the other bits do not change.\n";
-    print "Pattern: \n$ppattern\n";
-} #end if
-
-$pattern =~ s/\[\]/G/g;
-$pattern =~ s/m/a/g;
-
-if ($verbose == 1) {
-    print "\nComputer readable: ";
-} #end if
-print "($pattern)\n";
diff --git a/src/tgbatest/ltlcounter/LTLcounterCarry.pl b/src/tgbatest/ltlcounter/LTLcounterCarry.pl
deleted file mode 100755
index d7a8997b4..000000000
--- a/src/tgbatest/ltlcounter/LTLcounterCarry.pl
+++ /dev/null
@@ -1,146 +0,0 @@
-#!/usr/bin/perl
-
-# LTLcounterCarry.pl
-#
-# Input: n = the number of bits in the counter
-# 
-# Output: an LTL formula describing an n-bit counter
-#
-# Purpose: Simplify the formula created by LTLcounter by eliminating the 'until' operators and using a carry bit (one more variable) instead. 
-#
-# Usage: LTLcounterCarry.pl n
-#
-
-# System Description
-#
-# - 3 variables: 
-#                m = marker
-#                b = bits
-#                c = carries
-#
-# - the counter represents a sequence of n-bit strings in 3 variables
-#   ex: n=4
-#       m = 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001
-#       b = 0000 0001 0010 0011 0100 0101 0110 0111 1000 1001 1010 1011 1100 1101
-#       c = 0000 0001 0000 0011 0000 0001 0000 0111 0000 0001 0000 0011 0000 0001
-#       m marks the least-significant bit
-#       b is the sequence of bit-strings representing the counter
-#       c is the sequence of bit-strings representing the carries from each addition
-#         ex: 0011 + 0001 = 0100 with carries 0011
-#
-# - reverse bit order: in our actual LTL formula, we represent each n-length string 
-#     in reverse order (left -> right : least -> most significant bit)
-#   - the example above for n=4 becomes:
-#       m = 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000
-#       b = 0000 1000 0100 1100 0010 1010 0110 1110 0001 1001 0101 1101 0011 1011
-#       c = 0000 1000 0000 1100 0000 1000 0000 1110 0000 1000 0000 1100 0000 1000
-#
-# - the LTL formula produced is true if the values of the three variables over time 
-#     represent a proper n-bit counter
-
-
-
-#################### Argument Setup ####################
-
-#Check for correct number and type of command line arguments
-if ($ARGV[0] =~ /^-v?/) {
-    $verbose = 1;
-    shift(@ARGV);
-} #end if
-else {
-    $verbose = 0;
-} #end else
-
-if (@ARGV != 1) {
-    die "Usage: LTLcounterCarry.pl n\n\tproduces a formula describing an n-bit counter\n\tUse flag -v for verbose, human-readable output.\n";
-} #end if
-
-$n = $ARGV[0];
-
-#################### Generation of the Formula ####################
-$pattern = ""; #make sure the pattern starts empty
-$ppattern = ""; #make sure the printable pattern starts empty
-
-#Here are the parts of the formula we know to be true:
-
-#1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.
-$mpattern .= "(m) && ( [](m -> (";
-for ($i = 1; $i <= $n; $i++) {
-    if ($i == $n) { $nest = "m"; }
-    else { $nest = "!m"; }
-    for ($j = 0; $j < $i; $j++) {
-	$nest = "X($nest)";
-    } #end for
-    if ($i == $n) { $mpattern .= "($nest))))"; }
-    else { $mpattern .= "($nest) && ";}
-} #end for
-
-$ppattern .= "1. $mpattern\n"; #just for now: add a return for readability
-$pattern .= "($mpattern) && ";
-
-
-#2) The bit is initially n 0's.
-$bpattern = "(!b)";
-for ($i = 1; $i < $n; $i++) {
-    $nest = "!b";
-    for ($j = 0; $j < $i; $j++) {
-	$nest = "X($nest)";
-    } #end for
-    $bpattern .= " && ($nest)";
-} #end for
-$ppattern .= "2. $bpattern\n"; #just for now: add a return for readability
-$pattern .= "($bpattern) && ";
-
-
-#Establish strings for "n steps from now, b is 0 (or 1)"
-$nestb0 = "!b";
-$nestb1 = "b";
-for ($i = 1; $i <= $n; $i++) {
-    $nestb0 = "X($nestb0)";
-    $nestb1 = "X($nestb1)";
-} #end for
-
-
-### Add m to b ###
-
-#3) If m is 1 and b is 0 then c is 0 and n steps later b is 1.
-$ppattern .= "3. [] ( (m && !b) -> (!c && $nestb1) )\n";
-$pattern .= "([] ((m && (!b)) -> ((!c) && ($nestb1)))) && ";
-
-
-#4) If m is 1 and b is 1 then c is 1 and n steps later b is 0.
-$ppattern .= "4. [] ( (m && b) -> (c && $nestb0) )\n";
-$pattern .= "([] ((m && b) -> (c && ($nestb0)))) && ";
-
-
-### Add in the carry ###
-
-#5) If there's no carry, then all of the bits stay the same n steps later.
-$ppattern .= "5. [] (!c && X(!m)) -> ( X(!c) && (X(b) -> X($nestb1)) && (X(!b) -> X($nestb0)) )\n";
-$pattern .= "([] ( ((!c) && X(!m)) -> ( X(!c) && (X(b) -> (X($nestb1))) && (X(!b) -> (X($nestb0)) ) ) )) && ";
-
-
-#6) If there's a carry, then add one: flip the bits of b and adjust the carry.
-$ppattern .= "6. [] (c -> ( ( X(!b) -> ( X(!c) && X($nestb0) ) ) && ( X(c) && X($nestb1) ) ))\n";
-$pattern .= "([] ( c -> ( ( X(!b) -> ( X(!c) && (X($nestb1)) ) ) && ( X(b) -> ( X(c) && (X($nestb0)) ) ) )))";
-
-
-if ($verbose == 1) {
-    print "1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.\n";
-    print "2) The bit is initially n 0's.\n";
-    print "3) If m is 1 and b is 0 then c is 0 and n steps later b is 1.\n";
-    print "4) If m is 1 and b is 1 then c is 1 and n steps later b is 0.\n";
-#    print "5) If there's no carry, then all of the bits stay the same n steps later.\n";
-    print "5) If there is no carry, then the next bit stays the same n steps later.\n";
-#    print "6) If there's a carry, then add one: flip the bits of b and adjust the carry.\n";
-    print "6) If there is a carry, flip the next bit n steps later and adjust the carry.\n";
-    print "\nPattern: \n$ppattern\n";
-} #end if
-
-$pattern =~ s/\[\]/G/g;
-$pattern =~ s/m/a/g;
-
-if ($verbose == 1) {
-    print "\nComputer readable: ";
-} #end if
-print "($pattern)\n";
diff --git a/src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl b/src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl
deleted file mode 100755
index ecac3a90b..000000000
--- a/src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl
+++ /dev/null
@@ -1,149 +0,0 @@
-#!/usr/bin/perl
-#
-#by Kristin Y. Rozier
-#
-#This software has been determined to be outside the scope of NASA NPG 2210 and therefore is not considered as controlled software.
-#
-#This program may be freely redistributed and/or modified under the terms of the enclosed software agreement. NASA is neither liable nor responsible for maintenance, updating, or correction of any errors in the software provided. Use of this software shall not be construed to constitute the grant of a license to the user under any NASA patent, patent application or other intellectual property.
-#
-#You should have received a software agreement along with this program. If not, please refer to Section 4 of: http://opensource.arc.nasa.gov/pdf/NASA_Open_Source_Agreement_1.3.txt
-############################################################################
-# LTLcounterCarryLinear.pl
-#
-# Input: n = the number of bits in the counter
-# 
-# Output: an LTL formula describing an n-bit counter
-#
-# Purpose: Simplify the formula created by LTLcounter by eliminating the 'until' operators and using a carry bit (one more variable) instead. Reduce the number of 'next' operators using nesting.
-#
-# Usage: LTLcounterCarryLinear.pl n
-#
-# Note: This program is simply an optimized version of LTLcounterCarry.pl. It formulates formulas 1 and 2 linearly (i.e X(a & X(a & X(a))) ) instead of exponentially (i.e. X(a) && X(X(a)) && X(X(X(a))) ). Formulas 3 and 4 are the same. It pulls out the 'X' out in formulas 5 and 6 so that in formula 5, 5 'X's are condenced into one and in formula 6, 6 'X's are condenced into one. 
-
-# System Description
-#
-# - 3 variables: 
-#                m = marker
-#                b = bits
-#                c = carries
-#
-# - the counter represents a sequence of n-bit strings in 3 variables
-#   ex: n=4
-#       m = 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001
-#       b = 0000 0001 0010 0011 0100 0101 0110 0111 1000 1001 1010 1011 1100 1101
-#       c = 0000 0001 0000 0011 0000 0001 0000 0111 0000 0001 0000 0011 0000 0001
-#       m marks the least-significant bit
-#       b is the sequence of bit-strings representing the counter
-#       c is the sequence of bit-strings representing the carries from each addition
-#         ex: 0011 + 0001 = 0100 with carries 0011
-#
-# - reverse bit order: in our actual LTL formula, we represent each n-length string 
-#     in reverse order (left -> right : least -> most significant bit)
-#   - the example above for n=4 becomes:
-#       m = 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000
-#       b = 0000 1000 0100 1100 0010 1010 0110 1110 0001 1001 0101 1101 0011 1011
-#       c = 0000 1000 0000 1100 0000 1000 0000 1110 0000 1000 0000 1100 0000 1000
-#
-# - the LTL formula produced is true if the values of the three variables over time 
-#     represent a proper n-bit counter
-
-
-
-#################### Argument Setup ####################
-
-#Check for correct number and type of command line arguments
-if ($ARGV[0] =~ /^-v?/) {
-    $verbose = 1;
-    shift(@ARGV);
-} #end if
-else {
-    $verbose = 0;
-} #end else
-
-if (@ARGV != 1) {
-    die "Usage: LTLcounterCarryLinear.pl n\n\tproduces a formula describing an n-bit counter\n\tUse flag -v for verbose, human-readable output.\n";
-} #end if
-
-$n = $ARGV[0];
-
-#################### Generation of the Formula ####################
-$pattern = ""; #make sure the pattern starts empty
-$ppattern = ""; #make sure the printable pattern starts empty
-
-#Here are the parts of the formula we know to be true:
-
-#1)  The marker consists of a repeated pattern of a 1 followed by n-1 0's.
-$mpattern .= "(m) && ( [](m -> (NEST)))";
-for ($i = 1; $i <= $n; $i++) {
-    if ($i == $n) { $nest = "X(m)"; }
-    else { $nest = "X(!m && NEST)"; }
-    $mpattern =~ s/NEST/$nest/;
-} #end for
-
-$ppattern .= "1. $mpattern\n"; #just for now: add a return for readability
-$pattern .= "($mpattern) && ";
-
-
-#2) The bit is initially n 0's.
-$bpattern = "(!b)NEST";
-for ($i = 1; $i < $n; $i++) {
-    $nest = " && X(!bNEST)"; 
-    $bpattern =~ s/NEST/$nest/;
-} #end for
-$nest = "";
-$bpattern =~ s/NEST/$nest/;
-
-$ppattern .= "2. $bpattern\n"; #just for now: add a return for readability
-$pattern .= "($bpattern) && ";
-
-
-#Establish strings for "n steps from now, b is 0 (or 1)"
-$nestb0 = "!b";
-$nestb1 = "b";
-for ($i = 1; $i <= $n; $i++) {
-    $nestb0 = "X($nestb0)";
-    $nestb1 = "X($nestb1)";
-} #end for
-
-
-### Add m to b ###
-
-#3) If m is 1 and b is 0 then c is 0 and n steps later b is 1.
-$ppattern .= "3. [] ( (m && !b) -> (!c && $nestb1) )\n";
-$pattern .= "([] ((m && (!b)) -> ((!c) && ($nestb1)))) && ";
-
-
-#4) If m is 1 and b is 1 then c is 1 and n steps later b is 0.
-$ppattern .= "4. [] ( (m && b) -> (c && $nestb0) )\n";
-$pattern .= "([] ((m && b) -> (c && ($nestb0)))) && ";
-
-
-### Add in the carry ###
-
-#5) If there's no carry, then all of the bits stay the same n steps later.
-$ppattern .= "5. [] (!c && X(!m)) -> (X ( ((!c) && (b -> $nestb1) && ((!b) -> $nestb0) ) ) )\n";
-$pattern .= "([] ( ((!c) && X(!m)) -> ( X ( (!c) && (b -> ($nestb1)) && ((!b) -> ($nestb0)) )) )) && ";
-
-
-#6) If there's a carry, then add one: flip the bits of b and adjust the carry.
-$ppattern .= "6. [] (c -> ( (!b -> (!c && $nestb0)) && (b -> (c && $nestb1)) ))\n";
-$pattern .= "([] ( c -> ( X ( ((!b) -> ((!c) && ($nestb1)) ) && (b -> (c && ($nestb0)) ) ))))";
-
-
-if ($verbose == 1) {
-    print "1) The marker consists of a repeated pattern of a 1 followed by n-1 0's.\n";
-    print "2) The bit is initially n 0's.\n";
-    print "3) If m is 1 and b is 0 then c is 0 and n steps later b is 1.\n";
-    print "4) If m is 1 and b is 1 then c is 1 and n steps later b is 0.\n";
-    print "5) If there's no carry, then all of the bits stay the same n steps later.\n";
-    print "6) If there's a carry, then add one: flip the bits of b and adjust the carry.\n";
-    print "\nPattern: \n$ppattern\n";
-} #end if
-
-$pattern =~ s/\[\]/G/g;
-$pattern =~ s/m/a/g;
-
-if ($verbose == 1) {
-    print "\nComputer readable: ";
-} #end if
-print "($pattern)\n";
diff --git a/src/tgbatest/ltlcounter/LTLcounterLinear.pl b/src/tgbatest/ltlcounter/LTLcounterLinear.pl
deleted file mode 100755
index 206706351..000000000
--- a/src/tgbatest/ltlcounter/LTLcounterLinear.pl
+++ /dev/null
@@ -1,132 +0,0 @@
-#!/usr/bin/perl
-#
-#by Kristin Y. Rozier
-#
-#This software has been determined to be outside the scope of NASA NPG 2210 and therefore is not considered as controlled software.
-#
-#This program may be freely redistributed and/or modified under the terms of the enclosed software agreement. NASA is neither liable nor responsible for maintenance, updating, or correction of any errors in the software provided. Use of this software shall not be construed to constitute the grant of a license to the user under any NASA patent, patent application or other intellectual property.
-#
-#You should have received a software agreement along with this program. If not, please refer to Section 4 of: http://opensource.arc.nasa.gov/pdf/NASA_Open_Source_Agreement_1.3.txt
-############################################################################
-# LTLcounterLinear.pl
-#
-# Input: n = the number of bits in the counter
-# 
-# Output: an LTL formula describing an n-bit counter
-#
-# Purpose: Simplify the formula created by LTLcounter by reducing the number of 'next' operators using nesting.
-#
-# Usage: LTLcounterLinear.pl n
-#
-# Note: This program is simply an optimized version of LTLcounter.pl. It shares one extra 'X' in formula 3, two 'X's in formula 4, and formulates formulas 1 and 2 linearly (i.e X(a & X(a & X(a))) ) instead of exponentially (i.e. X(a) && X(X(a)) && X(X(X(a))) )
-
-# System Description
-#
-# - 3 variables: 
-#                m = marker
-#                b = bits
-#
-# - the counter represents a sequence of n-bit strings in 2 variables
-#   ex: n=4
-#       m = 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001 0001
-#       b = 0000 0001 0010 0011 0100 0101 0110 0111 1000 1001 1010 1011 1100 1101
-#       m marks the least-significant bit
-#       b is the sequence of bit-strings representing the counter
-#
-# - reverse bit order: in our actual LTL formula, we represent each n-length string 
-#     in reverse order (left -> right : least -> most significant bit)
-#   - the example above for n=4 becomes:
-#       m = 1000 1000 1000 1000 1000 1000 1000 1000
-#       b = 0000 1000 0100 1100 0010 1010 0110 1110
-#
-# - the LTL formula produced is true if the values of the two variables over time 
-#     represent a proper n-bit counter
-
-
-
-#################### Argument Setup ####################
-
-#Check for correct number and type of command line arguments
-if ($ARGV[0] =~ /^-v?/) {
-    $verbose = 1;
-    shift(@ARGV);
-} #end if
-else {
-    $verbose = 0;
-} #end else
-
-if (@ARGV != 1) {
-    die "Usage: LTLcounterLinear.pl n\n\tproduces a formula (linear in n) describing an n-bit counter\n\tUse flag -v for verbose, human-readable output.\n";
-} #end if
-
-$n = $ARGV[0]; 
-
-#################### Generation of the Formula ####################
-$pattern = ""; #make sure the pattern starts empty
-$ppattern = ""; #make sure the printable pattern starts empty
-
-#Here are the parts of the formula we know to be true:
-
-#1)  The marker consists of a repeated pattern of a 1 followed by n-1 0's
-$mpattern .= "(m) && ( [](m -> (NEST)))";
-for ($i = 1; $i <= $n; $i++) {
-    if ($i == $n) { $nest = "X(m)"; }
-    else { $nest = "X(!m && NEST)"; }
-    $mpattern =~ s/NEST/$nest/;
-} #end for
-
-$ppattern .= "1. $mpattern\n"; #just for now: add a return for readability
-$pattern .= "($mpattern) && ";
-
-
-#2) The bit is initially n 0's.
-$bpattern = "(!b)NEST";
-for ($i = 1; $i < $n; $i++) {
-    $nest = " && X(!bNEST)"; 
-    $bpattern =~ s/NEST/$nest/;
-} #end for
-$nest = "";
-$bpattern =~ s/NEST/$nest/;
-
-$ppattern .= "2. $bpattern\n"; #just for now: add a return for readability
-$pattern .= "($bpattern) && ";
-
-
-#3) If the least significant bit is 0, next time is is 1 and the other bits are the same.
-$nestb0m1 = "!b";
-$nestb1m1 = "b";
-for ($i = 1; $i <= $n; $i++) {
-    if ($i == $n) {
-	$nestb0 = "X($nestb0m1)";
-	$nestb1 = "X($nestb1m1)";
-    } #end if
-    else {
-	$nestb0m1 = "X($nestb0m1)";
-	$nestb1m1 = "X($nestb1m1)";
-    } #end else
-} #end for
-$ppattern .= "3. []( (m && !b) -> ( X ( $nestb1m1 && ( ( (!m) && (b -> $nestb1) && (!b -> $nestb0) ) U m ) ) ) )\n";
-#$pattern .= "([] (m -> ( (b -> ($nestb0)) && ((!b) -> ($nestb1)) ) ) ) && ";
-$pattern .= "([]( (m && (!b)) -> ( X ( ($nestb1m1) && ( ( (!m) && (b -> ($nestb1)) && ((!b) -> ($nestb0)) ) U (m) ) ) ) )) && ";
-#$pattern .= "([] ((m && (!b)) -> ( X ( ( ($nestb1m1) && (!m) && (b -> ($nestb1)) && ((!b) -> ($nestb0)) ) U (m) ) ) )) && ";
-
-
-#4) For every n-length string in b, all of the bits through the first 0 will be flipped n steps later and every bit after that will remain unchanged. (This is the add one.)
-$ppattern .= "4. [] ( (m && b) -> (X ($nestb0m1 && ( (b && !m && $nestb0) U (m || (!m && !b && X( $nestb1m1 && ( ( !m && (b -> $nestb1) && (!b -> $nestb0) ) U m ) ) ) ) ) ) ) )\n";
-$pattern .= "([] ( (m && b) -> (X (($nestb0m1) && ( ((b) && (!m) && ($nestb0)) U ((m) || ((!m) && (!b) && (X( ($nestb1m1) && ( ( (!m) && ((b) -> ($nestb1)) && ((!b) -> ($nestb0)) ) U (m) ) )) ) ) ) ) ) ))";
-
-if ($verbose == 1) {
-    print "1) The marker consists of a repeated pattern of a 1 followed by n-1 0's then another 1\n";
-    print "2) The bit is initially n 0's\n";
-    print "3) If the least significant bit is 0, next time it is 1 and the other bits are the same.\n";
-    print "4) For every n-length string in b, all of the bits through the first 0 will be flipped n steps later and every bit after that will remain unchanged. (This is the add one.)\n";
-    print "Pattern: \n$ppattern\n";
-} #end if
-
-$pattern =~ s/\[\]/G/g;
-$pattern =~ s/m/a/g;
-
-if ($verbose == 1) {
-    print "\nComputer readable: ";
-} #end if
-print "($pattern)\n";
diff --git a/src/tgbatest/ltlcounter/README b/src/tgbatest/ltlcounter/README
deleted file mode 100644
index f32926738..000000000
--- a/src/tgbatest/ltlcounter/README
+++ /dev/null
@@ -1,3 +0,0 @@
-The Perl scripts in this directory were written
-by Kristin Y. Rozier and comes from
-http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
diff --git a/src/tgbatest/ltlcounter/software_agreement.txt b/src/tgbatest/ltlcounter/software_agreement.txt
deleted file mode 100644
index 92ae76ee3..000000000
--- a/src/tgbatest/ltlcounter/software_agreement.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-This software was written by Kristin Y. Rozier, a civil servant of NASA Langley Research Center. It has been determined to be outside the scope of NASA NPG 2210 and therefore is not considered as controlled software.
-
-This program may be freely redistributed and/or modified under the terms of this software agreement. 
-
-NASA is neither liable nor responsible for maintenance, updating, or correction of any errors in the software provided. 
-
-Use of this software shall not be construed to constitute the grant of a license to the user under any NASA patent, patent application or other intellectual property.
-
-THE SOFTWARE IS PROVIDED 'AS IS' WITHOUT ANY WARRANTY OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, ANY WARRANTY THAT THE SOFTWARE WILL CONFORM TO SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, AND FREEDOM FROM INFRINGEMENT, AND ANY WARRANTY THAT THE DOCUMENTATION WILL CONFORM TO THE SOFTWARE, OR ANY WARRANTY THAT THE SOFTWARE WILL BE ERROR FREE.  IN NO EVENT SHALL NASA BE LIABLE FOR ANY DAMAGES, INCLUDING, BUT NOT LIMITED TO, DIRECT, INDIRECT, SPECIAL OR CONSEQUENTIAL DAMAGES, ARISING OUT OF, RESULTING FROM, OR IN ANY WAY CONNECTED WITH THIS SOFTWARE, WHETHER OR NOT BASED UPON WARRANTY, CONTRACT, TORT , OR OTHERWISE, WHETHER OR NOT INJURY WAS SUSTAINED BY PERSONS OR PROPERTY OR OTHERWISE, AND WHETHER OR NOT LOSS WAS SUSTAINED FROM, OR AROSE OUT OF THE RESULTS OF, OR USE OF, THE SOFTWARE OR SERVICES PROVIDED HEREUNDER.
- 
-RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST THE U.S. GOVERNMENT, THE U.S. GOVERNMENT'S CONTRACTORS AND SUBCONTRACTORS, AND SHALL INDEMNIFY AND HOLD HARMLESS THE U.S. GOVERNMENT AND THE U.S. GOVERNMENT'S CONTRACTORS AND SUBCONTRACTORS FOR ANY DAMAGE THAT MAY BE INCURRED FROM RECIPIENT'S PRIOR OR FUTURE USE OF THE PROVIDED SOFTWARE, INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, THE USE THEREOF.  RECIPIENT AGREES TO OBTAIN THIS IDENTICAL WAIVER OF CLAIMS, INDEMNIFICATION AND HOLD HARMLESS AGREEMENT WITH ANY ENTITIES THAT ARE PROVIDED WITH TECHNICAL DATA DERIVED FROM USE OF THE SOFTWARE.