From c2b3dac7aa4aefe62efc44782a5967814cdb97e8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 2 Mar 2010 16:25:08 +0100 Subject: [PATCH] Parse the fusion operator (":") and translate it in ltl2tgba_fm(). * src/ltlast/multop.hh (multop::type::Fusion): New operator. * src/ltlast/multop.cc: Handle it. * src/ltlparse/ltlparse.yy: Declare OP_FUSION and add grammar rules. * src/ltlparse/ltlscan.ll: Recognize ":" as OP_FUSION. * src/tgbaalgos/ltl2tgba_fm.cc (ratexp_trad_visitor::visit): Add translation rule for multop::Fusion. * src/tgbatest/ltl2tgba.test: Add more tests. * src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc, src/ltlvisit/contain.cc, src/ltlvisit/mark.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Handle multop::Fusion in switches. --- src/ltlast/multop.cc | 32 +++++++++++----- src/ltlast/multop.hh | 2 +- src/ltlparse/ltlparse.yy | 10 +++-- src/ltlparse/ltlscan.ll | 1 + src/ltlvisit/basicreduce.cc | 1 + src/ltlvisit/consterm.cc | 11 ++++++ src/ltlvisit/contain.cc | 1 + src/ltlvisit/mark.cc | 1 + src/ltlvisit/nenoform.cc | 31 +++++++++------ src/ltlvisit/syntimpl.cc | 2 + src/ltlvisit/tostring.cc | 6 +++ src/tgba/formula2bdd.cc | 1 + src/tgbaalgos/eltl2tgba_lacim.cc | 1 + src/tgbaalgos/ltl2taa.cc | 1 + src/tgbaalgos/ltl2tgba_fm.cc | 65 ++++++++++++++++++++++++++++++++ src/tgbaalgos/ltl2tgba_lacim.cc | 1 + src/tgbatest/ltl2tgba.test | 4 ++ 17 files changed, 146 insertions(+), 25 deletions(-) diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index ce9685070..7025e04ff 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -1,8 +1,8 @@ // Copyright (C) 2009, 2010 Laboratoire de Recherche et D�veloppement // de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de -// Paris 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC), -// Universit� Pierre et Marie Curie. +// 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. // @@ -113,6 +113,8 @@ namespace spot return "Or"; case Concat: return "Concat"; + case Fusion: + return "Fusion"; } // Unreachable code. assert(0); @@ -149,48 +151,60 @@ namespace spot } else { - // All operator except "Concat" not commutative, so - // we just keep a list of the inlined arguments that - // should later be added to the vector. + // All operator except "Concat" and "Fusion" are + // commutative, so we just keep a list of the inlined + // arguments that should later be added to the vector. // For concat we have to keep track of the order of // all the arguments. - if (op == Concat) + if (op == Concat || op == Fusion) inlined.push_back(*i); ++i; } } - if (op == Concat) + if (op == Concat || op == Fusion) *v = inlined; else v->insert(v->end(), inlined.begin(), inlined.end()); } - if (op != Concat) + if (op != Concat && op != Fusion) std::sort(v->begin(), v->end(), formula_ptr_less_than()); formula* neutral; formula* abs; + formula* abs2; formula* weak_abs; switch (op) { case And: neutral = constant::true_instance(); abs = constant::false_instance(); + abs2 = 0; weak_abs = constant::empty_word_instance(); break; case Or: neutral = constant::false_instance(); abs = constant::true_instance(); + abs2 = 0; weak_abs = 0; break; case Concat: neutral = constant::empty_word_instance(); abs = constant::false_instance(); + abs2 = 0; weak_abs = 0; break; + case Fusion: + neutral = constant::true_instance(); + abs = constant::false_instance(); + abs2 = constant::empty_word_instance(); + weak_abs = 0; + break; + default: neutral = 0; abs = 0; + abs2 = 0; weak_abs = 0; break; } @@ -209,7 +223,7 @@ namespace spot (*i)->destroy(); i = v->erase(i); } - else if (*i == abs) + else if (*i == abs || *i == abs2) { for (i = v->begin(); i != v->end(); ++i) (*i)->destroy(); diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 3b6919d2d..db74e8e3a 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -41,7 +41,7 @@ namespace spot class multop : public ref_formula { public: - enum type { Or, And, Concat }; + enum type { Or, And, Concat, Fusion }; /// List of formulae. typedef std::vector vec; diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index a2ba35c4d..990a21670 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -83,11 +83,11 @@ using namespace spot::ltl; %token OP_U "until operator" OP_R "release operator" %token OP_W "weak until operator" OP_M "strong release operator" %token OP_F "sometimes operator" OP_G "always operator" -%token OP_X "next operator" OP_NOT "not operator" +%token OP_X "next operator" OP_NOT "not operator" OP_STAR "star operator" %token OP_UCONCAT "universal concat operator" %token OP_ECONCAT "existential concat operator" %token ATOMIC_PROP "atomic proposition" -%token OP_STAR "star operator" OP_CONCAT "concat operator" +%token OP_CONCAT "concat operator" OP_FUSION "fusion operator" %token CONST_TRUE "constant true" CONST_FALSE "constant false" %token END_OF_INPUT "end of formula" CONST_EMPTYWORD "empty word" %token OP_POST_NEG "negative suffix" OP_POST_POS "positive suffix" @@ -97,7 +97,7 @@ using namespace spot::ltl; /* Low priority regex operator. */ %left OP_UCONCAT OP_ECONCAT -%left OP_CONCAT +%left OP_CONCAT OP_FUSION /* Logical operators. */ %left OP_IMPLIES OP_EQUIV @@ -264,6 +264,10 @@ rationalexp: booleanatom { $$ = multop::instance(multop::Concat, $1, $3); } | rationalexp OP_CONCAT error { missing_right_binop($$, $1, @2, "concat operator"); } + | rationalexp OP_FUSION rationalexp + { $$ = multop::instance(multop::Fusion, $1, $3); } + | rationalexp OP_FUSION error + { missing_right_binop($$, $1, @2, "fusion operator"); } | rationalexp OP_STAR { $$ = unop::instance(unop::Star, $1); } diff --git a/src/ltlparse/ltlscan.ll b/src/ltlparse/ltlscan.ll index b5a8b3d77..01f6a2ed9 100644 --- a/src/ltlparse/ltlscan.ll +++ b/src/ltlparse/ltlscan.ll @@ -97,6 +97,7 @@ flex_set_buffer(const char* buf, int start_tok) "<=>"|"<->"|"<-->" BEGIN(0); return token::OP_EQUIV; "*" BEGIN(0); return token::OP_STAR; ";" BEGIN(0); return token::OP_CONCAT; +":" BEGIN(0); return token::OP_FUSION; "[]->" BEGIN(0); return token::OP_UCONCAT; "<>->" BEGIN(0); return token::OP_ECONCAT; diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 35474254d..33e9ccdd8 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -787,6 +787,7 @@ namespace spot break; case multop::Concat: + case multop::Fusion: std::copy(res->begin(), res->end(), tmpOther->end()); break; } diff --git a/src/ltlvisit/consterm.cc b/src/ltlvisit/consterm.cc index 74b93e4e3..dae0ba8dd 100644 --- a/src/ltlvisit/consterm.cc +++ b/src/ltlvisit/consterm.cc @@ -97,6 +97,13 @@ namespace spot void visit(const multop* mo) { + // The fusion operator cannot be used to recognize the empty word. + if (mo->op() == multop::Fusion) + { + result_ = false; + return; + } + unsigned max = mo->size(); // This sets the initial value of result_. mo->nth(0)->accept(*this); @@ -118,6 +125,10 @@ namespace spot if (!result_) return; break; + case multop::Fusion: + /* Unreachable code */ + assert(0); + break; } } } diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 0a38faa26..eda34ca8c 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -356,6 +356,7 @@ namespace spot } break; case multop::Concat: + case multop::Fusion: break; } if (changed) diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 772817df1..30608e7f6 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -166,6 +166,7 @@ namespace spot { case multop::Or: case multop::Concat: + case multop::Fusion: for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); break; diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 8ce7f66a3..3eb6573db 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -226,23 +226,30 @@ namespace spot op = multop::And; break; case multop::Concat: + case multop::Fusion: break; } multop::vec* res = new multop::vec; unsigned mos = mo->size(); - if (op != multop::Concat) + switch (op) { - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse(mo->nth(i))); - result_ = multop::instance(op, res); - } - else - { - for (unsigned i = 0; i < mos; ++i) - res->push_back(recurse_(mo->nth(i), false)); - result_ = multop::instance(op, res); - if (negated_) - result_ = unop::instance(unop::Not, result_); + case multop::And: + case multop::Or: + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse(mo->nth(i))); + result_ = multop::instance(op, res); + break; + } + case multop::Concat: + case multop::Fusion: + { + for (unsigned i = 0; i < mos; ++i) + res->push_back(recurse_(mo->nth(i), false)); + result_ = multop::instance(op, res); + if (negated_) + result_ = unop::instance(unop::Not, result_); + } } } diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index 0034834e8..9c0e2b32d 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -203,6 +203,7 @@ namespace spot result_ = true; break; case multop::Concat: + case multop::Fusion: break; } } @@ -458,6 +459,7 @@ namespace spot result_ = true; break; case multop::Concat: + case multop::Fusion: break; } } diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index d47493926..2e53948e4 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -259,6 +259,9 @@ namespace spot case multop::Concat: ch = ";"; break; + case multop::Fusion: + ch = ":"; + break; } for (unsigned n = 1; n < max; ++n) @@ -460,6 +463,9 @@ namespace spot case multop::Concat: ch = ";"; break; + case multop::Fusion: + ch = ":"; + break; } for (unsigned n = 1; n < max; ++n) diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 8bae93f3d..7b4959da9 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -142,6 +142,7 @@ namespace spot res_ = bddfalse; break; case multop::Concat: + case multop::Fusion: assert(!"unsupported operator"); } assert(op != -1); diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 34731c90d..6804bf241 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -159,6 +159,7 @@ namespace spot res_ = bddfalse; break; case multop::Concat: + case multop::Fusion: assert(!"unsupported operator"); } assert(op != -1); diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index 81c22ca54..4b7b33704 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -323,6 +323,7 @@ namespace spot } return; case multop::Concat: + case multop::Fusion: assert(!"unsupported operator"); return; } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 2db1c6b8e..f790ecdf1 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -486,6 +486,70 @@ namespace spot multop::instance(multop::Concat, v)); break; } + case multop::Fusion: + { + assert(node->size() >= 2); + + // the head + bdd res = recurse(node->nth(0)); + + // the tail + multop::vec* v = new multop::vec; + unsigned s = node->size(); + v->reserve(s - 1); + for (unsigned n = 1; n < s; ++n) + v->push_back(node->nth(n)->clone()); + formula* tail = multop::instance(multop::Fusion, v); + bdd tail_bdd; + bool tail_computed = false; + + //trace_ltl_bdd(dict_, res); + + minato_isop isop(res); + bdd cube; + res_ = bddfalse; + while ((cube = isop.next()) != bddfalse) + { + bdd label = bdd_exist(cube, dict_.next_set); + bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); + formula* dest = dict_.conj_bdd_to_formula(dest_bdd); + + if (constant_term_as_bool(dest)) + { + // The destination is a final state. Make sure we + // can also exit if tail is satisfied. + if (!tail_computed) + { + tail_bdd = recurse(tail, + to_concat_ ? + to_concat_->clone() : 0); + tail_computed = true; + } + res_ |= label & tail_bdd; + } + + if (dynamic_cast(dest) == 0) + { + // If the destination is not a constant, it + // means it can have successors. Fusion the + // tail and append anything to concatenate. + formula* dest2 = multop::instance(multop::Fusion, dest, + tail->clone()); + if (to_concat_) + dest2 = multop::instance(multop::Concat, dest2, + to_concat_->clone()); + if (dest2 != constant::false_instance()) + { + int x = dict_.register_next_variable(dest2); + dest2->destroy(); + res_ |= label & bdd_ithvar(x); + } + } + } + + tail->destroy(); + break; + } } } @@ -822,6 +886,7 @@ namespace spot break; } case multop::Concat: + case multop::Fusion: assert(!"Not an LTL operator"); break; } diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index 85503e88f..ad7323f3e 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -257,6 +257,7 @@ namespace spot res_ = bddfalse; break; case multop::Concat: + case multop::Fusion: assert(!"unsupported operator"); } assert(op != -1); diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index c9c77fe81..46e6151ae 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -64,6 +64,10 @@ check_psl '{((a*;b;c)*)&((b*;a;c)*)}<>->x' check_psl '{(g;y;r)*}<>->x' check_psl 'G({(g;y;r)*}<>->x)' check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' +check_psl 'G({(a;b)*}<>->x)&G({(c;d)*}<>->y)' +check_psl '{(#e + a):c*:(#e + b)}<>->d' +check_psl '{a;e;f:(g*);h}<>->d' +check_psl '{(a:b)* & (c*:d)}<>->e' # Make sure 'a U (b U c)' has 3 states and 6 transitions, # before and after degeneralization.