diff --git a/ChangeLog b/ChangeLog index 012d62321..d2f1ff692 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,40 @@ 2003-11-24 Alexandre Duret-Lutz + Explicit automata can now have arbitrary logic formula on their + arcs. ltl2tgba_fm benefits from this and join multiple arcs with + the same destination and acceptance conditions. + * src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files. + * src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them. + * src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula, + bdd_format_formula): New functions. + * src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition, + tgba_explicit::add_condition, tgba_explicit::add_neg_condition, + tgba_explicit::declare_accepting_condition, + tgba_explicit::has_accepting_condition, + tgba_explicit::get_accepting_condition, + tgba_explicit::add_accepting_condition): Take a const formula*. + * src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition): + Rewrite using formula_to_bdd. + * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use + bdd_print_formula to display conditions. + * src/tgbaalgos/save.cc (save_bfs::process_state): Likewise. + * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula): + New function. + (translate_dict::conj_bdd_to_atomic_props): Remove. + (ltl_to_tgba_fm): Factor successors on accepting conditions + and destinations, not conditions. Use bdd_to_formula to translate + the conditions. + * src/tgbaparse/tgbaparse.yy: Expect conditions as a formula + in a string, call the LTL parser for this. + * src/tgbaparse/tgbascan.ll: Process \" and \\ escapes in + strings. + * src/tgbatest/emptchke.test, src/tgbatest/explicit.test, + src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, + src/tgbatest/explprod.test, src/tgbatest/mixprod.test, + src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, + src/tgbatest/tripprod.test: Adjust to new syntax for explicit + automata. + * src/misc/minato.hh (minato_isop(bdd,bdd)): New constructor variant. (minato_isop::local_vars::vars): New attribute. (minato_isop::local_vars::local_vars): Add the vars arguments. diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 6d9fa91a7..00399081c 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -27,6 +27,7 @@ tgbadir = $(pkgincludedir)/tgba tgba_HEADERS = \ bdddict.hh \ bddprint.hh \ + formula2bdd.hh \ public.hh \ state.hh \ statebdd.hh \ @@ -46,6 +47,7 @@ noinst_LTLIBRARIES = libtgba.la libtgba_la_SOURCES = \ bdddict.cc \ bddprint.cc \ + formula2bdd.cc \ statebdd.cc \ succiterconcrete.cc \ tgba.cc \ diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index a4d15e57a..5de4acd76 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -23,6 +23,8 @@ #include #include "bddprint.hh" #include "ltlvisit/tostring.hh" +#include "formula2bdd.hh" +#include "ltlvisit/destroy.hh" namespace spot { @@ -163,6 +165,23 @@ namespace spot return os.str(); } + std::ostream& + bdd_print_formula(std::ostream& os, const bdd_dict* d, bdd b) + { + const ltl::formula* f = bdd_to_formula(b, d); + to_string(f, os); + destroy(f); + return os; + } + + std::string + bdd_format_formula(const bdd_dict* d, bdd b) + { + std::ostringstream os; + bdd_print_formula(os, d, b); + return os.str(); + } + std::ostream& bdd_print_dot(std::ostream& os, const bdd_dict* d, bdd b) { diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index bb2732a48..a2dcf26a6 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -69,6 +69,18 @@ namespace spot /// \return The BDD formated as a string. std::string bdd_format_set(const bdd_dict* dict, bdd b); + /// \brief Print a BDD as a formula. + /// \param os The output stream. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + std::ostream& bdd_print_formula(std::ostream& os, + const bdd_dict* dict, bdd b); + /// \brief Format a BDD as a formula. + /// \param dict The dictionary to use, to lookup variables. + /// \param b The BDD to print. + /// \return The BDD formated as a string. + std::string bdd_format_formula(const bdd_dict* dict, bdd b); + /// \brief Print a BDD as a diagram in dotty format. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc new file mode 100644 index 000000000..eccbcced2 --- /dev/null +++ b/src/tgba/formula2bdd.cc @@ -0,0 +1,207 @@ +// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#include "formula2bdd.hh" +#include "ltlast/allnodes.hh" +#include "ltlast/visitor.hh" +#include "misc/minato.hh" +#include "ltlvisit/clone.hh" + +namespace spot +{ + using namespace ltl; + + class formula_to_bdd_visitor : public ltl::const_visitor + { + public: + formula_to_bdd_visitor(bdd_dict* d, void* owner) + : d_(d), owner_(owner) + { + } + + virtual + ~formula_to_bdd_visitor() + { + } + + virtual void + visit(const atomic_prop* node) + { + res_ = bdd_ithvar(d_->register_proposition(node, owner_)); + } + + virtual void + visit(const constant* node) + { + switch (node->val()) + { + case constant::True: + res_ = bddtrue; + return; + case constant::False: + res_ = bddfalse; + return; + } + /* Unreachable code. */ + assert(0); + } + + virtual void + visit(const unop* node) + { + switch (node->op()) + { + case unop::F: + case unop::G: + case unop::X: + assert(!"unsupported operator"); + case unop::Not: + { + res_ = bdd_not(recurse(node->child())); + return; + } + } + /* Unreachable code. */ + assert(0); + } + + virtual void + visit(const binop* node) + { + bdd f1 = recurse(node->first()); + bdd f2 = recurse(node->second()); + + switch (node->op()) + { + case binop::Xor: + res_ = bdd_apply(f1, f2, bddop_xor); + return; + case binop::Implies: + res_ = bdd_apply(f1, f2, bddop_imp); + return; + case binop::Equiv: + res_ = bdd_apply(f1, f2, bddop_biimp); + return; + case binop::U: + case binop::R: + assert(!"unsupported operator"); + } + /* Unreachable code. */ + assert(0); + } + + virtual void + visit(const multop* node) + { + int op = -1; + switch (node->op()) + { + case multop::And: + op = bddop_and; + res_ = bddtrue; + break; + case multop::Or: + op = bddop_or; + res_ = bddfalse; + break; + } + assert(op != -1); + unsigned s = node->size(); + for (unsigned n = 0; n < s; ++n) + { + res_ = bdd_apply(res_, recurse(node->nth(n)), op); + } + } + + bdd + result() const + { + return res_; + } + + bdd + recurse(const formula* f) const + { + return formula_to_bdd(f, d_, owner_); + } + + private: + bdd_dict* d_; + void* owner_; + bdd res_; + }; + + bdd + formula_to_bdd(const formula* f, bdd_dict* d, void* for_me) + { + formula_to_bdd_visitor v(d, for_me); + f->accept(v); + return v.result(); + } + + // Convert a BDD which is known to be a conjonction into a formula. + static ltl::formula* + conj_to_formula(bdd b, const bdd_dict* d) + { + if (b == bddfalse) + return constant::false_instance(); + multop::vec* v = new multop::vec; + while (b != bddtrue) + { + int var = bdd_var(b); + bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); + assert(isi != d->var_formula_map.end()); + formula* res = clone(isi->second); + + bdd high = bdd_high(b); + if (high == bddfalse) + { + res = unop::instance(unop::Not, res); + b = bdd_low(b); + } + else + { + // If bdd_low is not false, then b was not a conjunction. + assert(bdd_low(b) == bddfalse); + b = high; + } + assert(b != bddfalse); + v->push_back(res); + } + return multop::instance(multop::And, v); + } + + const formula* + bdd_to_formula(bdd f, const bdd_dict* d) + { + if (f == bddfalse) + return constant::false_instance(); + + multop::vec* v = new multop::vec; + + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v->push_back(conj_to_formula(cube, d)); + + return multop::instance(multop::Or, v); + } +} diff --git a/src/tgba/formula2bdd.hh b/src/tgba/formula2bdd.hh new file mode 100644 index 000000000..fa25cfdab --- /dev/null +++ b/src/tgba/formula2bdd.hh @@ -0,0 +1,41 @@ +// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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. + +#ifndef SPOT_TGBA_FORMULA2BDD_HH +# define SPOT_TGBA_FORMULA2BDD_HH + +# include "bdddict.hh" +# include "ltlast/formula.hh" + +namespace spot +{ + // \brief Convert a formula into a BDD. + // + // Convert formula \a f into a Bdd, using existing variables from \a + // d, and registering new one as necessary. \a for_me is the + // address to use as owner of the variables used in the BDD. + bdd formula_to_bdd(const ltl::formula* f, bdd_dict* d, void* for_me); + + // Convert a BDD into a formula. + const ltl::formula* bdd_to_formula(bdd f, const bdd_dict* d); +} + +#endif // SPOT_TGBA_FORMULA2BDD_HH diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc index e0aeef982..2a85df0e4 100644 --- a/src/tgba/tgbaexplicit.cc +++ b/src/tgba/tgbaexplicit.cc @@ -23,6 +23,7 @@ #include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" #include "tgbaexplicit.hh" +#include "tgba/formula2bdd.hh" #include namespace spot @@ -171,22 +172,23 @@ namespace spot } bdd - tgba_explicit::get_condition(ltl::formula* f) + tgba_explicit::get_condition(const ltl::formula* f) { - assert(dynamic_cast(f)); + assert(dynamic_cast(f)); int v = dict_->register_proposition(f, this); ltl::destroy(f); return bdd_ithvar(v); } void - tgba_explicit::add_condition(transition* t, ltl::formula* f) + tgba_explicit::add_condition(transition* t, const ltl::formula* f) { - t->condition &= get_condition(f); + t->condition &= formula_to_bdd(f, dict_, this); + ltl::destroy(f); } void - tgba_explicit::add_neg_condition(transition* t, ltl::formula* f) + tgba_explicit::add_neg_condition(transition* t, const ltl::formula* f) { t->condition -= get_condition(f); } @@ -199,7 +201,7 @@ namespace spot } void - tgba_explicit::declare_accepting_condition(ltl::formula* f) + tgba_explicit::declare_accepting_condition(const ltl::formula* f) { int v = dict_->register_accepting_variable(f, this); ltl::destroy(f); @@ -234,15 +236,15 @@ namespace spot } bool - tgba_explicit::has_accepting_condition(ltl::formula* f) const + tgba_explicit::has_accepting_condition(const ltl::formula* f) const { return dict_->is_registered_accepting_variable(f, this); } bdd - tgba_explicit::get_accepting_condition(ltl::formula* f) + tgba_explicit::get_accepting_condition(const ltl::formula* f) { - ltl::constant* c = dynamic_cast(f); + const ltl::constant* c = dynamic_cast(f); if (c) { switch (c->val()) @@ -267,7 +269,7 @@ namespace spot } void - tgba_explicit::add_accepting_condition(transition* t, ltl::formula* f) + tgba_explicit::add_accepting_condition(transition* t, const ltl::formula* f) { bdd c = get_accepting_condition(f); t->accepting_conditions |= c; diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index fbc589f03..23e1a17bf 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -55,13 +55,13 @@ namespace spot transition* create_transition(const std::string& source, const std::string& dest); - void add_condition(transition* t, ltl::formula* f); - void add_neg_condition(transition* t, ltl::formula* f); + void add_condition(transition* t, const ltl::formula* f); + void add_neg_condition(transition* t, const ltl::formula* f); /// This assumes that all variables in \a f are known from dict. void add_conditions(transition* t, bdd f); - void declare_accepting_condition(ltl::formula* f); - bool has_accepting_condition(ltl::formula* f) const; - void add_accepting_condition(transition* t, ltl::formula* f); + void declare_accepting_condition(const ltl::formula* f); + bool has_accepting_condition(const ltl::formula* f) const; + void add_accepting_condition(transition* t, const ltl::formula* f); /// This assumes that all accepting conditions in \a f are known from dict. void add_accepting_conditions(transition* t, bdd f); void complement_all_accepting_conditions(); @@ -84,8 +84,8 @@ namespace spot virtual bdd compute_support_variables(const spot::state* state) const; state* add_state(const std::string& name); - bdd get_condition(ltl::formula* f); - bdd get_accepting_condition(ltl::formula* f); + bdd get_condition(const ltl::formula* f); + bdd get_accepting_condition(const ltl::formula* f); typedef Sgi::hash_map ns_map; diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index adcb70447..d2b4c065c 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -60,8 +60,8 @@ namespace spot process_link(int in, int out, const tgba_succ_iterator* si) { os_ << " " << in << " -> " << out << " [label=\""; - bdd_print_set(os_, automata_->get_dict(), - si->current_condition()) << "\\n"; + bdd_print_formula(os_, automata_->get_dict(), + si->current_condition()) << "\\n"; bdd_print_set(os_, automata_->get_dict(), si->current_accepting_conditions()) << "\"]" << std::endl; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index d177dc9da..9b652ce0f 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -208,6 +208,7 @@ namespace spot } else { + assert(bdd_low(b) == bddfalse); b = high; } assert(b != bddfalse); @@ -216,30 +217,21 @@ namespace spot return ltl::multop::instance(ltl::multop::And, v); } - void - conj_bdd_to_atomic_props(tgba_explicit* a, bdd b, - tgba_explicit::transition* t) + const formula* + bdd_to_formula(bdd f) { - assert(b != bddfalse); - while (b != bddtrue) - { - int var = bdd_var(b); - ltl::formula* ap = var_to_formula(var); - bdd high = bdd_high(b); - if (high == bddfalse) - { - a->add_neg_condition(t, ap); - b = bdd_low(b); - } - else - { - a->add_condition(t, ap); - b = high; - } - assert(b != bddfalse); - } - } + if (f == bddfalse) + return ltl::constant::false_instance(); + multop::vec* v = new multop::vec; + + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v->push_back(conj_bdd_to_formula(cube)); + + return multop::instance(multop::Or, v); + } void conj_bdd_to_acc(tgba_explicit* a, bdd b, tgba_explicit::transition* t) @@ -462,7 +454,7 @@ namespace spot std::string now = to_string(f); - minato_isop isop(res); + minato_isop isop(res, d.next_set & d.a_set); bdd cube; while ((cube = isop.next()) != bddfalse) { @@ -473,7 +465,8 @@ namespace spot tgba_explicit::transition* t = a->create_transition(now, next); - d.conj_bdd_to_atomic_props(a, bdd_existcomp(cube, d.var_set), t); + a->add_condition(t, + d.bdd_to_formula(bdd_existcomp(cube, d.var_set))); d.conj_bdd_to_acc(a, bdd_existcomp(cube, d.a_set), t); if (formulae_seen.find(dest) == formulae_seen.end()) diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 81361ad10..f9949b81c 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -77,8 +77,8 @@ namespace spot { state* dest = si->current_state(); os_ << "\"" << cur << "\", \"" - << automata_->format_state(dest) << "\", "; - bdd_print_sat(os_, d, si->current_condition()) << ","; + << automata_->format_state(dest) << "\", \""; + bdd_print_formula(os_, d, si->current_condition()) << "\","; bdd_print_acc(os_, d, si->current_accepting_conditions()); os_ << ";" << std::endl; } diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy index d305eb8ac..3d22c448e 100644 --- a/src/tgbaparse/tgbaparse.yy +++ b/src/tgbaparse/tgbaparse.yy @@ -40,6 +40,7 @@ %{ #include "ltlast/constant.hh" #include "ltlvisit/destroy.hh" +#include "ltlparse/public.hh" /* tgbaparse.hh and parsedecl.hh include each other recursively. We mut ensure that YYSTYPE is declared (by the above %union) @@ -55,9 +56,9 @@ using namespace spot::ltl; typedef std::pair pair; %} -%token STRING +%token STRING UNTERMINATED_STRING %token IDENT -%type strident +%type strident string %type cond_list %type acc_list %token ACC_DEF @@ -92,17 +93,37 @@ line: strident ',' strident ',' cond_list ',' acc_list ';' } ; -strident: STRING | IDENT; +string: STRING + | UNTERMINATED_STRING + { + error_list.push_back(spot::tgba_parse_error(@1, + "unterminated string")); + } + +strident: string | IDENT cond_list: { $$ = new std::list; } - | cond_list strident + | cond_list string§ { if (*$2 != "") { - $1->push_back(pair(false, parse_environment.require(*$2))); + parse_error_list pel; + formula* f = spot::ltl::parse(*$2, pel, parse_environment); + for (parse_error_list::iterator i = pel.begin(); + i != pel.end(); ++i) + { + // Adjust the diagnostic to the current position. + Location here = @2; + here.begin.line += i->first.begin.line; + here.begin.column += i->first.begin.column; + here.end.line = here.begin.line + i->first.begin.line; + here.end.column = here.begin.column + i->first.begin.column; + error_list.push_back(spot::tgba_parse_error(here, i->second)); + } + $1->push_back(pair(false, f)); } delete $2; $$ = $1; diff --git a/src/tgbaparse/tgbascan.ll b/src/tgbaparse/tgbascan.ll index 76aa8d49b..dfaee6b00 100644 --- a/src/tgbaparse/tgbascan.ll +++ b/src/tgbaparse/tgbascan.ll @@ -22,6 +22,7 @@ %option noyywrap %option prefix="tgbayy" %option outfile="lex.yy.c" +%x STATE_STRING %{ #include @@ -50,12 +51,6 @@ eol \n|\r|\n\r|\r\n yylloc->step (); %} -\"[^\"]*\" { - yylval->str = new std::string(yytext + 1, - yyleng - 2); - return STRING; - } - acc[ \t]*= return ACC_DEF; [a-zA-Z][a-zA-Z0-9_]* { @@ -67,8 +62,27 @@ acc[ \t]*= return ACC_DEF; {eol} yylloc->lines(yyleng); yylloc->step(); [ \t]+ yylloc->step(); +\" { + yylval->str = new std::string; + BEGIN(STATE_STRING); + } + . return *yytext; + /* Handle \" and \\ in strings. */ +{ + \" { + BEGIN(INITIAL); + return STRING; + } + \\["\\] yylval->str->append(1, yytext[1]); + [^"\\]+ yylval->str->append (yytext, yyleng); + <> { + BEGIN(INITIAL); + return UNTERMINATED_STRING; + } +} + %{ /* Dummy use of yyunput to shut up a gcc warning. */ (void) &yyunput; diff --git a/src/tgbatest/emptchke.test b/src/tgbatest/emptchke.test index 44c21ce9c..5b7b669f7 100755 --- a/src/tgbatest/emptchke.test +++ b/src/tgbatest/emptchke.test @@ -27,8 +27,8 @@ set -e cat >input <<'EOF' acc = c d; -s1, "s2", a!b, c d; -"s2", "state 3", a, c; +s1, "s2", "a & !b", c d; +"s2", "state 3", "a", c; "state 3", s1,,; EOF diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test index 5c8767cb9..6feaaf419 100755 --- a/src/tgbatest/explicit.test +++ b/src/tgbatest/explicit.test @@ -32,11 +32,11 @@ digraph G { 0 [label="", style=invis, height=0] 0 -> 1 1 [label="state 0"] - 1 -> 2 [label="T\n"] + 1 -> 2 [label="1\n"] 2 [label="state 1"] - 2 -> 3 [label="\n"] + 2 -> 3 [label="a\n"] 3 [label="state 2"] - 3 -> 1 [label="\nF"] + 3 -> 1 [label="(b & c)\nF"] } EOF diff --git a/src/tgbatest/explpro2.test b/src/tgbatest/explpro2.test index 0949b6c06..ff0b2a515 100755 --- a/src/tgbatest/explpro2.test +++ b/src/tgbatest/explpro2.test @@ -27,27 +27,27 @@ set -e cat >input1 <input2 <expected < 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' \ +perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(!b & a\)/(a & !b)/g;s/\(!c & a\)/(a & !c)/g' \ stdout > tmp_ && mv tmp_ stdout cat stdout diff --git a/src/tgbatest/explpro3.test b/src/tgbatest/explpro3.test index d75a11237..0329c843a 100755 --- a/src/tgbatest/explpro3.test +++ b/src/tgbatest/explpro3.test @@ -27,27 +27,27 @@ set -e cat >input1 <input2 <expected < stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -sed 's/"p3" "p2"/"p2" "p3"/g' stdout > tmp_ && mv tmp_ stdout +sed 's/"p3" "p2"/"p2" "p3"/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 0ada7a935..c2615e897 100755 --- a/src/tgbatest/explprod.test +++ b/src/tgbatest/explprod.test @@ -27,29 +27,29 @@ set -e cat >input1 <input2 <expected < 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' \ +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/mixprod.test b/src/tgbatest/mixprod.test index 57f2e705b..9e72bab17 100755 --- a/src/tgbatest/mixprod.test +++ b/src/tgbatest/mixprod.test @@ -30,10 +30,10 @@ set -e cat >input1 <stdout diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index c3e3e329a..f306437e7 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -27,8 +27,8 @@ set -e cat >input <expected < tmp_ && mv tmp_ stdout +sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff stdout expected @@ -52,7 +52,7 @@ mv stdout input # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -sed 's/"d" "c"/"c" "d"/g' stdout > tmp_ && mv tmp_ stdout +sed 's/"d" "c"/"c" "d"/g;s/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff input stdout diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test index 2423bac68..14ec7eb85 100755 --- a/src/tgbatest/tgbaread.test +++ b/src/tgbatest/tgbaread.test @@ -27,8 +27,8 @@ set -e cat >input < 1 1 [label="s1"] - 1 -> 2 [label="\n"] + 1 -> 2 [label="(a & !b)\n"] 2 [label="s2"] - 2 -> 3 [label="\n"] + 2 -> 3 [label="a\n"] 3 [label="state 3"] - 3 -> 1 [label="T\nF"] + 3 -> 1 [label="1\nF"] } EOF +# Sort out some possible inversions in the output. +# (The order is not guaranteed by SPOT.) +sed 's/!b & a/a \& !b/g' stdout > tmp_ && mv tmp_ stdout diff stdout expected rm input stdout expected diff --git a/src/tgbatest/tripprod.test b/src/tgbatest/tripprod.test index d24e72870..5f36f20cd 100755 --- a/src/tgbatest/tripprod.test +++ b/src/tgbatest/tripprod.test @@ -27,41 +27,41 @@ set -e cat >input1 <input2 <input3 <expected < stdout # Sort out some possible inversions in the output. # (The order is not guaranteed by SPOT.) -perl -pe 's/c a/a c/g;s/b a/a b/g;s/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1, $2, $3, $4]}/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