diff --git a/ChangeLog b/ChangeLog index b021d02b3..da4a9fbc1 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,15 @@ +2004-05-10 Alexandre Duret-Lutz + + * src/sanity/80columns.test: New file. + * src/sanity/Makefile.am (check-local): Run it. + * src/ltltest/equals.test, src/ltltest/lunabbrev.test, + src/ltltest/nenoform.test, src/ltltest/parseerr.test + src/ltltest/tunabbrev.test, src/ltltest/reduc.cc, + src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc, + src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, + src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test, + src/tgbatest/tripprod.test: Wrap long lines. + 2004-05-10 Thomas MARTINEZ * src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula. diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test index ceb700e34..858bb60fe 100755 --- a/src/ltltest/equals.test +++ b/src/ltltest/equals.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -39,7 +39,8 @@ 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 & 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 @@ -51,7 +52,8 @@ 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' +run 1 ./equals 'a & b & (c |(f U g)| e)' \ + 'b & a & a & (c | e |(g U g)| e | c) & b' # Precedence run 0 ./equals 'a & b ^ c | d' 'd | c ^ b & a' diff --git a/src/ltltest/lunabbrev.test b/src/ltltest/lunabbrev.test index e22a4e8c1..aec793646 100755 --- a/src/ltltest/lunabbrev.test +++ b/src/ltltest/lunabbrev.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -40,10 +40,12 @@ 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' +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 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)' +run 0 ./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 ee105adb7..bfb833580 100755 --- a/src/ltltest/nenoform.test +++ b/src/ltltest/nenoform.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -40,7 +40,8 @@ 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 '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 @@ -60,5 +61,6 @@ 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 -run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))' +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' diff --git a/src/ltltest/parseerr.test b/src/ltltest/parseerr.test index 4a0144701..721b37da2 100755 --- a/src/ltltest/parseerr.test +++ b/src/ltltest/parseerr.test @@ -56,7 +56,8 @@ check 'a U b c' 'binop(U, AP(a), AP(b))' check 'a &&& b' 'multop(And, constant(0), AP(b))' # (check multop merging while we are at it) check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))' -check 'a & (b | c) & d should work' 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))' +check 'a & (b | c) & d should work' \ + 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))' # Binop recovery check 'a U' 'constant(0)' diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc index 533de2846..656afc2a9 100644 --- a/src/ltltest/reduc.cc +++ b/src/ltltest/reduc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -45,7 +45,7 @@ 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); spot::ltl::formula* f2 = NULL; @@ -53,37 +53,37 @@ main(int argc, char** argv) if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) return 2; - + if (argc == 3){ spot::ltl::parse_error_list p2; f2 = spot::ltl::parse(argv[2], p2); if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) return 2; } - + int exit_code = 0; - + spot::ltl::formula* ftmp1; spot::ltl::formula* ftmp2; - + ftmp1 = f1; f1 = unabbreviate_logic(f1); ftmp2 = f1; f1 = negative_normal_form(f1); spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); - - + + int length_f1_before = spot::ltl::form_length(f1); std::string f1s_before = spot::ltl::to_string(f1); - + ftmp1 = f1; f1 = spot::ltl::reduce(f1); ftmp2 = f1; f1 = spot::ltl::unabbreviate_logic(f1); spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); - + int length_f1_after = spot::ltl::form_length(f1); std::string f1s_after = spot::ltl::to_string(f1); @@ -102,49 +102,54 @@ main(int argc, char** argv) spot::ltl::destroy(ftmp1); f2s = spot::ltl::to_string(f2); } - - + + if (red && (f2 == NULL)) { - std::cout << length_f1_before << " " << length_f1_after - << " '" << f1s_before << "' reduce to '" << f1s_after << "'" << std::endl; + std::cout << length_f1_before << " " << length_f1_after + << " '" << f1s_before << "' reduce to '" << f1s_after << "'" + << std::endl; } - + if (f2 != NULL){ if (f1 != f2) { if (length_f1_after < length_f1_before) - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOREDUC " << std::endl; + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " KOREDUC " << std::endl; else - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOIDEM " << std::endl; + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " KOIDEM " << std::endl; exit_code = 1; } else { if (f1s_before != f1s_after) - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKREDUC " << std::endl; + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " OKREDUC " << std::endl; else - std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKIDEM" << std::endl; + std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after + << " OKIDEM" << std::endl; exit_code = 0; } } - else{ + else{ if (length_f1_after < length_f1_before) exit_code = 0; } - + /* spot::ltl::dump(std::cout, f1); std::cout << std::endl; if (f2 != NULL) spot::ltl::dump(std::cout, f2); std::cout << std::endl; */ - - + + spot::ltl::destroy(f1); if (f2 != NULL) spot::ltl::destroy(f2); - + assert(spot::ltl::atomic_prop::instance_count() == 0); assert(spot::ltl::unop::instance_count() == 0); assert(spot::ltl::binop::instance_count() == 0); assert(spot::ltl::multop::instance_count() == 0); - + return exit_code; } diff --git a/src/ltltest/tunabbrev.test b/src/ltltest/tunabbrev.test index 5637d8945..57b3aa448 100755 --- a/src/ltltest/tunabbrev.test +++ b/src/ltltest/tunabbrev.test @@ -1,5 +1,5 @@ #! /bin/sh -# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre # et Marie Curie. # @@ -39,16 +39,19 @@ 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' +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: 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)' +run 0 ./tunabbrev '(a ^ b) | (b ^ c)' \ + '(c & !b) | (!c & b) | (a & !b) | (!a & b)' # LTL unabbreviations: 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 '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)))' diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/forminf.cc index 24904d862..88e1c6735 100644 --- a/src/ltlvisit/forminf.cc +++ b/src/ltlvisit/forminf.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -42,7 +42,7 @@ namespace spot return true; return false; } - + bool is_FG(const formula* f) { @@ -58,47 +58,47 @@ namespace spot nb_term_multop(const formula* f) { if ((const multop*)f == NULL) return -1; - + unsigned mos = ((const multop*)(f))->size(); return mos; } - + node_type_form_visitor::node_type_form_visitor(){} - + node_type_form_visitor::type node_type_form_visitor::result() const { return result_;} - + void - node_type_form_visitor::visit(const atomic_prop* ap){ + node_type_form_visitor::visit(const atomic_prop* ap){ if (ap == NULL); result_ = node_type_form_visitor::Atom; } - + void - node_type_form_visitor::visit(const constant* c){ + node_type_form_visitor::visit(const constant* c){ if (c == NULL); result_ = node_type_form_visitor::Const; } - + void node_type_form_visitor::visit(const unop* uo){ - if (uo == NULL); + if (uo == NULL); result_ = node_type_form_visitor::Unop; } - + void - node_type_form_visitor::visit(const binop* bo){ + node_type_form_visitor::visit(const binop* bo){ if (bo == NULL); result_ = node_type_form_visitor::Binop; } - + void - node_type_form_visitor::visit(const multop* mo){ + node_type_form_visitor::visit(const multop* mo){ if (mo == NULL); result_ = node_type_form_visitor::Multop; } - + node_type_form_visitor::type node_type(const formula* f) { node_type_form_visitor v; @@ -110,41 +110,41 @@ namespace spot class form_eventual_universal_visitor : public const_visitor { public: - + form_eventual_universal_visitor() { eventual = false; // faux au départ universal = false; } - + virtual ~form_eventual_universal_visitor() { } - bool + bool is_eventual() const { return eventual; } - - bool + + bool is_universal() const { return universal; } - + void visit(const atomic_prop* ap) { if (ap); } - + void visit(const constant* c) { if (c->val()); } - + void visit(const unop* uo) { @@ -156,7 +156,7 @@ namespace spot eventual = recurse_ev(f1); universal = recurse_un(f1); return; - case unop::F: + case unop::F: eventual = true; return; case unop::G: @@ -166,7 +166,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const binop* bo) { @@ -191,13 +191,13 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const multop* mo) { if (mo == NULL); unsigned mos = mo->size(); - + eventual = true; universal = true; for (unsigned i = 0; i < mos; ++i){ @@ -213,7 +213,7 @@ namespace spot } } } - + bool recurse_ev(const formula* f) { @@ -235,7 +235,7 @@ namespace spot bool universal; }; - + bool is_eventual(const formula* f) { form_eventual_universal_visitor v; @@ -249,19 +249,19 @@ namespace spot const_cast(f)->accept(v); return v.is_universal(); } - + ///////////////////////////////////////////////////////////////////////// class inf_form_right_recurse_visitor : public const_visitor { public: - + inf_form_right_recurse_visitor(const formula *f) { this->f = f; result_ = false; // faux au départ } - + virtual ~inf_form_right_recurse_visitor() { } @@ -278,19 +278,19 @@ namespace spot return false; } */ - int + int result() const { return result_; } - + void visit(const atomic_prop* ap) { - if ((const atomic_prop*)f == ap) + if ((const atomic_prop*)f == ap) result_ = true; } - + void visit(const constant* c) { @@ -304,7 +304,7 @@ namespace spot return; } } - + void visit(const unop* uo) { @@ -316,7 +316,7 @@ namespace spot return; case unop::X:// à gérer !! return; - case unop::F: + case unop::F: // F(a) = true U a result_ = inf_form(f,f1); return; @@ -331,7 +331,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const binop* bo) { @@ -355,7 +355,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const multop* mo) { @@ -377,7 +377,7 @@ namespace spot break; } } - + bool recurse(const formula* f1, const formula* f2) { @@ -397,34 +397,35 @@ namespace spot class inf_form_left_recurse_visitor : public const_visitor { public: - + inf_form_left_recurse_visitor(const formula *f) { this->f = f; result_ = false; } - + virtual ~inf_form_left_recurse_visitor() { } bool special_case(const formula* f2) { - if ((node_type(f) == node_type_form_visitor::Binop) + if ((node_type(f) == node_type_form_visitor::Binop) && (node_type(f2) == node_type_form_visitor::Binop)) if (((const binop*)f)->op() == ((const binop*)f2)->op()) if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first()) - && inf_form(((const binop*)f2)->second(),((const binop*)f)->second()) ) + && inf_form(((const binop*)f2)->second(), + ((const binop*)f)->second())) return true; return false; } - int + int result() const { return result_; } - + void visit(const atomic_prop* ap) { @@ -432,7 +433,7 @@ namespace spot const_cast(f)->accept(v); result_ = v.result(); } - + void visit(const constant* c) { @@ -450,7 +451,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const unop* uo) { @@ -469,7 +470,7 @@ namespace spot result_ = inf_form(f1,((const unop*)f)->child()); } return; - case unop::F: + case unop::F: // F(a) = true U a tmp = binop::instance(binop::U,constant::true_instance(),clone(f1)); if (this->special_case(tmp)){ @@ -483,7 +484,8 @@ namespace spot return; case unop::G: // F(a) = false R a - tmp = binop::instance(binop::R,constant::false_instance(),clone(f1)); + tmp = binop::instance(binop::R, + constant::false_instance(), clone(f1)); if (this->special_case(tmp)){ result_ = true; spot::ltl::destroy(tmp); @@ -497,17 +499,17 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const binop* bo) { - + if (this->special_case(bo)) { result_ = true; return; } - + const formula* f1 = bo->first(); const formula* f2 = bo->second(); switch (bo->op()) @@ -520,7 +522,7 @@ namespace spot if ( (inf_form(f1,f)) && (inf_form(f2,f)) ) result_ = true; return; - case binop::R: + case binop::R: if ( (inf_form(f2,f)) ) result_ = true; return; @@ -528,7 +530,7 @@ namespace spot /* Unreachable code. */ assert(0); } - + void visit(const multop* mo) { @@ -550,7 +552,7 @@ namespace spot break; } } - + protected: bool result_; // true if f1 < f, 1 otherwise. const formula* f; @@ -558,19 +560,19 @@ namespace spot bool inf_form(const formula* f1, const formula* f2) { - // f1 and f2 are unabbreviate + // f1 and f2 are unabbreviate if (f1 == f2) return true; inf_form_left_recurse_visitor v1(f2); inf_form_right_recurse_visitor v2(f1); - - if ( (node_type(f1) == node_type_form_visitor::Const) && + + if ( (node_type(f1) == node_type_form_visitor::Const) && (node_type(f2) == node_type_form_visitor::Const) ) if ( (((const constant*)f2)->val() == constant::True) || (((const constant*)f1)->val() == constant::False) ) { return true; } - + const_cast(f1)->accept(v1); if (v1.result()) { return true; @@ -580,38 +582,39 @@ namespace spot if (v2.result()) { return true; } - + return false; } - + bool infneg_form(const formula* f1, const formula* f2, int n) { const formula* ftmp1; const formula* ftmp2; - const formula* ftmp3 = unop::instance(unop::Not,(n == 0)? clone(f1) : clone(f2)); + const formula* ftmp3 = unop::instance(unop::Not, + (n == 0)? clone(f1) : clone(f2)); const formula* ftmp4 = spot::ltl::negative_normal_form((n == 0)? f2 : f1); const formula* ftmp5; const formula* ftmp6; bool retour; - + ftmp2 = spot::ltl::unabbreviate_logic(ftmp3); ftmp1 = spot::ltl::negative_normal_form(ftmp2); - + ftmp5 = spot::ltl::unabbreviate_logic(ftmp4); ftmp6 = spot::ltl::negative_normal_form(ftmp5); - + if (n == 0) retour = inf_form(ftmp1, ftmp6); - else + else retour = inf_form(ftmp6, ftmp1); - + spot::ltl::destroy(ftmp1); spot::ltl::destroy(ftmp2); spot::ltl::destroy(ftmp3); spot::ltl::destroy(ftmp4); spot::ltl::destroy(ftmp5); spot::ltl::destroy(ftmp6); - + return retour; } diff --git a/src/sanity/80columns.test b/src/sanity/80columns.test new file mode 100755 index 000000000..ad373ae1a --- /dev/null +++ b/src/sanity/80columns.test @@ -0,0 +1,28 @@ +#! /bin/sh + +# Check that all files use at most 80 columns. + +set -e + +rm -f failures + +find "${INCDIR-..}" \( -name "${1-*}.hh" -o -name "${1-*}.cc" \ + -o -name "${1-*}.test" \) -a -type f -a -print | +while read file; do + x='.........................................' + if grep -q $x$x "$file"; then + if grep 'GNU Bison' "$file" >/dev/null || + grep 'generated by flex' "$file" >/dev/null ; then + : + else + echo "$file" >>failures + fi + fi +done + +if test -f failures; then + echo "The following files contain lines with more than 80 characters:" + cat failures + rm failures + exit 1; +fi diff --git a/src/sanity/Makefile.am b/src/sanity/Makefile.am index 49c32f42e..72b5198de 100644 --- a/src/sanity/Makefile.am +++ b/src/sanity/Makefile.am @@ -30,6 +30,8 @@ check-local: CXXFLAGS='$(AM_CXXFLAGS) $(CXXFLAGS)' \ INCDIR='$(top_srcdir)/src' \ $(SHELL) $(srcdir)/includes.test $(TESTHEADER) + INCDIR='$(top_srcdir)/src' \ + $(SHELL) $(srcdir)/80columns.test $(TESTHEADER) # Ensure we have not forgotten to include an header. installcheck-local: diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index c5ae2f6d6..a80ddba75 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -47,7 +47,8 @@ run 0 ./explprod input1 input2 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \ +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g; + s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \ stdout > tmp_ && mv tmp_ stdout cat stdout diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index b2fb69645..2a1ed284b 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -47,7 +47,8 @@ run 0 ./explprod input1 input2 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g;s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout +sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g; + s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout cat stdout diff stdout expected diff --git a/src/tgbatest/explprod.test b/src/tgbatest/explprod.test index 6bb5f4b3d..3f01d5a8c 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -49,7 +49,8 @@ EOF run 0 ./explprod input1 input2 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g; + s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ stdout > tmp_ && mv tmp_ stdout cat stdout diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 81cd3751c..d409a4692 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -185,7 +185,8 @@ Algorithm Algorithm { Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba" - Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'" + Path = + "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'" Enabled = no } diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index f961b61ce..66a6ee1eb 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -61,7 +61,8 @@ run 0 ./tripprod input1 input2 input3 > stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1, $2, $3, $4]}/g;s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1,$2,$3,$4]}/g; + s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \ stdout > tmp_ && mv tmp_ stdout