Correct LaCIM for ELTL and make it work with LBTT.

* src/eltlparse/eltlparse.yy: Adjust.
* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc: Clean the way we
handle the negation of automaton operators.
* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Add an
optional argument to output a fully parenthesized string.
* src/tgbaalgos/eltl2tgba_lacim.cc: Fix it.
* src/tgbatest/eltl2tgba.cc: Add a new option (-L) to read formulae
from an LBTT-compatible file.
* src/tgbatest/eltl2tgba.test: A new tests.
* src/tgbatest/spotlbtt.test: Add LaCIM for ELTL.

ChangeLog

@@ -1,3 +1,19 @@
+2009-04-08  Damien Lefortier <dam@lrde.epita.fr>
+
+	Correct LaCIM for ELTL and make it work with LBTT.
+
+	* src/eltlparse/eltlparse.yy: Adjust.
+	* src/ltlast/automatop.cc, src/ltlast/automatop.hh,
+	src/ltlvisit/clone.cc, src/ltlvisit/nenoform.cc: Clean the way we
+	handle the negation of automaton operators.
+	* src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh: Add an
+	optional argument to output a fully parenthesized string.
+	* src/tgbaalgos/eltl2tgba_lacim.cc: Fix it.
+	* src/tgbatest/eltl2tgba.cc: Add a new option (-L) to read formulae
+	from an LBTT-compatible file.
+	* src/tgbatest/eltl2tgba.test: A new tests.
+	* src/tgbatest/spotlbtt.test: Add LaCIM for ELTL.
+
 2009-04-04  Damien Lefortier <dam@lrde.epita.fr>
 
 	Extend the ELTL parser to support basic aliases of automaton

src/eltlparse/eltlparse.yy

@@ -59,13 +59,20 @@ namespace spot
     {
       alias_ptr s;
     };
-    enum type { Xor, Implies, Equiv, Or, And };
     struct alias_binary : alias
     {
-      type ty;
+      virtual ~alias_binary() = 0; // Should not be instanciate
       alias_ptr lhs;
       alias_ptr rhs;
     };
+    struct alias_binop : alias_binary
+    {
+      binop::type ty;
+    };
+    struct alias_multop : alias_binary
+    {
+      multop::type ty;
+    };
     struct alias_nfa : alias
     {
       nfa::ptr nfa;
@@ -100,9 +107,18 @@ namespace spot
 	std::list<alias_ptr>::const_iterator i = a->s.begin();
 	while (i != a->s.end())
 	  va->push_back(alias2formula(*i++, v));
-	return automatop::instance(a->nfa, va);
+	return automatop::instance(a->nfa, va, false);
       }
-      /// TODO.
+      if (alias_binop* a = dynamic_cast<alias_binop*>(ap.get()))
+	return binop::instance(a->ty,
+			       alias2formula(a->lhs, v),
+			       alias2formula(a->rhs, v));
+      if (alias_multop* a = dynamic_cast<alias_multop*>(ap.get()))
+	return multop::instance(a->ty,
+			       alias2formula(a->lhs, v),
+			       alias2formula(a->rhs, v));
+
+      /* Unreachable code.  */
       assert(0);
     }
 
@@ -122,9 +138,15 @@ namespace spot
 	  res = std::max(arity(*i++), res);
 	return res;
       }
-      /// TODO.
+      if (alias_binary* a = dynamic_cast<alias_binary*>(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.
   }
 }
 
@@ -268,6 +290,17 @@ nfa: IDENT "=" "(" nfa_def ")"
         }
    | IDENT "=" nfa_alias
         {
+	  /// Recursivity issues of aliases are handled by a parse error.
+	  aliasmap::iterator i = amap.find(*$1);
+	  if (i != amap.end())
+	  {
+	    std::string s = "`";
+	    s += *$1;
+	    s += "' is already aliased";
+	    PARSE_ERROR(@1, s);
+	    delete $1;
+	    YYERROR;
+	  }
 	  amap[*$1] = alias_ptr($3);
    	  delete $1;
    	}
