diff --git a/ChangeLog b/ChangeLog index 566a7e56c..8b82580a8 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2003-04-29 Alexandre DURET-LUTZ + * src/ltltest/tostring.test: Simplify with set -e. Move the + description of the test ... + * src/ltltest/tostring.cc: ... here, where it is actually coded. + * src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test, + src/ltltest/nenoform.test, src/ltltest/tunenoform.test: + Simplify with set -e. + * configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make sure we always use paths relative to src/ in src/'s subdirectories. diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test index 386dfd165..0f1a5fde8 100755 --- a/src/ltltest/lunabbrev.test +++ b/src/ltltest/lunabbrev.test @@ -4,32 +4,25 @@ . ./defs || exit 1 -check() -{ - ./lunabbrev "$1" "$2" || exit 1 -} +set -e # A few things that do not change -check 'a' 'a' -check '1' '1' -check '0' '0' -check 'G a ' ' G a' -check 'a U b' 'a U b' -check 'a & b' 'a & b' -check 'a & b' 'b & a' -check 'a & b & c' 'c & a & b' -check 'a & b & c' 'b & c & a' -check 'a & b & a' 'b & a & b' -check 'a & b' 'b & a & b' -check 'a & b' 'b & a & a' -check 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b' - +./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' # other formulae that do change -check 'a ^ b' '(a & !b) | (!a & b)' -check 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)' -check 'GF a => F G(b)' '!GFa | F Gb' -check '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)' -check '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)' - -# Success. -: \ No newline at end of file +./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)' diff --git a/src/ltltest/nenoform.test b/src/ltltest/nenoform.test index 91cf388d6..224500b3c 100755 --- a/src/ltltest/nenoform.test +++ b/src/ltltest/nenoform.test @@ -4,46 +4,40 @@ . ./defs || exit 1 -check() -{ - ./nenoform "$1" "$2" || exit 1 -} +set -e # A few things that do not change -check 'a' 'a' -check '1' '1' -check '0' '0' -check '!a' '!a' -check 'a U b' 'a U b' -check 'a & b' 'a & b' -check 'a & b' 'b & a' -check 'a & !b & c' 'c & a & !b' -check 'a & b & c' 'b & c & a' -check 'Xa & b & Xa' 'b & Xa & b' -check 'a & b' 'b & a & b' -check 'a & !b' '!b & a & a' -check 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b' -check 'GFa => FGb' 'GFa => FGb' +./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' # Basic rewritings -check '!!a' 'a' -check '!!!!!a' '!a' -check '!Xa' 'X!a' -check '!Fa' 'G!a' -check '!Ga' 'F!a' -check '!(a ^ b)' 'a <=> b' -check '!(a <=> b)' '(((a) ^ (b)))' -check '!(a => b)' 'a&!b' -check '!(!a => !b)' '!a&b' -check '!(a U b)' '!a R !b' -check '!(a R b)' '!a U !b' -check '!(!a R !b)' 'a U b' -check '!(a & b & c & d & b)' '!a | !b | !c | !d' -check '!(a | b | c | d)' '!a & !b & !c & !d' +./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' # Nested rewritings -check '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))' -check '!(GF a => FG b)' 'GFa & GF!b' - -# Success. -: \ No newline at end of file +./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' diff --git a/src/ltltest/tostring.cc b/src/ltltest/tostring.cc index 66cb29a1d..3a2bb9217 100644 --- a/src/ltltest/tostring.cc +++ b/src/ltltest/tostring.cc @@ -16,13 +16,16 @@ main(int argc, char **argv) { if (argc != 2) syntax(argv[0]); - + spot::ltl::parse_error_list p1; spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; + // The string generated from an abstract tree should be parsable + // again. + std::ostringstream os; spot::ltl::to_string(*f1, os); std::cout << os.str() << std::endl; @@ -32,14 +35,18 @@ main(int argc, char **argv) if (spot::ltl::format_parse_errors(std::cerr, os.str(), p1)) return 2; + // This second abstract tree should be equal to the first. + + if (! equals(f1, f2)) + return 1; + + // It should also map to the same string. + std::ostringstream os2; spot::ltl::to_string(*f2, os2); std::cout << os2.str() << std::endl; if (os2.str() != os.str()) return 1; - - if (! equals(f1, f2)) - return 1; } diff --git a/src/ltltest/tostring.test b/src/ltltest/tostring.test index 04c7a3015..9579b63a5 100755 --- a/src/ltltest/tostring.test +++ b/src/ltltest/tostring.test @@ -1,28 +1,24 @@ #! /bin/sh -# Check that spot::ltl::tostring is correct: after to parse we get the -# string of the abstract syntax tree and xe parse it again to apply spot::ltl::tostring one more times. +# Check for spot::ltl::tostring. . ./defs || exit 1 -check() -{ - ./tostring "$1" || exit 1 -} +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' -check 'a' -check '1' -check '0' -check 'a => b' -check 'G a ' -check 'a U b' -check 'a & b' -check 'a & b & c' -check 'b & a & b' -check 'b & a & a' -check 'a & b & (c |(f U g)| e)' -check 'b & a & a & (c | e |(f U g)| e | c) & b' -check 'a <=> b' -check 'a & b & (c |(f U g)| e)' -check 'b & a & a & (c | e |(g U g)| e | c) & b' -: diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test index 80ae8c56b..2321f9ddd 100755 --- a/src/ltltest/tunabbrev.test +++ b/src/ltltest/tunabbrev.test @@ -4,36 +4,30 @@ . ./defs || exit 1 -check() -{ - ./tunabbrev "$1" "$2" || exit 1 -} +set -e # A few things that do not change -check 'a' 'a' -check '1' '1' -check '0' '0' -check 'a U b' 'a U b' -check 'a & b' 'a & b' -check 'a & b' 'b & a' -check 'a & b & c' 'c & a & b' -check 'a & b & c' 'b & c & a' -check 'a & b & a' 'b & a & b' -check 'a & b' 'b & a & b' -check 'a & b' 'b & a & a' -check 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b' +./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' # same as in lunabbrev.test: -check 'a ^ b' '(a & !b) | (!a & b)' -check 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)' -check '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)' -check '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)' +./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)' # LTL unabbreviations: -check 'G a ' 'false R a' -check 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))' -check 'GGGGa' 'false V (false V (false V (false V a)))' -check 'FFFfalse' 'true U ((true) U (true U (false)))' - -# Success. -: \ No newline at end of file +./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)))' diff --git a/src/ltltest/tunenoform.test b/src/ltltest/tunenoform.test index 0eba7111e..c131800b9 100755 --- a/src/ltltest/tunenoform.test +++ b/src/ltltest/tunenoform.test @@ -4,18 +4,12 @@ . ./defs || exit 1 -check() -{ - ./tunenoform "$1" "$2" || exit 1 -} +set -e -check '!(a ^ b)' '(a|!b) & (!a|b)' -check '!(a <=> b)' '(a|b) & (!a|!b)' -check '!(a => b)' 'a&!b' -check '!(!a => !b)' '!a&b' -check '!Fa' 'false R !a' -check '!G!a' 'true U a' -check '!(GF a => FG b)' '(0 R (1 U a)) & (0 R (1 U !b))' - -# Success. -: \ No newline at end of file +./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))'