Skip to content
GitLab
Commit 866af2a7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 4087d37f
Hide whitespace changes
Inline Side-by-side
ChangeLog
View file @ 866af2a7
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.
......
bench/ltlcounter/README
View file @ 866af2a7
......@@ -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.
bench/ltlcounter/run
View file @ 866af2a7
#!/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`
......
src/tgbatest/Makefile.am
View file @ 866af2a7
......@@ -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)
src/tgbatest/ltlcounter.test
View file @ 866af2a7
#!/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,
......
src/tgbatest/ltlcounter/LTLcounter.pl deleted 100755 → 0
View file @ 4087d37f
#!/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";
src/tgbatest/ltlcounter/LTLcounterCarry.pl deleted 100755 → 0
View file @ 4087d37f
#!/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";
src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl deleted 100755 → 0
View file @ 4087d37f
#!/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";
src/tgbatest/ltlcounter/LTLcounterLinear.pl deleted 100755 → 0
View file @ 4087d37f
#!/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