@@ -305,13 +338,17 @@ nfa_alias: IDENT "(" nfa_alias_arg_list ")"
 	  }
 	  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;
 	}
-	// TODO: more complicated aliases like | IDENT "(" nfa_alias ")"
 
 nfa_alias_arg_list: nfa_alias_arg
 	{
@@ -337,7 +374,7 @@ nfa_alias_arg: nfa_arg
 	  a->s = alias_ptr($2);
 	  $$ = a;
 	}
-	// TODO
+	// TODO: factoring with nfa_alias
 
 nfa_arg: ARG
 	{
@@ -394,7 +431,7 @@ subformula: ATOMIC_PROP
 	    automatop::vec* v = new automatop::vec;
 	    v->push_back($1);
 	    v->push_back($3);
-	    $$ = automatop::instance(np, v);
+	    $$ = automatop::instance(np, v, false);
 	  }
 	  delete $2;
 	}
@@ -413,7 +450,7 @@ subformula: ATOMIC_PROP
 	    nfa::ptr np = nmap[*$1];
 
 	    CHECK_ARITY(@1, $1, $3->size(), np->arity());
-	    $$ = automatop::instance(np, $3);
+	    $$ = automatop::instance(np, $3, false);
 	  }
 	  delete $1;
 	}

src/ltlast/automatop.cc

@@ -27,10 +27,11 @@ namespace spot
 {
   namespace ltl
   {
-    automatop::automatop(const nfa::ptr nfa, vec* v)
+    automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
-      : negated_(false), nfa_(nfa), children_(v)
+      : nfa_(nfa), children_(v), negated_(negated)
     {
-      dump_= nfa->get_name();
+      dump_ = negated ? "!" : "";
+      dump_ += nfa->get_name();
       dump_ += "(";
       dump_ += (*v)[0]->dump();
       for (unsigned n = 1; n < v->size(); ++n)
@@ -42,7 +43,7 @@ namespace spot
     automatop::~automatop()
     {
       // Get this instance out of the instance map.
-      pair p(nfa(), children_);
+      triplet p(std::make_pair(nfa(), negated_), children_);
       map::iterator i = instances.find(p);
       assert (i != instances.end());
       instances.erase(i);
@@ -65,17 +66,17 @@ namespace spot
     automatop::map automatop::instances;
 
     automatop*
-    automatop::instance(const nfa::ptr nfa, vec* v)
+    automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
     {
       assert(nfa != 0);
-      pair p(nfa, v);
+      triplet p(std::make_pair(nfa, negated), v);
       map::iterator i = instances.find(p);
       if (i != instances.end())
 	{
 	  delete v;
 	  return static_cast<automatop*>(i->second->ref());
 	}
-      automatop* res = new automatop(nfa, v);
+      automatop* res = new automatop(nfa, v, negated);
       instances[p] = res;
       return static_cast<automatop*>(res->ref());
     }
@@ -104,5 +105,11 @@ namespace spot
       assert(nfa_ != 0);
       return nfa_;
     }
+
+    bool
+    automatop::is_negated() const
+    {
+      return negated_;
+    }
   }
 }

src/ltlast/automatop.hh

@@ -49,7 +49,7 @@ namespace spot
       /// (especially not destroy it) after it has been passed to
       /// spot::ltl::automatop.
       static automatop*
-      instance(const nfa::ptr nfa, vec* v);
+      instance(const nfa::ptr nfa, vec* v, bool negated);
 
       virtual void accept(visitor& v);
       virtual void accept(const_visitor& v) const;
@@ -68,29 +68,33 @@ namespace spot
       /// Get the NFA of this operator.
       const nfa::ptr nfa() const;
 
-      bool negated_;
+      bool is_negated() const;
+
     protected:
-      typedef std::pair<nfa::ptr, vec*> pair;
+      typedef std::pair<std::pair<nfa::ptr, bool>, vec*> triplet;
       /// Comparison functor used internally by ltl::automatop.
       struct paircmp
       {
 	bool
-	operator () (const pair& p1, const pair& p2) const
+	operator () (const triplet& p1, const triplet& p2) const
 	{
-	  if (p1.first != p2.first)
+	  if (p1.first.first != p2.first.first)
-	    return p1.first < p2.first;
+	    return p1.first.first < p2.first.first;
+	  if (p1.first.second != p2.first.second)
+	    return p1.first.second < p2.first.second;
 	  return *p1.second < *p2.second;
 	}
       };
-      typedef std::map<pair, formula*, paircmp> map;
+      typedef std::map<triplet, formula*, paircmp> map;
       static map instances;
 
-      automatop(const nfa::ptr nfa, vec* v);
+      automatop(const nfa::ptr nfa, vec* v, bool negated);
       virtual ~automatop();
 
     private:
       nfa::ptr nfa_;
       vec* children_;
+      bool negated_;
     };
   }
 }

