From b06c9cd563ce155ffbbd50f65eb033d32df7ea94 Mon Sep 17 00:00:00 2001 From: Damien Lefortier Date: Sat, 18 Apr 2009 16:24:18 +0200 Subject: [PATCH] Extend the ELTL parser to support more complex aliases of automaton operators such as Strong=G(F($0))->G(F($1)) and G=R(false, $0). * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add support for more complex aliases. * src/eltltest/acc.cc, src/eltltest/acc.test: Adjust. * src/ltlast/nfa.cc, src/ltlast/nfa.hh (arity): Now returns an unsigned value. * src/tgbatest/eltl2tgba.test: Adjust. * src/tgbalagos/eltl2tgba_lacim.cc: Fix sanity. --- ChangeLog | 14 +++ src/eltlparse/eltlparse.yy | 187 +++++++++++++++++++++---------- src/eltlparse/eltlscan.ll | 3 + src/eltltest/acc.cc | 9 ++ src/eltltest/acc.test | 12 ++ src/ltlast/nfa.cc | 10 +- src/ltlast/nfa.hh | 2 +- src/tgbaalgos/eltl2tgba_lacim.cc | 5 +- src/tgbatest/eltl2tgba.cc | 1 - src/tgbatest/eltl2tgba.test | 11 ++ 10 files changed, 188 insertions(+), 66 deletions(-) diff --git a/ChangeLog b/ChangeLog index ece7cf309..c85fc9252 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,17 @@ +2009-04-18 Damien Lefortier + + Extend the ELTL parser to support more complex aliases of + automaton operators such as Strong=G(F($0))->G(F($1)) and + G=R(false, $0). + + * src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll: Add + support for more complex aliases. + * src/eltltest/acc.cc, src/eltltest/acc.test: Adjust. + * src/ltlast/nfa.cc, src/ltlast/nfa.hh (arity): Now returns an + unsigned value. + * src/tgbatest/eltl2tgba.test: Adjust. + * src/tgbalagos/eltl2tgba_lacim.cc: Fix sanity. + 2009-04-09 Guillaume SADEGH Minor fixes to compile with GCC 4.4. diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 5debf3595..5d2039ee0 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -57,26 +57,24 @@ namespace spot struct alias_not : alias { - alias_ptr s; + alias_ptr child; }; - struct alias_binary : alias + struct alias_binop : alias { - virtual ~alias_binary() = 0; // Should not be instanciate + binop::type op; alias_ptr lhs; alias_ptr rhs; }; - struct alias_binop : alias_binary + struct alias_multop : alias { - binop::type ty; - }; - struct alias_multop : alias_binary - { - multop::type ty; + multop::type op; + alias_ptr lhs; + alias_ptr rhs; }; struct alias_nfa : alias { + std::vector children; spot::ltl::nfa::ptr nfa; - std::list s; }; struct alias_arg : alias { @@ -93,28 +91,32 @@ namespace spot std::string file_; }; + /// TODO: maybe implementing a visitor could be better than + /// dynamic casting all the time here. + /// Instanciate the formula corresponding to the given alias. static formula* - alias2formula(alias_ptr ap, spot::ltl::automatop::vec* v) + alias2formula(const alias_ptr ap, spot::ltl::automatop::vec* v) { if (alias_not* a = dynamic_cast(ap.get())) - return unop::instance(unop::Not, alias2formula(a->s, v)); + return unop::instance(unop::Not, alias2formula(a->child, v)); if (alias_arg* a = dynamic_cast(ap.get())) - return a->i == -1 ? constant::true_instance() : v->at(a->i); + return a->i == -1 ? constant::true_instance() : + a->i == -2 ? constant::false_instance() : v->at(a->i); if (alias_nfa* a = dynamic_cast(ap.get())) { automatop::vec* va = new automatop::vec; - std::list::const_iterator i = a->s.begin(); - while (i != a->s.end()) + std::vector::const_iterator i = a->children.begin(); + while (i != a->children.end()) va->push_back(alias2formula(*i++, v)); return automatop::instance(a->nfa, va, false); } if (alias_binop* a = dynamic_cast(ap.get())) - return binop::instance(a->ty, + return binop::instance(a->op, alias2formula(a->lhs, v), alias2formula(a->rhs, v)); if (alias_multop* a = dynamic_cast(ap.get())) - return multop::instance(a->ty, + return multop::instance(a->op, alias2formula(a->lhs, v), alias2formula(a->rhs, v)); @@ -124,29 +126,74 @@ namespace spot /// Get the arity of a given alias. static size_t - arity(alias_ptr ap) + arity(const alias_ptr ap) { if (alias_not* a = dynamic_cast(ap.get())) - return arity(a->s); + return arity(a->child); if (alias_arg* a = dynamic_cast(ap.get())) - return a->i + 1; + return std::max(a->i + 1, 0); if (alias_nfa* a = dynamic_cast(ap.get())) { size_t res = 0; - std::list::const_iterator i = a->s.begin(); - while (i != a->s.end()) + std::vector::const_iterator i = a->children.begin(); + while (i != a->children.end()) res = std::max(arity(*i++), res); return res; } - if (alias_binary* a = dynamic_cast(ap.get())) + if (alias_binop* a = dynamic_cast(ap.get())) + return std::max(arity(a->lhs), arity(a->rhs)); + if (alias_multop* a = dynamic_cast(ap.get())) return std::max(arity(a->lhs), arity(a->rhs)); /* Unreachable code. */ assert(0); } - /// Create a new alias from an existing one according to \a v. - /// TODO. + /// Alias an existing alias, as in Strong=G(F($0))->G(F($1)), + /// where F is an alias. + /// + /// \param ap The original alias. + /// \param v The arguments of the new alias. + static alias_ptr + realias(const alias_ptr ap, std::vector v) + { + if (alias_not* a = dynamic_cast(ap.get())) + { + alias_not* res = new alias_not; + res->child = realias(a->child, v); + return alias_ptr(res); + } + if (alias_arg* a = dynamic_cast(ap.get())) // Do it. + return a->i < 0 ? ap : v.at(a->i); + if (alias_nfa* a = dynamic_cast(ap.get())) + { + alias_nfa* res = new alias_nfa; + std::vector::const_iterator i = a->children.begin(); + while (i != a->children.end()) + res->children.push_back(realias(*i++, v)); + res->nfa = a->nfa; + return alias_ptr(res); + } + if (alias_binop* a = dynamic_cast(ap.get())) + { + alias_binop* res = new alias_binop; + res->op = a->op; + res->lhs = realias(a->lhs, v); + res->rhs = realias(a->rhs, v); + return alias_ptr(res); + } + if (alias_multop* a = dynamic_cast(ap.get())) + { + alias_multop* res = new alias_multop; + res->op = a->op; + res->lhs = realias(a->lhs, v); + res->rhs = realias(a->rhs, v); + return alias_ptr(res); + } + + /* Unreachable code. */ + assert(0); + } } } @@ -156,7 +203,7 @@ namespace spot #define CHECK_EXISTING_NMAP(Loc, Ident) \ { \ - nfamap::iterator i = nmap.find(*Ident); \ + nfamap::const_iterator i = nmap.find(*Ident); \ if (i == nmap.end()) \ { \ std::string s = "unknown automaton operator `"; \ @@ -308,7 +355,7 @@ nfa: IDENT "=" "(" nfa_def ")" nfa_def: /* empty */ { - $$ = new nfa(); + $$ = new nfa; } | nfa_def STATE STATE nfa_arg { @@ -324,59 +371,86 @@ nfa_def: /* empty */ nfa_alias: IDENT "(" nfa_alias_arg_list ")" { - aliasmap::iterator i = amap.find(*$1); + aliasmap::const_iterator i = amap.find(*$1); if (i != amap.end()) - assert(0); // FIXME + { + CHECK_ARITY(@1, $1, $3->children.size(), arity(i->second)); + + // Hack to return the right type without screwing with the + // boost::shared_ptr memory handling by using get for + // example. FIXME: Wait for the next version of boost and + // modify the %union to handle alias_ptr. + alias_not* tmp1 = new alias_not; + tmp1->child = realias(i->second, $3->children); + alias_not* tmp2 = new alias_not; + tmp2->child = alias_ptr(tmp1); + $$ = tmp2; + delete $3; + } else { CHECK_EXISTING_NMAP(@1, $1); nfa::ptr np = nmap[*$1]; - CHECK_ARITY(@1, $1, $3->s.size(), - static_cast(np->arity())); + CHECK_ARITY(@1, $1, $3->children.size(), np->arity()); $3->nfa = np; $$ = $3; } delete $1; } - /// TODO - // | IDENT "(" nfa_alias ")" // Should be a list - // { - // assert(0); - // } | OP_NOT nfa_alias { - alias_not* a = new alias_not; - a->s = alias_ptr($2); - $$ = a; + alias_not* res = new alias_not; + res->child = alias_ptr($2); + $$ = res; } + | nfa_alias OP_IMPLIES nfa_alias + { + alias_binop* res = new alias_binop; + res->op = binop::Implies; + res->lhs = alias_ptr($1); + res->rhs = alias_ptr($3); + $$ = res; + } + // More TBD here. + +nfa_alias_arg: nfa_arg + { + alias_arg* res = new alias_arg; + res->i = $1; + $$ = res; + } + | CONST_FALSE + { + alias_arg* res = new alias_arg; + res->i = -2; + $$ = res; + } + | OP_NOT nfa_alias_arg + { + alias_not* res = new alias_not; + res->child = alias_ptr($2); + $$ = res; + } + // More TBD here. nfa_alias_arg_list: nfa_alias_arg { $$ = new alias_nfa; - $$->s.push_back(alias_ptr($1)); + $$->children.push_back(alias_ptr($1)); + } + | nfa_alias // Cannot factorize because != . + { + $$ = new alias_nfa; + $$->children.push_back(alias_ptr($1)); } | nfa_alias_arg_list "," nfa_alias_arg { - $1->s.push_back(alias_ptr($3)); + $1->children.push_back(alias_ptr($3)); $$ = $1; } ; -nfa_alias_arg: nfa_arg - { - alias_arg* a = new alias_arg; - a->i = $1; - $$ = a; - } - | OP_NOT nfa_alias_arg - { - alias_not* a = new alias_not; - a->s = alias_ptr($2); - $$ = a; - } - // TODO: factoring with nfa_alias - nfa_arg: ARG { if ($1 == -1) @@ -449,8 +523,7 @@ subformula: ATOMIC_PROP CHECK_EXISTING_NMAP(@1, $1); nfa::ptr np = nmap[*$1]; - CHECK_ARITY(@1, $1, $3->size(), - static_cast(np->arity())); + CHECK_ARITY(@1, $1, $3->size(), np->arity()); $$ = automatop::instance(np, $3, false); } delete $1; diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll index 47b0abfc0..f26a3cdb5 100644 --- a/src/eltlparse/eltlscan.ll +++ b/src/eltlparse/eltlscan.ll @@ -105,6 +105,9 @@ eol \n|\r|\n\r|\r\n [tT][rR][uU][eE] { return token::CONST_TRUE; } +[fF][aA][lL][sS][eE] { + return token::CONST_FALSE; + } [a-zA-Z][a-zA-Z0-9_]* { yylval->sval = new std::string(yytext, yyleng); diff --git a/src/eltltest/acc.cc b/src/eltltest/acc.cc index cf00a7833..0c71f7d11 100644 --- a/src/eltltest/acc.cc +++ b/src/eltltest/acc.cc @@ -22,6 +22,9 @@ #include #include #include "eltlparse/public.hh" +#include "ltlvisit/destroy.hh" +#include "ltlvisit/lunabbrev.hh" +#include "ltlvisit/nenoform.hh" int main(int argc, char** argv) @@ -37,6 +40,12 @@ main(int argc, char** argv) return 1; } + const spot::ltl::formula* f1 = spot::ltl::unabbreviate_logic(f); + const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(f1); + spot::ltl::destroy(f1); + assert(f != 0); std::cout << f->dump() << std::endl; + assert(f2 != 0); + std::cout << f2->dump() << std::endl; } diff --git a/src/eltltest/acc.test b/src/eltltest/acc.test index ab9b9b939..fca12d508 100755 --- a/src/eltltest/acc.test +++ b/src/eltltest/acc.test @@ -22,6 +22,18 @@ A(1,a,a|b)&X(!f) EOF run 0 ./acc input || exit 1 +cat >input <input <dst = add_state(dst); t->label = label; s->push_back(t); - if (label > arity_) - arity_ = label; + if (label >= arity_) + arity_ = label + 1; } void @@ -96,10 +96,10 @@ namespace spot return finals_.empty(); } - int + unsigned nfa::arity() { - return arity_ + 1; + return arity_; } const nfa::state* diff --git a/src/ltlast/nfa.hh b/src/ltlast/nfa.hh index d75f0ae72..98ec2de63 100644 --- a/src/ltlast/nfa.hh +++ b/src/ltlast/nfa.hh @@ -74,7 +74,7 @@ namespace spot bool is_loop(); /// \brief Get the `arity' i.e. max t.cost, for each transition t. - int arity(); + unsigned arity(); /// \brief Return an iterator on the first succesor (if any) of \a state. /// diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index c1b897034..0bd3781fe 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -228,13 +228,14 @@ namespace spot fact_.constrain_relation(bdd_apply(bdd_ithvar(v1), tmp1, bddop_biimp)); if (is_loop) { - fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_invimp)); acc &= bdd_ithvar(v2) | !tmpacc; + fact_.constrain_relation( + bdd_apply(bdd_ithvar(v2), tmp2, bddop_invimp)); } else { - fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp)); acc &= bdd_nithvar(v2) | tmpacc; + fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp)); } return m[s]; diff --git a/src/tgbatest/eltl2tgba.cc b/src/tgbatest/eltl2tgba.cc index 07e1ebaaf..b4a168ac9 100644 --- a/src/tgbatest/eltl2tgba.cc +++ b/src/tgbatest/eltl2tgba.cc @@ -95,7 +95,6 @@ main(int argc, char** argv) input += spot::ltl::to_string(f, true); spot::ltl::destroy(f); - // std::cerr << input << std::endl; f = spot::eltl::parse_string(input, p, env, false); formula_index = 2; } diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test index 65c4e16d1..b9212be25 100755 --- a/src/tgbatest/eltl2tgba.test +++ b/src/tgbatest/eltl2tgba.test @@ -37,6 +37,7 @@ G=( 0 0 \$0 ) F=U(true, \$0) +Strong=G(F(\$0))->G(F(\$1)) R=!U(!\$0, !\$1) EOF @@ -114,6 +115,16 @@ check_construct input check_true 'Fa' check_false '!Fa' +cat >input <G(F(b))' +check_false '!(G(F(a))->G(F(b)))' + cat >input <