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

@@ -1,3 +1,17 @@
+2009-04-18  Damien Lefortier <dam@lrde.epita.fr>
+
+	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  <sadegh@lrde.epita.fr>
 
 	Minor fixes to compile with GCC 4.4.

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;
+      multop::type op;
-    };
+      alias_ptr lhs;
-    struct alias_multop : alias_binary
+      alias_ptr rhs;
-    {
-      multop::type ty;
     };
     struct alias_nfa : alias
     {
+      std::vector<alias_ptr> children;
       spot::ltl::nfa::ptr nfa;
-      std::list<alias_ptr> 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<alias_not*>(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<alias_arg*>(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<alias_nfa*>(ap.get()))
       {
 	automatop::vec* va = new automatop::vec;
-	std::list<alias_ptr>::const_iterator i = a->s.begin();
+	std::vector<alias_ptr>::const_iterator i = a->children.begin();
-	while (i != a->s.end())
+	while (i != a->children.end())
 	  va->push_back(alias2formula(*i++, v));
 	return automatop::instance(a->nfa, va, false);
       }
       if (alias_binop* a = dynamic_cast<alias_binop*>(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<alias_multop*>(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<alias_not*>(ap.get()))
-	return arity(a->s);
+	return arity(a->child);
       if (alias_arg* a = dynamic_cast<alias_arg*>(ap.get()))
-	return a->i + 1;
+	return std::max(a->i + 1, 0);
       if (alias_nfa* a = dynamic_cast<alias_nfa*>(ap.get()))
       {
 	size_t res = 0;
-	std::list<alias_ptr>::const_iterator i = a->s.begin();
+	std::vector<alias_ptr>::const_iterator i = a->children.begin();
-	while (i != a->s.end())
+	while (i != a->children.end())
 	  res = std::max(arity(*i++), res);
 	return res;
       }
-      if (alias_binary* a = dynamic_cast<alias_binary*>(ap.get()))
+      if (alias_binop* a = dynamic_cast<alias_binop*>(ap.get()))
+	return std::max(arity(a->lhs), arity(a->rhs));
+      if (alias_multop* a = dynamic_cast<alias_multop*>(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.
+    /// Alias an existing alias, as in Strong=G(F($0))->G(F($1)),
-    /// TODO.
+    /// 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<alias_ptr> v)
+    {
+      if (alias_not* a = dynamic_cast<alias_not*>(ap.get()))
+      {
+	alias_not* res = new alias_not;
+	res->child = realias(a->child, v);
+	return alias_ptr(res);
+      }
+      if (alias_arg* a = dynamic_cast<alias_arg*>(ap.get())) // Do it.
+	return a->i < 0 ? ap : v.at(a->i);
+      if (alias_nfa* a = dynamic_cast<alias_nfa*>(ap.get()))
+      {
+	alias_nfa* res = new alias_nfa;
+	std::vector<alias_ptr>::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<alias_binop*>(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<alias_multop*>(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(),
+	    CHECK_ARITY(@1, $1, $3->children.size(), np->arity());
-                        static_cast<unsigned>(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;
+	  alias_not* res = new alias_not;
-	  a->s = alias_ptr($2);
+	  res->child = alias_ptr($2);
-	  $$ = a;
+	  $$ = 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 <pval> != <bval>.
+	{
+	  $$ = 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(),
+	    CHECK_ARITY(@1, $1, $3->size(), np->arity());
-                        static_cast<unsigned>(np->arity()));
 	    $$ = automatop::instance(np, $3, false);
 	  }
 	  delete $1;

src/eltlparse/eltlscan.ll

@@ -105,6 +105,9 @@ eol      \n|\r|\n\r|\r\n
 <INITIAL>[tT][rR][uU][eE] {
 			  return token::CONST_TRUE;
 			}
+<INITIAL>[fF][aA][lL][sS][eE] {
+			  return token::CONST_FALSE;
+			}
 
 <INITIAL>[a-zA-Z][a-zA-Z0-9_]* {
 			  yylval->sval = new std::string(yytext, yyleng);

src/eltltest/acc.cc

@@ -22,6 +22,9 @@
 #include <iostream>
 #include <cassert>
 #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;
 }

src/eltltest/acc.test

@@ -22,6 +22,18 @@ A(1,a,a|b)&X(!f)
 EOF
 run 0 ./acc input || exit 1
 
+cat >input <<EOF
+include prelude
+A=(
+    0 1 \$2
+    1 2 \$0
+    accept 0
+  )
+%
+A(1,a)
+EOF
+run 1 ./acc input || exit 1
+
 cat >input <<EOF
 X=(
     0 1 true

src/ltlast/nfa.cc

@@ -27,7 +27,7 @@ namespace spot
   namespace ltl
   {
     nfa::nfa()
-      : is_(), si_(), arity_(-1), name_(), init_(0), finals_()
+      : is_(), si_(), arity_(0), name_(), init_(0), finals_()
     {
     }
 
@@ -68,8 +68,8 @@ namespace spot
       t->dst = add_state(dst);
       t->label = label;
       s->push_back(t);
-      if (label > arity_)
+      if (label >= arity_)
-	arity_ = label;
+	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*

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.
       ///

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];

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;
   }

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 <<EOF
+include input1
+%
+Strong(a,b)
+EOF
+
+check_construct input
+check_true 'G(F(a))->G(F(b))'
+check_false '!(G(F(a))->G(F(b)))'
+
 cat >input <<EOF
 include input1
 %