src/ltlvisit/clone.cc

@@ -71,7 +71,7 @@ namespace spot
       automatop::vec* res = new automatop::vec;
       for (unsigned i = 0; i < ao->size(); ++i)
         res->push_back(recurse(ao->nth(i)));
-      result_ = automatop::instance(ao->nfa(), res);
+      result_ = automatop::instance(ao->nfa(), res, ao->is_negated());
     }
 
     void

src/ltlvisit/nenoform.cc

@@ -154,16 +154,13 @@ namespace spot
 	void
 	visit(automatop* ao)
 	{
-	  if (negated_)
+	  bool negated = negated_;
-	  {
+	  negated_ = false;
-	    negated_ = false;
-	    ao->negated_ = true;
-	  }
 	  automatop::vec* res = new automatop::vec;
 	  unsigned aos = ao->size();
 	  for (unsigned i = 0; i < aos; ++i)
 	    res->push_back(recurse(ao->nth(i)));
-	  result_ = automatop::instance(ao->nfa(), res);
+	  result_ = automatop::instance(ao->nfa(), res, negated);
 	}
 
 	void

src/ltlvisit/tostring.cc

@@ -59,8 +59,8 @@ namespace spot
       class to_string_visitor: public const_visitor
       {
       public:
-	to_string_visitor(std::ostream& os)
+	to_string_visitor(std::ostream& os, bool full_parent = false)
-	  : os_(os), top_level_(true)
+	  : os_(os), top_level_(true), full_parent_(full_parent)
 	{
 	}
 
@@ -147,17 +147,18 @@ namespace spot
 	    }
 
 	  top_level_ = false;
-	  if (need_parent)
+	  if (need_parent || full_parent_)
 	    os_ << "(";
 	  uo->child()->accept(*this);
-	  if (need_parent)
+	  if (need_parent || full_parent_)
 	    os_ << ")";
 	}
 
 	void
 	visit(const automatop* ao)
 	{
-	  // Warning: this string isn't parsable.
+	  // Warning: this string isn't parsable because the automaton
+	  // operators used may not be defined.
 	  bool top_level = top_level_;
 	  top_level_ = false;
 	  if (!top_level)
@@ -206,6 +207,7 @@ namespace spot
       protected:
 	std::ostream& os_;
 	bool top_level_;
+	bool full_parent_;
       };
 
       class to_spin_string_visitor : public to_string_visitor
@@ -308,7 +310,8 @@ namespace spot
 	void
 	visit(const automatop* ao)
 	{
-	  // Warning: this string isn't parsable.
+	  // Warning: this string isn't parsable because the automaton
+	  // operators used may not be defined.
 	  bool top_level = top_level_;
 	  top_level_ = false;
 	  if (!top_level)
@@ -359,18 +362,18 @@ namespace spot
     } // anonymous
 
     std::ostream&
