* src/ltltest/defs.in (run): New function, run valgrind.
* src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run(). * Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files, Automake 1.8 find them automatically. * configure.ac: Require Automake 1.8, in gnits mode, and check for valgrind. * THANKS: New empty file.
This commit is contained in:
Alexandre Duret-Lutz
parent
c2892a8275
commit
6f88e518a9
14 changed files with 167 additions and 160 deletions
11
ChangeLog
11
ChangeLog
|
|
@ -1,5 +1,16 @@
|
|||
2003-12-29 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/ltltest/defs.in (run): New function, run valgrind.
|
||||
* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
|
||||
src/ltltest/nenoform.test, src/ltltest/parse.test,
|
||||
src/ltltest/parseerr.test, src/ltltest/tostring.test,
|
||||
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run().
|
||||
* Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files,
|
||||
Automake 1.8 find them automatically.
|
||||
* configure.ac: Require Automake 1.8, in gnits mode, and check
|
||||
for valgrind.
|
||||
* THANKS: New empty file.
|
||||
|
||||
* doc/Doxyfile.in: Upgrade to Doxygen 1.3.5. Build
|
||||
documentation for iface/.
|
||||
* dox/mainpage.dox: Fix reference to ltl_to_tgba.
|
||||
|
|
|
|||
4
HACKING
4
HACKING
|
|
@ -10,11 +10,11 @@ Here are the tools you need to bootstrap the CVS tree, or more
|
|||
generally if you plan to regenerate some of the generated files.
|
||||
|
||||
GNU Autoconf 2.57
|
||||
GNU Automake 1.7.8
|
||||
GNU Automake 1.8
|
||||
GNU Flex (the version probably doesn't matter much, we used 2.5.4)
|
||||
The CVS version of GNU Bison (called 1.875b at the time of writing)
|
||||
SWIG 1.3.19
|
||||
Doxygen 1.3.4
|
||||
Doxygen 1.3.5
|
||||
|
||||
Bootstrap the CVS tree by running
|
||||
|
||||
|
|
|
|||
12
Makefile.am
12
Makefile.am
|
|
@ -29,14 +29,4 @@ endif WITH_INCLUDED_LBTT
|
|||
SUBDIRS = $(MAYBE_BUDDY) $(MAYBE_LBTT) doc src wrap iface
|
||||
|
||||
ACLOCAL_AMFLAGS = -I m4
|
||||
EXTRA_DIST = \
|
||||
m4/buddy.m4 \
|
||||
m4/debug.m4 \
|
||||
m4/devel.m4 \
|
||||
m4/gccoptim.m4 \
|
||||
m4/gccwarn.m4 \
|
||||
m4/gspnlib.m4 \
|
||||
m4/lbtt.m4 \
|
||||
m4/ndebug.m4 \
|
||||
m4/pypath.m4 \
|
||||
HACKING
|
||||
EXTRA_DIST = HACKING
|
||||
|
|
|
|||
0
THANKS
Normal file
0
THANKS
Normal file
|
|
@ -22,7 +22,7 @@
|
|||
AC_PREREQ([2.57])
|
||||
AC_INIT([spot], [0.0m])
|
||||
AC_CONFIG_AUX_DIR([tools])
|
||||
AM_INIT_AUTOMAKE([nostdinc check-news 1.7.3])
|
||||
AM_INIT_AUTOMAKE([gnits nostdinc 1.8])
|
||||
|
||||
adl_ENABLE_DEVEL
|
||||
adl_CHECK_PYTHON
|
||||
|
|
@ -46,6 +46,7 @@ ad_GCC_OPTIM
|
|||
adl_NDEBUG
|
||||
|
||||
AC_CHECK_PROG([DOT], [dot], [dot])
|
||||
AC_CHECK_PROG([VALGRIND], [valgrind], [valgrind])
|
||||
|
||||
AC_CONFIG_FILES([
|
||||
Makefile
|
||||
|
|
|
|||
|
|
@ -46,6 +46,26 @@ test -z "$VERBOSE" && exec >/dev/null 2>&1
|
|||
echo "== Running test $0"
|
||||
|
||||
DOT='@DOT@'
|
||||
VALGRIND='@VALGRIND@'
|
||||
|
||||
run()
|
||||
{
|
||||
expected_exitcode=$1
|
||||
shift
|
||||
exitcode=0
|
||||
if test -n "$VALGRIND"; then
|
||||
exec 6>valgrind.err
|
||||
# No --leak-check=yes for now, as it causes parserr.test to fail.
|
||||
GLIBCPP_FORCE_NEW=1 \
|
||||
$VALGRIND --logfile-fd=6 -q "$@" || exitcode=$?
|
||||
cat valgrind.err 1>&2
|
||||
test -z "`sed 1q valgrind.err`" || exit 50
|
||||
rm -f valgrind.err
|
||||
else
|
||||
"$@" || exitcode $?
|
||||
fi
|
||||
test $exitcode = $expected_exitcode || exit 1
|
||||
}
|
||||
|
||||
# Turn on shell traces when VERBOSE=x.
|
||||
if test "x$VERBOSE" = xx; then
|
||||
|
|
|
|||
|
|
@ -25,42 +25,33 @@
|
|||
|
||||
. ./defs || exit 1
|
||||
|
||||
check()
|
||||
{
|
||||
./equals "$2" "$3"
|
||||
test $? != $1 && exit 1;
|
||||
}
|
||||
|
||||
# A few things which are equal
|
||||
check 0 'a' 'a'
|
||||
check 0 '1' '1'
|
||||
check 0 '0' '0'
|
||||
check 0 'a => b' 'a => b'
|
||||
check 0 'G a ' ' G a'
|
||||
check 0 'a U b' 'a U b'
|
||||
check 0 'a & b' 'a & b'
|
||||
check 0 'a & b' 'b & a'
|
||||
check 0 'a & b & c' 'c & a && b'
|
||||
check 0 'a & b & c' 'b & c & a'
|
||||
check 0 'a && b & a' 'b & a & b'
|
||||
check 0 'a & b' 'b & a & b'
|
||||
check 0 'a & b' 'b & a & a'
|
||||
check 0 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
check 0 'a & a' 'a'
|
||||
run 0 ./equals 'a' 'a'
|
||||
run 0 ./equals '1' '1'
|
||||
run 0 ./equals '0' '0'
|
||||
run 0 ./equals 'a => b' 'a => b'
|
||||
run 0 ./equals 'G a ' ' G a'
|
||||
run 0 ./equals 'a U b' 'a U b'
|
||||
run 0 ./equals 'a & b' 'a & b'
|
||||
run 0 ./equals 'a & b' 'b & a'
|
||||
run 0 ./equals 'a & b & c' 'c & a && b'
|
||||
run 0 ./equals 'a & b & c' 'b & c & a'
|
||||
run 0 ./equals 'a && b & a' 'b & a & b'
|
||||
run 0 ./equals 'a & b' 'b & a & b'
|
||||
run 0 ./equals 'a & b' 'b & a & a'
|
||||
run 0 ./equals 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./equals 'a & a' 'a'
|
||||
|
||||
# other formulae which are not
|
||||
check 1 'a' 'b'
|
||||
check 1 '1' '0'
|
||||
check 1 'a => b' 'b => a'
|
||||
check 1 'a => b' 'a <=> b'
|
||||
check 1 'a => b' 'a U b'
|
||||
check 1 'a R b' 'a U b'
|
||||
check 1 'a & b & c' 'c & a'
|
||||
check 1 'b & c' 'c & a & b'
|
||||
check 1 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
run 1 ./equals 'a' 'b'
|
||||
run 1 ./equals '1' '0'
|
||||
run 1 ./equals 'a => b' 'b => a'
|
||||
run 1 ./equals 'a => b' 'a <=> b'
|
||||
run 1 ./equals 'a => b' 'a U b'
|
||||
run 1 ./equals 'a R b' 'a U b'
|
||||
run 1 ./equals 'a & b & c' 'c & a'
|
||||
run 1 ./equals 'b & c' 'c & a & b'
|
||||
run 1 ./equals 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
|
||||
# Precedence
|
||||
check 0 'a & b ^ c | d' 'd | c ^ b & a'
|
||||
|
||||
# Success.
|
||||
:
|
||||
run 0 ./equals 'a & b ^ c | d' 'd | c ^ b & a'
|
||||
|
|
|
|||
|
|
@ -28,22 +28,22 @@
|
|||
set -e
|
||||
|
||||
# A few things that do not change
|
||||
./lunabbrev 'a' 'a'
|
||||
./lunabbrev '1' '1'
|
||||
./lunabbrev '0' '0'
|
||||
./lunabbrev 'G a ' ' G a'
|
||||
./lunabbrev 'a U b' 'a U b'
|
||||
./lunabbrev 'a & b' 'a & b'
|
||||
./lunabbrev 'a & b' 'b & a'
|
||||
./lunabbrev 'a & b & c' 'c & a & b'
|
||||
./lunabbrev 'a & b & c' 'b & c & a'
|
||||
./lunabbrev 'a & b & a' 'b & a & b'
|
||||
./lunabbrev 'a & b' 'b & a & b'
|
||||
./lunabbrev 'a & b' 'b & a & a'
|
||||
./lunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./lunabbrev 'a' 'a'
|
||||
run 0 ./lunabbrev '1' '1'
|
||||
run 0 ./lunabbrev '0' '0'
|
||||
run 0 ./lunabbrev 'G a ' ' G a'
|
||||
run 0 ./lunabbrev 'a U b' 'a U b'
|
||||
run 0 ./lunabbrev 'a & b' 'a & b'
|
||||
run 0 ./lunabbrev 'a & b' 'b & a'
|
||||
run 0 ./lunabbrev 'a & b & c' 'c & a & b'
|
||||
run 0 ./lunabbrev 'a & b & c' 'b & c & a'
|
||||
run 0 ./lunabbrev 'a & b & a' 'b & a & b'
|
||||
run 0 ./lunabbrev 'a & b' 'b & a & b'
|
||||
run 0 ./lunabbrev 'a & b' 'b & a & a'
|
||||
run 0 ./lunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
# other formulae that do change
|
||||
./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
|
||||
./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
./lunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
run 0 ./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
run 0 ./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
run 0 ./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
|
||||
run 0 ./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
run 0 ./lunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
|
|
|
|||
|
|
@ -28,37 +28,37 @@
|
|||
set -e
|
||||
|
||||
# A few things that do not change
|
||||
./nenoform 'a' 'a'
|
||||
./nenoform '1' '1'
|
||||
./nenoform '0' '0'
|
||||
./nenoform '!a' '!a'
|
||||
./nenoform 'a U b' 'a U b'
|
||||
./nenoform 'a & b' 'a & b'
|
||||
./nenoform 'a & b' 'b & a'
|
||||
./nenoform 'a & !b & c' 'c & a & !b'
|
||||
./nenoform 'a & b & c' 'b & c & a'
|
||||
./nenoform 'Xa & b & Xa' 'b & Xa & b'
|
||||
./nenoform 'a & b' 'b & a & b'
|
||||
./nenoform 'a & !b' '!b & a & a'
|
||||
./nenoform 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
|
||||
./nenoform 'GFa => FGb' 'GFa => FGb'
|
||||
run 0 ./nenoform 'a' 'a'
|
||||
run 0 ./nenoform '1' '1'
|
||||
run 0 ./nenoform '0' '0'
|
||||
run 0 ./nenoform '!a' '!a'
|
||||
run 0 ./nenoform 'a U b' 'a U b'
|
||||
run 0 ./nenoform 'a & b' 'a & b'
|
||||
run 0 ./nenoform 'a & b' 'b & a'
|
||||
run 0 ./nenoform 'a & !b & c' 'c & a & !b'
|
||||
run 0 ./nenoform 'a & b & c' 'b & c & a'
|
||||
run 0 ./nenoform 'Xa & b & Xa' 'b & Xa & b'
|
||||
run 0 ./nenoform 'a & b' 'b & a & b'
|
||||
run 0 ./nenoform 'a & !b' '!b & a & a'
|
||||
run 0 ./nenoform 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
|
||||
run 0 ./nenoform 'GFa => FGb' 'GFa => FGb'
|
||||
|
||||
# Basic rewritings
|
||||
./nenoform '!!a' 'a'
|
||||
./nenoform '!!!!!a' '!a'
|
||||
./nenoform '!Xa' 'X!a'
|
||||
./nenoform '!Fa' 'G!a'
|
||||
./nenoform '!Ga' 'F!a'
|
||||
./nenoform '!(a ^ b)' 'a <=> b'
|
||||
./nenoform '!(a <=> b)' '(((a) ^ (b)))'
|
||||
./nenoform '!(a => b)' 'a&!b'
|
||||
./nenoform '!(!a => !b)' '!a&b'
|
||||
./nenoform '!(a U b)' '!a R !b'
|
||||
./nenoform '!(a R b)' '!a U !b'
|
||||
./nenoform '!(!a R !b)' 'a U b'
|
||||
./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
|
||||
./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
|
||||
run 0 ./nenoform '!!a' 'a'
|
||||
run 0 ./nenoform '!!!!!a' '!a'
|
||||
run 0 ./nenoform '!Xa' 'X!a'
|
||||
run 0 ./nenoform '!Fa' 'G!a'
|
||||
run 0 ./nenoform '!Ga' 'F!a'
|
||||
run 0 ./nenoform '!(a ^ b)' 'a <=> b'
|
||||
run 0 ./nenoform '!(a <=> b)' '(((a) ^ (b)))'
|
||||
run 0 ./nenoform '!(a => b)' 'a&!b'
|
||||
run 0 ./nenoform '!(!a => !b)' '!a&b'
|
||||
run 0 ./nenoform '!(a U b)' '!a R !b'
|
||||
run 0 ./nenoform '!(a R b)' '!a U !b'
|
||||
run 0 ./nenoform '!(!a R !b)' 'a U b'
|
||||
run 0 ./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
|
||||
run 0 ./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
|
||||
|
||||
# Nested rewritings
|
||||
./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
|
||||
./nenoform '!(GF a => FG b)' 'GFa & GF!b'
|
||||
run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
|
||||
run 0 ./nenoform '!(GF a => FG b)' 'GFa & GF!b'
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ do
|
|||
fi
|
||||
|
||||
if test -n "$DOT"; then
|
||||
./ltl2dot "$f" > parse.dot
|
||||
run 0 ./ltl2dot "$f" > parse.dot
|
||||
if $DOT -o /dev/null parse.dot; then
|
||||
rm -f parse.dot
|
||||
else
|
||||
|
|
|
|||
|
|
@ -28,26 +28,21 @@
|
|||
|
||||
check()
|
||||
{
|
||||
if ./ltl2text "$1" >stdout; then
|
||||
echo "ltl2text unexpectedly parsed '$1' successfully"
|
||||
rm -f stdout
|
||||
exit 1
|
||||
run 1 ./ltl2text "$1" >stdout
|
||||
if test -n "$2"; then
|
||||
echo "$2" >expect
|
||||
else
|
||||
if test -n "$2"; then
|
||||
echo "$2" >expect
|
||||
else
|
||||
: >expect
|
||||
fi
|
||||
if cmp stdout expect; then
|
||||
:
|
||||
else
|
||||
echo "'$1' parsed as"
|
||||
cat stdout
|
||||
echo "instead of"
|
||||
cat expect
|
||||
rm -f stdout expect
|
||||
exit 1
|
||||
fi
|
||||
: >expect
|
||||
fi
|
||||
if cmp stdout expect; then
|
||||
:
|
||||
else
|
||||
echo "'$1' parsed as"
|
||||
cat stdout
|
||||
echo "instead of"
|
||||
cat expect
|
||||
rm -f stdout expect
|
||||
exit 1
|
||||
fi
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -27,19 +27,18 @@
|
|||
|
||||
set -e
|
||||
|
||||
./tostring 'a'
|
||||
./tostring '1'
|
||||
./tostring '0'
|
||||
./tostring 'a => b'
|
||||
./tostring 'G a '
|
||||
./tostring 'a U b'
|
||||
./tostring 'a & b'
|
||||
./tostring 'a & b & c'
|
||||
./tostring 'b & a & b'
|
||||
./tostring 'b & a & a'
|
||||
./tostring 'a & b & (c |(f U g)| e)'
|
||||
./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
./tostring 'a <=> b'
|
||||
./tostring 'a & b & (c |(f U g)| e)'
|
||||
./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
|
||||
run 0 ./tostring 'a'
|
||||
run 0 ./tostring '1'
|
||||
run 0 ./tostring '0'
|
||||
run 0 ./tostring 'a => b'
|
||||
run 0 ./tostring 'G a '
|
||||
run 0 ./tostring 'a U b'
|
||||
run 0 ./tostring 'a & b'
|
||||
run 0 ./tostring 'a & b & c'
|
||||
run 0 ./tostring 'b & a & b'
|
||||
run 0 ./tostring 'b & a & a'
|
||||
run 0 ./tostring 'a & b & (c |(f U g)| e)'
|
||||
run 0 ./tostring 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./tostring 'a <=> b'
|
||||
run 0 ./tostring 'a & b & (c |(f U g)| e)'
|
||||
run 0 ./tostring 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
|
|
|
|||
|
|
@ -28,27 +28,27 @@
|
|||
set -e
|
||||
|
||||
# A few things that do not change
|
||||
./tunabbrev 'a' 'a'
|
||||
./tunabbrev '1' '1'
|
||||
./tunabbrev '0' '0'
|
||||
./tunabbrev 'a U b' 'a U b'
|
||||
./tunabbrev 'a & b' 'a & b'
|
||||
./tunabbrev 'a & b' 'b & a'
|
||||
./tunabbrev 'a & b & c' 'c & a & b'
|
||||
./tunabbrev 'a & b & c' 'b & c & a'
|
||||
./tunabbrev 'a & b & a' 'b & a & b'
|
||||
./tunabbrev 'a & b' 'b & a & b'
|
||||
./tunabbrev 'a & b' 'b & a & a'
|
||||
./tunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./tunabbrev 'a' 'a'
|
||||
run 0 ./tunabbrev '1' '1'
|
||||
run 0 ./tunabbrev '0' '0'
|
||||
run 0 ./tunabbrev 'a U b' 'a U b'
|
||||
run 0 ./tunabbrev 'a & b' 'a & b'
|
||||
run 0 ./tunabbrev 'a & b' 'b & a'
|
||||
run 0 ./tunabbrev 'a & b & c' 'c & a & b'
|
||||
run 0 ./tunabbrev 'a & b & c' 'b & c & a'
|
||||
run 0 ./tunabbrev 'a & b & a' 'b & a & b'
|
||||
run 0 ./tunabbrev 'a & b' 'b & a & b'
|
||||
run 0 ./tunabbrev 'a & b' 'b & a & a'
|
||||
run 0 ./tunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
|
||||
# same as in lunabbrev.test:
|
||||
./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
./tunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
run 0 ./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
run 0 ./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
run 0 ./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
run 0 ./tunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
|
||||
# LTL unabbreviations:
|
||||
./tunabbrev 'G a ' 'false R a'
|
||||
./tunabbrev 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
|
||||
./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
|
||||
./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
|
||||
run 0 ./tunabbrev 'G a ' 'false R a'
|
||||
run 0 ./tunabbrev 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
|
||||
run 0 ./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
|
||||
run 0 ./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
|
||||
|
|
|
|||
|
|
@ -27,10 +27,10 @@
|
|||
|
||||
set -e
|
||||
|
||||
./tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
|
||||
./tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
|
||||
./tunenoform '!(a => b)' 'a&!b'
|
||||
./tunenoform '!(!a => !b)' '!a&b'
|
||||
./tunenoform '!Fa' 'false R !a'
|
||||
./tunenoform '!G!a' 'true U a'
|
||||
./tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
|
||||
run 0 ./tunenoform '!(a ^ b)' '(a|!b) & (!a|b)'
|
||||
run 0 ./tunenoform '!(a <=> b)' '(a|b) & (!a|!b)'
|
||||
run 0 ./tunenoform '!(a => b)' 'a&!b'
|
||||
run 0 ./tunenoform '!(!a => !b)' '!a&b'
|
||||
run 0 ./tunenoform '!Fa' 'false R !a'
|
||||
run 0 ./tunenoform '!G!a' 'true U a'
|
||||
run 0 ./tunenoform '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue