Fix a longstanding bug reported by Kristin Y. Rozier..
* src/ltlast/formula.hh (formula_ptr_less_than::operator()): Fix a typo where `l' was typed as `1'. * src/tgbatest/ltlcounter/: New files from Kristin Y. Rozier. * src/tgbatest/ltlcounter.test: New * src/tgbatest/Makefile.am (TESTS): Add ltlcounter.test. (EXTRA_DIST): Add files in ltlcounter/.
This commit is contained in:
Alexandre Duret-Lutz
parent
24b78fde34
commit
6fb7e9faff
10 changed files with 644 additions and 3 deletions
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2008 Laboratoire d'Informatique de
|
||||
// Copyright (C) 2003, 2004, 2005, 2008, 2009 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
|
|
@ -144,7 +144,7 @@ namespace spot
|
|||
assert(right);
|
||||
size_t l = left->hash();
|
||||
size_t r = right->hash();
|
||||
if (1 != r)
|
||||
if (l != r)
|
||||
return l < r;
|
||||
return left->dump() < right->dump();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -94,10 +94,14 @@ TESTS = \
|
|||
emptchke.test \
|
||||
dfs.test \
|
||||
emptchkr.test \
|
||||
ltlcounter.test \
|
||||
spotlbtt.test \
|
||||
complementation.test
|
||||
|
||||
EXTRA_DIST = $(TESTS)
|
||||
EXTRA_DIST = $(TESTS) ltlcounter/LTLcounter.pl \
|
||||
ltlcounter/LTLcounterCarry.pl ltlcounter/LTLcounterCarryLinear.pl \
|
||||
ltlcounter/LTLcounterLinear.pl ltlcounter/README \
|
||||
ltlcounter/software_agreement.txt
|
||||
|
||||
distclean-local:
|
||||
rm -rf $(TESTS:.test=.dir)
|
||||
|
|
|
|||
62
src/tgbatest/ltlcounter.test
Executable file
62
src/tgbatest/ltlcounter.test
Executable file
|
|
@ -0,0 +1,62 @@
|
|||
#!/bin/sh
|
||||
|
||||
# Copyright (C) 2009 Laboratoire de Recherche et Développement de
|
||||
# l'EPITA (LRDE)
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 2 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with Spot; see the file COPYING. If not, write to the Free
|
||||
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
# 02111-1307, USA.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
lcdir=$srcdir/../ltlcounter
|
||||
lc=$lcdir/LTLcounter.pl
|
||||
lcl=$lcdir/LTLcounterLinear.pl
|
||||
lcc=$lcdir/LTLcounterCarry.pl
|
||||
lccl=$lcdir/LTLcounterCarryLinear.pl
|
||||
|
||||
check_formula()
|
||||
{
|
||||
# First, check the satisfiability of the formula with Spot
|
||||
run 0 ../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
|
||||
}
|
||||
|
||||
# Kristin Y. Rozier reported that the formulae with n=10 were badly
|
||||
# translated. Each of these formulae should have exactly one
|
||||
# accepting path, but in this case the emptiness returned an automata
|
||||
# without cycle. It turned out the function used to compare LTL
|
||||
# formulae was bugged when two LTL formulae had the same hash value,
|
||||
# so the translation of the formula stopped midway, on a formula it
|
||||
# thought it had already seen.
|
||||
|
||||
for i in 1 2 3 4 5 6 7 8 9 10 11 12
|
||||
do
|
||||
:;:;: "========== $i counters ==========" ;:;: # only visible with "set -x"
|
||||
f=`"$lc" $i`
|
||||
check_formula "$f"
|
||||
f=`"$lcl" $i`
|
||||
check_formula "$f"
|
||||
f=`"$lcc" $i`
|
||||
check_formula "$f"
|
||||
f=`"$lccl" $i`
|
||||
check_formula "$f"
|
||||
done
|
||||
123
src/tgbatest/ltlcounter/LTLcounter.pl
Executable file
123
src/tgbatest/ltlcounter/LTLcounter.pl
Executable file
|
|
@ -0,0 +1,123 @@
|
|||
#!/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";
|
||||
146
src/tgbatest/ltlcounter/LTLcounterCarry.pl
Executable file
146
src/tgbatest/ltlcounter/LTLcounterCarry.pl
Executable file
|
|
@ -0,0 +1,146 @@
|
|||
#!/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";
|
||||
149
src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl
Executable file
149
src/tgbatest/ltlcounter/LTLcounterCarryLinear.pl
Executable file
|
|
@ -0,0 +1,149 @@
|
|||
#!/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";
|
||||
132
src/tgbatest/ltlcounter/LTLcounterLinear.pl
Executable file
132
src/tgbatest/ltlcounter/LTLcounterLinear.pl
Executable file
|
|
@ -0,0 +1,132 @@
|
|||
#!/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";
|
||||
3
src/tgbatest/ltlcounter/README
Normal file
3
src/tgbatest/ltlcounter/README
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
The Perl scripts in this directory were written
|
||||
by Kristin Y. Rozier and comes from
|
||||
http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
|
||||
11
src/tgbatest/ltlcounter/software_agreement.txt
Normal file
11
src/tgbatest/ltlcounter/software_agreement.txt
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
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.
|
||||
Loading…
Add table
Add a link
Reference in a new issue