-    to_string(const formula* f, std::ostream& os)
+    to_string(const formula* f, std::ostream& os, bool full_parent)
     {
-      to_string_visitor v(os);
+      to_string_visitor v(os, full_parent);
       f->accept(v);
       return os;
     }
 
     std::string
-    to_string(const formula* f)
+    to_string(const formula* f, bool full_parent)
     {
       std::ostringstream os;
-      to_string(f, os);
+      to_string(f, os, full_parent);
       return os.str();
     }
 

src/ltlvisit/tostring.hh

@@ -32,14 +32,22 @@ namespace spot
     /// \addtogroup ltl_io
     /// @{
 
-    /// \brief Output a formula as a (parsable) string.
+    /// \brief Output a formula as a string which is parsable unless the formula
+    /// contains automaton operators (used in ELTL formulae).
     /// \param f The formula to translate.
     /// \param os The stream where it should be output.
-    std::ostream& to_string(const formula* f, std::ostream& os);
+    /// \param full_parent Whether or not the string should by fully
+    ///	                   parenthesized.
+    std::ostream&
+    to_string(const formula* f, std::ostream& os, bool full_parent = false);
 
-    /// \brief Convert a formula into a (parsable) string.
+    /// \brief Output a formula as a string which is parsable unless the formula
+    /// contains automaton operators (used in ELTL formulae).
     /// \param f The formula to translate.
-    std::string to_string(const formula* f);
+    /// \param full_parent Whether or not the string should by fully
+    ///	                   parenthesized.
+    std::string
+    to_string(const formula* f, bool full_parent = false);
 
     /// \brief Output a formula as a (parsable by Spin) string.
     /// \param f The formula to translate.

src/tgbaalgos/eltl2tgba_lacim.cc

@@ -145,9 +145,7 @@ namespace spot
 	assert(op != -1);
 	unsigned s = node->size();
 	for (unsigned n = 0; n < s; ++n)
-	  {
+	  res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
-	    res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
-	  }
       }
 
       void
@@ -164,11 +162,9 @@ namespace spot
 			   bdd_ithvar(it->second.second + 1), bddop_biimp);
 	fact_.constrain_relation(bdd_apply(acc, tmp, bddop_imp));
 
-	if (!node->nfa()->is_loop())
+	fact_.declare_acceptance_condition(acc, node);
-	  fact_.declare_acceptance_condition(acc, node);
+	res_ = node->is_negated() ?
-
+	  bdd_nithvar(vp.first) : bdd_ithvar(vp.first);
-	bdd init = bdd_ithvar(vp.first);
-	res_ = node->negated_ ? bdd_not(init) : init;
       }
 
       bdd
@@ -193,6 +189,7 @@ namespace spot
       recurse_state(const automatop* n, const nfa::state* s, nmap& m, bdd& acc)
       {
 	const nfa::ptr nfa = n->nfa();
+	bool is_loop = nfa->is_loop();
 	nmap::iterator it;
 	it = m.find(s);
 
@@ -209,8 +206,7 @@ namespace spot
 
 	bdd tmp1 = bddfalse;
 	bdd tmp2 = bddfalse;
-	bdd tmpacc = !bdd_ithvar(v2);
+	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));
@@ -225,13 +221,22 @@ namespace spot
 	    std::pair<int, int> vp = recurse_state(n, (*i)->dst, m, acc);
 	    tmp1 |= (f & bdd_ithvar(vp.first + 1));
 	    tmp2 |= (f & bdd_ithvar(vp.second + 1));
+	    if (is_loop)
+	      tmpacc |= f;
 	  }
 	}
-	acc &= tmpacc;
 	fact_.constrain_relation(bdd_apply(bdd_ithvar(v1), tmp1, bddop_biimp));
