diff --git a/ChangeLog b/ChangeLog index 0458eedff..d50e50db5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,25 @@ +2009-06-05 Damien Lefortier + + Modify the ELTL parser to be able to support PSL operators. Add a + new keyword in the ELTL format: finish, which applies to an + automaton operator and tells whether it just completed. + + * src/eltlparse/eltlparse.yy: Clean it. Add finish. + * src/eltlparse/eltlscan.ll: Add finish. + * src/formula_tree.cc, src/formula_tree.hh: New files. Define a + small AST representing formulae where atomic props are unknown + which is used in the ELTL parser. + * src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc, + ltlast/nfa.hh: Adjust. + * src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop. + * src/ltlvisit/basicreduce.cc, src/ltlvisit/nenoform.cc, + src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc, + src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc, + src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc, + src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches. + * src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish. + * src/tgbatest/eltl2tgba.test: More tests. + 2009-06-02 Alexandre Duret-Lutz * src/tgbatest/scc.test: Redirect stdout into file `stdout' diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 5d2039ee0..206e92be3 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -36,53 +36,22 @@ #include #include "public.hh" #include "ltlast/allnodes.hh" +#include "ltlast/formula_tree.hh" #include "ltlvisit/destroy.hh" +#include "ltlvisit/clone.hh" namespace spot { namespace eltl { + typedef std::map nfamap; + /// The following parser allows one to define aliases of automaton /// operators such as: F=U(true,$0). Internally it's handled by /// creating a small AST associated with each alias in order to /// instanciate the right automatop after: U(constant(1), AP(f)) /// for the formula F(f). - /// - struct alias - { - virtual ~alias() {}; - }; - /// We use boost::shared_ptr to easily handle deletion. - typedef boost::shared_ptr alias_ptr; - - struct alias_not : alias - { - alias_ptr child; - }; - struct alias_binop : alias - { - binop::type op; - alias_ptr lhs; - alias_ptr rhs; - }; - struct alias_multop : alias - { - multop::type op; - alias_ptr lhs; - alias_ptr rhs; - }; - struct alias_nfa : alias - { - std::vector children; - spot::ltl::nfa::ptr nfa; - }; - struct alias_arg : alias - { - int i; - }; - - typedef std::map nfamap; - typedef std::map aliasmap; + typedef std::map aliasmap; /// Implementation details for error handling. struct parse_error_list_t @@ -91,104 +60,51 @@ 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(const alias_ptr ap, spot::ltl::automatop::vec* v) - { - if (alias_not* a = dynamic_cast(ap.get())) - return unop::instance(unop::Not, alias2formula(a->child, v)); - if (alias_arg* a = dynamic_cast(ap.get())) - 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::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->op, - alias2formula(a->lhs, v), - alias2formula(a->rhs, v)); - if (alias_multop* a = dynamic_cast(ap.get())) - return multop::instance(a->op, - alias2formula(a->lhs, v), - alias2formula(a->rhs, v)); - - /* Unreachable code. */ - assert(0); - } - - /// Get the arity of a given alias. - static size_t - arity(const alias_ptr ap) - { - if (alias_not* a = dynamic_cast(ap.get())) - return arity(a->child); - if (alias_arg* a = dynamic_cast(ap.get())) - return std::max(a->i + 1, 0); - if (alias_nfa* a = dynamic_cast(ap.get())) - { - size_t res = 0; - std::vector::const_iterator i = a->children.begin(); - while (i != a->children.end()) - res = std::max(arity(*i++), res); - return res; - } - 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); - } + using namespace spot::ltl::formula_tree; /// 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) + static node_ptr + realias(const node_ptr ap, std::vector v) { - if (alias_not* a = dynamic_cast(ap.get())) + if (node_atomic* a = dynamic_cast(ap.get())) // Do it. + return a->i < 0 ? ap : v.at(a->i); + + // Traverse the tree. + if (node_unop* 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; + node_unop* res = new node_unop; res->op = a->op; - res->lhs = realias(a->lhs, v); - res->rhs = realias(a->rhs, v); - return alias_ptr(res); + res->child = realias(a->child, v); + return node_ptr(res); } - if (alias_multop* a = dynamic_cast(ap.get())) + if (node_nfa* 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); + node_nfa* res = new node_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 node_ptr(res); + } + if (node_binop* a = dynamic_cast(ap.get())) + { + node_binop* res = new node_binop; + res->op = a->op; + res->lhs = realias(a->lhs, v); + res->rhs = realias(a->rhs, v); + return node_ptr(res); + } + if (node_multop* a = dynamic_cast(ap.get())) + { + node_multop* res = new node_multop; + res->op = a->op; + res->lhs = realias(a->lhs, v); + res->rhs = realias(a->rhs, v); + return node_ptr(res); } /* Unreachable code. */ @@ -197,8 +113,8 @@ namespace spot } } -#define PARSE_ERROR(Loc, Msg) \ - pe.list_.push_back \ +#define PARSE_ERROR(Loc, Msg) \ + pe.list_.push_back \ (parse_error(Loc, spair(pe.file_, Msg))) #define CHECK_EXISTING_NMAP(Loc, Ident) \ @@ -235,6 +151,15 @@ namespace spot } \ } +#define INSTANCIATE_OP(Name, TypeNode, TypeOp, L, R) \ + { \ + TypeNode* res = new TypeNode; \ + res->op = TypeOp; \ + res->lhs = formula_tree::node_ptr(L); \ + res->rhs = formula_tree::node_ptr(R); \ + Name = res; \ + } + } %parse-param {spot::eltl::nfamap& nmap} @@ -254,8 +179,8 @@ namespace spot spot::ltl::formula* fval; /// To handle aliases. - spot::eltl::alias* pval; - spot::eltl::alias_nfa* bval; + spot::ltl::formula_tree::node* pval; + spot::ltl::formula_tree::node_nfa* bval; } %code { @@ -283,6 +208,7 @@ using namespace spot::ltl; %token ACC "accept" EQ "=" + FIN "finish" LPAREN "(" RPAREN ")" COMMA "," @@ -304,10 +230,8 @@ using namespace spot::ltl; %type nfa_def %type subformula %type arg_list -%type nfa_arg -%type nfa_alias -%type nfa_alias_arg -%type nfa_alias_arg_list +%type nfa_arg +%type nfa_arg_list %destructor { delete $$; } "atomic proposition" %destructor { spot::ltl::destroy($$); } subformula @@ -335,7 +259,7 @@ nfa: IDENT "=" "(" nfa_def ")" nmap[*$1] = nfa::ptr($4); delete $1; } - | IDENT "=" nfa_alias + | IDENT "=" nfa_arg { /// Recursivity issues of aliases are handled by a parse error. aliasmap::iterator i = amap.find(*$1); @@ -348,7 +272,7 @@ nfa: IDENT "=" "(" nfa_def ")" delete $1; YYERROR; } - amap[*$1] = alias_ptr($3); + amap.insert(make_pair(*$1, formula_tree::node_ptr($3))); delete $1; } ; @@ -359,7 +283,7 @@ nfa_def: /* empty */ } | nfa_def STATE STATE nfa_arg { - $1->add_transition($2, $3, $4); + $1->add_transition($2, $3, formula_tree::node_ptr($4)); $$ = $1; } | nfa_def ACC STATE @@ -369,21 +293,94 @@ nfa_def: /* empty */ } ; -nfa_alias: IDENT "(" nfa_alias_arg_list ")" +nfa_arg_list: nfa_arg + { + $$ = new formula_tree::node_nfa; + $$->children.push_back(formula_tree::node_ptr($1)); + } + | nfa_arg_list "," nfa_arg + { + $1->children.push_back(formula_tree::node_ptr($3)); + $$ = $1; + } +; + +nfa_arg: ARG + { + if ($1 == -1) + { + std::string s = "out of range integer"; + PARSE_ERROR(@1, s); + YYERROR; + } + formula_tree::node_atomic* res = new formula_tree::node_atomic; + res->i = $1; + $$ = res; + } + | CONST_TRUE + { + formula_tree::node_atomic* res = new formula_tree::node_atomic; + res->i = formula_tree::True; + $$ = res; + } + | CONST_FALSE + { + formula_tree::node_atomic* res = new formula_tree::node_atomic; + res->i = formula_tree::False; + $$ = res; + } + | OP_NOT nfa_arg + { + formula_tree::node_unop* res = new formula_tree::node_unop; + res->op = unop::Not; + res->child = formula_tree::node_ptr($2); + $$ = res; + } + | FIN "(" nfa_arg ")" + { + formula_tree::node_unop* res = new formula_tree::node_unop; + res->op = unop::Finish; + res->child = formula_tree::node_ptr($3); + $$ = res; + } + | nfa_arg OP_AND nfa_arg + { + INSTANCIATE_OP($$, formula_tree::node_multop, multop::And, $1, $3); + } + | nfa_arg OP_OR nfa_arg + { + INSTANCIATE_OP($$, formula_tree::node_multop, multop::Or, $1, $3); + } + | nfa_arg OP_XOR nfa_arg + { + INSTANCIATE_OP($$, formula_tree::node_binop, binop::Xor, $1, $3); + } + | nfa_arg OP_IMPLIES nfa_arg + { + INSTANCIATE_OP($$, formula_tree::node_binop, binop::Implies, $1, $3); + } + | nfa_arg OP_EQUIV nfa_arg + { + INSTANCIATE_OP($$, formula_tree::node_binop, binop::Equiv, $1, $3); + } + | IDENT "(" nfa_arg_list ")" { aliasmap::const_iterator i = amap.find(*$1); if (i != amap.end()) { - CHECK_ARITY(@1, $1, $3->children.size(), arity(i->second)); + int arity = formula_tree::arity(i->second); + CHECK_ARITY(@1, $1, $3->children.size(), arity); // 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; + // modify the %union to handle formula_tree::node_ptr. + formula_tree::node_unop* tmp1 = new formula_tree::node_unop; + tmp1->op = unop::Not; tmp1->child = realias(i->second, $3->children); - alias_not* tmp2 = new alias_not; - tmp2->child = alias_ptr(tmp1); + formula_tree::node_unop* tmp2 = new formula_tree::node_unop; + tmp2->op = unop::Not; + tmp2->child = formula_tree::node_ptr(tmp1); $$ = tmp2; delete $3; } @@ -398,73 +395,6 @@ nfa_alias: IDENT "(" nfa_alias_arg_list ")" } delete $1; } - | OP_NOT nfa_alias - { - 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; - $$->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->children.push_back(alias_ptr($3)); - $$ = $1; - } -; - -nfa_arg: ARG - { - if ($1 == -1) - { - std::string s = "out of range integer"; - PARSE_ERROR(@1, s); - YYERROR; - } - $$ = $1; - } - | CONST_TRUE - { $$ = -1; } -; - /* Formulae. */ @@ -490,12 +420,11 @@ subformula: ATOMIC_PROP aliasmap::iterator i = amap.find(*$2); if (i != amap.end()) { - CHECK_ARITY(@1, $2, 2, arity(i->second)); - automatop::vec* v = new automatop::vec; - v->push_back($1); - v->push_back($3); - $$ = alias2formula(i->second, v); - delete v; + CHECK_ARITY(@1, $2, 2, formula_tree::arity(i->second)); + automatop::vec v; + v.push_back($1); + v.push_back($3); + $$ = instanciate(i->second, v); } else { @@ -514,8 +443,8 @@ subformula: ATOMIC_PROP aliasmap::iterator i = amap.find(*$1); if (i != amap.end()) { - CHECK_ARITY(@1, $1, $3->size(), arity(i->second)); - $$ = alias2formula(i->second, $3); + CHECK_ARITY(@1, $1, $3->size(), formula_tree::arity(i->second)); + $$ = instanciate(i->second, *$3); delete $3; } else diff --git a/src/eltlparse/eltlscan.ll b/src/eltlparse/eltlscan.ll index f26a3cdb5..cae3bf216 100644 --- a/src/eltlparse/eltlscan.ll +++ b/src/eltlparse/eltlscan.ll @@ -101,6 +101,7 @@ eol \n|\r|\n\r|\r\n "=" return token::EQ; "accept" return token::ACC; +"finish" return token::FIN; [tT][rR][uU][eE] { return token::CONST_TRUE; diff --git a/src/ltlast/Makefile.am b/src/ltlast/Makefile.am index 54014c57e..aaab8d5ee 100644 --- a/src/ltlast/Makefile.am +++ b/src/ltlast/Makefile.am @@ -31,6 +31,7 @@ ltlast_HEADERS = \ binop.hh \ constant.hh \ formula.hh \ + formula_tree.hh \ multop.hh \ nfa.hh \ predecl.hh \ @@ -45,6 +46,7 @@ libltlast_la_SOURCES = \ binop.cc \ constant.cc \ formula.cc \ + formula_tree.cc \ multop.cc \ nfa.cc \ refformula.cc \ diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index bef06886d..113ec89fd 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -21,6 +21,7 @@ #include #include "automatop.hh" +#include "nfa.hh" #include "visitor.hh" namespace spot diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh index df3b229bd..ae1305cd2 100644 --- a/src/ltlast/automatop.hh +++ b/src/ltlast/automatop.hh @@ -88,11 +88,11 @@ namespace spot typedef std::map map; static map instances; - automatop(const nfa::ptr nfa, vec* v, bool negated); + automatop(const nfa::ptr, vec* v, bool negated); virtual ~automatop(); private: - nfa::ptr nfa_; + const nfa::ptr nfa_; vec* children_; bool negated_; }; diff --git a/src/ltlast/formula_tree.cc b/src/ltlast/formula_tree.cc new file mode 100644 index 000000000..09f8eac32 --- /dev/null +++ b/src/ltlast/formula_tree.cc @@ -0,0 +1,88 @@ +// Copyright (C) 2009 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 +#include "formula_tree.hh" +#include "allnodes.hh" +#include "ltlvisit/clone.hh" + +namespace spot +{ + namespace ltl + { + namespace formula_tree + { + formula* + instanciate(const node_ptr np, const std::vector& v) + { + if (node_atomic* n = dynamic_cast(np.get())) + return n->i == True ? constant::true_instance() : + n->i == False ? constant::false_instance() : clone(v.at(n->i)); + + if (node_unop* n = dynamic_cast(np.get())) + return unop::instance(n->op, instanciate(n->child, v)); + if (node_nfa* n = dynamic_cast(np.get())) + { + automatop::vec* va = new automatop::vec; + std::vector::const_iterator i = n->children.begin(); + while (i != n->children.end()) + va->push_back(instanciate(*i++, v)); + return automatop::instance(n->nfa, va, false); + } + if (node_binop* n = dynamic_cast(np.get())) + return binop::instance(n->op, + instanciate(n->lhs, v), + instanciate(n->rhs, v)); + if (node_multop* n = dynamic_cast(np.get())) + return multop::instance(n->op, + instanciate(n->lhs, v), + instanciate(n->rhs, v)); + + /* Unreachable code. */ + assert(0); + } + + size_t + arity(const node_ptr np) + { + if (node_atomic* n = dynamic_cast(np.get())) + return std::max(n->i + 1, 0); + if (node_unop* n = dynamic_cast(np.get())) + return arity(n->child); + if (node_nfa* n = dynamic_cast(np.get())) + { + size_t res = 0; + std::vector::const_iterator i = n->children.begin(); + while (i != n->children.end()) + res = std::max(arity(*i++), res); + return res; + } + if (node_binop* n = dynamic_cast(np.get())) + return std::max(arity(n->lhs), arity(n->rhs)); + if (node_multop* n = dynamic_cast(np.get())) + return std::max(arity(n->lhs), arity(n->rhs)); + + /* Unreachable code. */ + assert(0); + } + } + } +} diff --git a/src/ltlast/formula_tree.hh b/src/ltlast/formula_tree.hh new file mode 100644 index 000000000..4de43afee --- /dev/null +++ b/src/ltlast/formula_tree.hh @@ -0,0 +1,88 @@ +// Copyright (C) 2009 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. + +/// \file ltlast/formula_tree.hh +/// \brief Trees representing formulae where atomic propositions are unknown +#ifndef SPOT_LTLAST_FORMULA_TREE_HH +# define SPOT_LTLAST_FORMULA_TREE_HH + +# include +# include +# include "formula.hh" +# include "multop.hh" +# include "binop.hh" +# include "unop.hh" +# include "nfa.hh" + +namespace spot +{ + namespace ltl + { + /// Trees representing formulae where atomic propositions are unknown. + namespace formula_tree + { + struct node + { + virtual ~node() {}; + }; + /// We use boost::shared_ptr to easily handle deletion. + typedef boost::shared_ptr node_ptr; + + struct node_unop : node + { + unop::type op; + node_ptr child; + }; + struct node_binop : node + { + binop::type op; + node_ptr lhs; + node_ptr rhs; + }; + struct node_multop : node + { + multop::type op; + node_ptr lhs; + node_ptr rhs; + }; + struct node_nfa : node + { + std::vector children; + spot::ltl::nfa::ptr nfa; + }; + /// Integer values for True and False used in node_atomic. + enum { True = -1, False = -2 }; + struct node_atomic : node + { + int i; + }; + + /// Instanciate the formula corresponding to the node with + /// atomic propositions taken from \a v. + formula* instanciate(const node_ptr np, const std::vector& v); + + /// Get the arity. + size_t arity(const node_ptr np); + } + } +} + +#endif // SPOT_LTLAST_FORMULA_TREE_HH_ diff --git a/src/ltlast/nfa.cc b/src/ltlast/nfa.cc index 95490e47a..dcfea1867 100644 --- a/src/ltlast/nfa.cc +++ b/src/ltlast/nfa.cc @@ -21,6 +21,7 @@ #include #include "nfa.hh" +#include "formula_tree.hh" namespace spot { @@ -61,15 +62,16 @@ namespace spot } void - nfa::add_transition(int src, int dst, int label) + nfa::add_transition(int src, int dst, const label lbl) { state* s = add_state(src); nfa::transition* t = new transition; t->dst = add_state(dst); - t->label = label; + t->lbl = lbl; s->push_back(t); - if (label >= arity_) - arity_ = label + 1; + size_t arity = formula_tree::arity(formula_tree::node_ptr(lbl)); + if (arity >= arity_) + arity_ = arity; } void diff --git a/src/ltlast/nfa.hh b/src/ltlast/nfa.hh index 98ec2de63..033443444 100644 --- a/src/ltlast/nfa.hh +++ b/src/ltlast/nfa.hh @@ -36,31 +36,39 @@ namespace spot { /// Forward declaration. See below. class succ_iterator; + /// Forward declaration. NFA's labels are reprensented by nodes + /// which are defined in formula_tree.hh, included in nfa.cc. + namespace formula_tree + { + class node; + } /// \brief Nondeterministic Finite Automata used by automata operators. /// - /// States & labels are represented by integers. + /// States are represented by integers. + /// Labels are represented by formula_tree's nodes. /// Currently, only one initial state is possible. class nfa { public: - struct transition; - typedef std::list state; + struct transition; + typedef std::list state; + typedef boost::shared_ptr label; /// Iterator over the successors of a state. - typedef succ_iterator iterator; - typedef boost::shared_ptr ptr; + typedef succ_iterator iterator; + typedef boost::shared_ptr ptr; /// Explicit transitions. struct transition { - int label; + label lbl; const state* dst; }; nfa(); ~nfa(); - void add_transition(int src, int dst, int label); + void add_transition(int src, int dst, const label lbl); void set_init_state(int name); void set_final(int name); @@ -101,7 +109,7 @@ namespace spot is_map is_; si_map si_; - int arity_; + size_t arity_; std::string name_; state* init_; diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index f4cd9f2a4..14e946f25 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -88,6 +88,8 @@ namespace spot return "F"; case G: return "G"; + case Finish: + return "Finish"; } // Unreachable code. assert(0); diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index 487ecf034..0f522cb8f 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -37,7 +37,7 @@ namespace spot class unop : public ref_formula { public: - enum type { Not, X, F, G }; + enum type { Not, X, F, G, Finish }; // Finish is used in ELTL formulae. /// Build an unary operator with operation \a op and /// child \a child. diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 261cd5473..7c0a7dac3 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -223,6 +223,10 @@ namespace spot result_ = unop::instance(unop::G, result_); return; + + case unop::Finish: + result_ = unop::instance(unop::Finish, result_); + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/nenoform.cc b/src/ltlvisit/nenoform.cc index 054ae2863..9799996ce 100644 --- a/src/ltlvisit/nenoform.cc +++ b/src/ltlvisit/nenoform.cc @@ -102,6 +102,12 @@ namespace spot result_ = unop::instance(negated_ ? unop::F : unop::G, recurse(f)); return; + + case unop::Finish: + result_ = unop::instance(unop::Finish, recurse_(f, false)); + if (negated_) + result_ = unop::instance(unop::Not, result_); + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 96734a46a..ae5915a7e 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -97,6 +97,10 @@ namespace spot || !is_universal(result_)) result_ = unop::instance(unop::G, result_); return; + + case unop::Finish: + result_ = unop::instance(unop::Finish, result_); + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index ba3a6eb55..7fc7bdf7f 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -241,6 +241,8 @@ namespace spot if (syntactic_implication(f, constant::false_instance())) result_ = true; return; + case unop::Finish: + return; } /* Unreachable code. */ assert(0); @@ -431,6 +433,8 @@ namespace spot destroy(tmp); return; } + case unop::Finish: + return; } /* Unreachable code. */ assert(0); diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index 1987ee57b..bca593eec 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -144,6 +144,10 @@ namespace spot case unop::G: os_ << "G"; break; + case unop::Finish: + os_ << "finish"; + need_parent = true; + break; } top_level_ = false; @@ -297,6 +301,10 @@ namespace spot case unop::G: os_ << "[]"; break; + case unop::Finish: + os_ << "finish"; + need_parent = true; + break; } top_level_ = false; diff --git a/src/ltlvisit/tunabbrev.cc b/src/ltlvisit/tunabbrev.cc index 7d372148e..f778ccdcd 100644 --- a/src/ltlvisit/tunabbrev.cc +++ b/src/ltlvisit/tunabbrev.cc @@ -39,6 +39,7 @@ namespace spot { switch (uo->op()) { + case unop::Finish: case unop::X: case unop::Not: this->super::visit(uo); diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index ab7c9940d..c4e70d237 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -72,6 +72,7 @@ namespace spot { switch (node->op()) { + case unop::Finish: case unop::F: case unop::G: case unop::X: diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index 0bd3781fe..2f0bcf19e 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -21,6 +21,7 @@ #include "ltlast/visitor.hh" #include "ltlast/allnodes.hh" +#include "ltlast/formula_tree.hh" #include "ltlvisit/lunabbrev.hh" #include "ltlvisit/nenoform.hh" #include "ltlvisit/destroy.hh" @@ -40,7 +41,7 @@ namespace spot { public: eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) - : fact_(fact), root_(root) + : fact_(fact), root_(root), finish_() { } @@ -87,6 +88,18 @@ namespace spot res_ = bdd_not(recurse(node->child())); return; } + case unop::Finish: + { + // Ensure finish_[node->child()] has been computed if + // node->child() is an automaton operator. + bdd f = recurse(node->child()); + finish_map_::const_iterator it = finish_.find(node->child()); + if (it == finish_.end()) + res_ = f; + else + res_ = finish_[node->child()]; + return; + } case unop::X: case unop::F: case unop::G: @@ -149,12 +162,23 @@ namespace spot } void - visit (const automatop* node) + visit(const automatop* node) { nmap m; + bdd finish = bddfalse; bdd acc = bddtrue; + + std::vector v; + for (unsigned i = 0; i < node->size(); ++i) + v.push_back(const_cast(node->nth(i))); + std::pair vp = - recurse_state(node, node->nfa()->get_init_state(), m, acc); + recurse_state(node->nfa(), + node->nfa()->get_init_state(), v, m, acc, finish); + + // Update finish_ with finish(node). + // FIXME: when node is loop, it does not make sense; hence the bddtrue. + finish_[node] = !node->nfa()->is_loop() ? bddtrue : finish; bdd tmp = bddtrue; for (nmap::iterator it = m.begin(); it != m.end(); ++it) @@ -180,15 +204,22 @@ namespace spot tgba_bdd_concrete_factory& fact_; bool root_; + /// BDD associated to each automatop A representing finish(A). + typedef Sgi::hash_map finish_map_; + + finish_map_ finish_; + // Table containing the two now variables associated with each state. // TODO: a little documentation about that. typedef Sgi::hash_map< const nfa::state*, std::pair, ptr_hash > nmap; std::pair& - recurse_state(const automatop* n, const nfa::state* s, nmap& m, bdd& acc) + recurse_state(const nfa::ptr& nfa, const nfa::state* s, + const std::vector& v, + nmap& m, bdd& acc, bdd& finish) { - const nfa::ptr nfa = n->nfa(); bool is_loop = nfa->is_loop(); nmap::iterator it; it = m.find(s); @@ -209,16 +240,18 @@ namespace spot bdd tmpacc = bddfalse; for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i) { - bdd f = (*i)->label == -1 ? bddtrue : recurse(n->nth((*i)->label)); + bdd f = recurse(formula_tree::instanciate((*i)->lbl, v)); if (nfa->is_final((*i)->dst)) { tmp1 |= f; tmp2 |= f; tmpacc |= f; + finish |= bdd_ithvar(v1) & f; } else { - std::pair vp = recurse_state(n, (*i)->dst, m, acc); + std::pair vp = + recurse_state(nfa, (*i)->dst, v, m, acc, finish); tmp1 |= (f & bdd_ithvar(vp.first + 1)); tmp2 |= (f & bdd_ithvar(vp.second + 1)); if (is_loop) diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index b4b1652f7..5562cc2a1 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -358,6 +358,8 @@ namespace spot res_ = bdd_ithvar(x); return; } + case unop::Finish: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index f35ee65ad..4e00732b0 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -146,6 +146,8 @@ namespace spot res_ = next; return; } + case unop::Finish: + assert(!"unsupported operator"); } /* Unreachable code. */ assert(0); diff --git a/src/tgbatest/eltl2tgba.test b/src/tgbatest/eltl2tgba.test index b9212be25..d1d0b71e9 100755 --- a/src/tgbatest/eltl2tgba.test +++ b/src/tgbatest/eltl2tgba.test @@ -145,3 +145,37 @@ T(f) EOF check_construct input + +cat >input <input <