-	fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp));
+	if (is_loop)
-	fact_.constrain_relation(
+	{
-	  bdd_apply(bdd_ithvar(v2), bdd_ithvar(v1), bddop_imp));
+	  fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_invimp));
+	  acc &= bdd_ithvar(v2) | !tmpacc;
+	}
+	else
+	{
+	  fact_.constrain_relation(bdd_apply(bdd_ithvar(v2), tmp2, bddop_imp));
+	  acc &= bdd_nithvar(v2) | tmpacc;
+	}
+
 	return m[s];
       }
     };

src/tgbatest/eltl2tgba.cc

@@ -24,20 +24,26 @@
 #include <fstream>
 #include <cassert>
 #include <cstring>
+#include "ltlparse/public.hh"
 #include "eltlparse/public.hh"
 #include "tgbaalgos/eltl2tgba_lacim.hh"
 #include "tgbaalgos/dotty.hh"
+#include "tgbaalgos/lbtt.hh"
 #include "tgbaalgos/save.hh"
 #include "ltlvisit/destroy.hh"
+#include "ltlvisit/tostring.hh"
 
 void
 syntax(char* prog)
 {
-  std::cerr << "Usage: "<< prog << " [OPTIONS...] formula [file]" << std::endl
+  std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl
-	    << "       "<< prog << " -F [OPTIONS...] file [file]" << std::endl
+	    << "       " << prog << " -F [OPTIONS...] file [file]" << std::endl
+	    << "       " << prog << " -L [OPTIONS...] file [file]" << std::endl
 	    << std::endl
 	    << "Options:" << std::endl
 	    << "  -F    read the formula from the file (extended input format)"
+	    << std::endl
+	    << "  -L    read the formula from an LBTT-compatible file"
 	    << std::endl;
 }
 
@@ -76,11 +82,28 @@ main(int argc, char** argv)
     f = spot::eltl::parse_file(argv[2], p, env, false);
     formula_index = 2;
   }
-  else
+  if (strcmp(argv[1], "-L") == 0)
+  {
+    std::string input;
+    std::ifstream ifs(argv[2]);
+    std::getline(ifs, input, '\0');
+
+    spot::ltl::parse_error_list p_;
+    f = spot::ltl::parse(input, p_, env, false);
+    input = ltl_defs();
+    input += "%";
+    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;
+  }
+  if (formula_index == 0)
   {
     std::stringstream oss;
     oss << ltl_defs() << "%" << argv[1];
-      f = spot::eltl::parse_string(oss.str(), p, env, false);
+    f = spot::eltl::parse_string(oss.str(), p, env, false);
     formula_index = 1;
   }
 
@@ -97,12 +120,17 @@ main(int argc, char** argv)
   spot::bdd_dict* dict = new spot::bdd_dict();
   spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict);
 
-  spot::dotty_reachable(std::cout, concrete);
+  if (strcmp(argv[1], "-L") == 0)
-  if (argc >= formula_index + 1)
+    spot::lbtt_reachable(std::cout, concrete);
+  else
   {
-    std::ofstream ofs(argv[formula_index + 1]);
+    spot::dotty_reachable(std::cout, concrete);
-    spot::tgba_save_reachable(ofs, concrete);
+    if (formula_index + 1 < argc)
-    ofs.close();
+    {
+      std::ofstream ofs(argv[formula_index + 1]);
+      spot::tgba_save_reachable(ofs, concrete);
+      ofs.close();
+    }
   }
 
   spot::ltl::destroy(f);

src/tgbatest/eltl2tgba.test

@@ -97,12 +97,12 @@ check_false '!XXa'
 cat >input <<EOF
 include input1
 %
-G(a)
+G(a|b&!c)
 EOF
 
 check_construct input
-check_true 'Ga'
+check_true 'G (a|b&!c)'
-check_false '!Ga'
+check_false '!G (a|b&!c)'
 
 cat >input <<EOF
 include input1

src/tgbatest/spotlbtt.test

@@ -60,6 +60,14 @@ Algorithm
    Enabled = no
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- LaCIM), eltl"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot './eltl2tgba -L'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- FM)"