* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ...

* src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh:
... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well.
* iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/tripprod.cc, wrap/python/spot.i,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py: Adjust.

src/tgbaalgos/ltl2tgba_lacim.cc

@@ -0,0 +1,254 @@
+#include "ltlast/visitor.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/nenoform.hh"
+#include "ltlvisit/destroy.hh"
+#include "tgba/tgbabddconcretefactory.hh"
+#include <cassert>
+
+#include "ltl2tgba_lacim.hh"
+
+namespace spot
+{
+  using namespace ltl;
+
+  /// \brief Recursively translate a formula into a BDD.
+  ///
+  /// The algorithm used here is adapted from Jean-Michel Couvreur's
+  /// Probataf tool.
+  class ltl_trad_visitor: public const_visitor
+  {
+  public:
+    ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
+      : fact_(fact), root_(root)
+    {
+    }
+
+    virtual
+    ~ltl_trad_visitor()
+    {
+    }
+
+    bdd
+    result()
+    {
+      return res_;
+    }
+
+    void
+    visit(const atomic_prop* node)
+    {
+      res_ = bdd_ithvar(fact_.create_atomic_prop(node));
+    }
+
+    void
+    visit(const constant* node)
+    {
+      switch (node->val())
+	{
+	case constant::True:
+	  res_ = bddtrue;
+	  return;
+	case constant::False:
+	  res_ = bddfalse;
+	  return;
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const unop* node)
+    {
+      switch (node->op())
+	{
+	case unop::F:
+	  {
+	    /*
+		   Fx  <=> x | XFx
+	       In other words:
+		   now <=> x | next
+	    */
+	    int v = fact_.create_state(node);
+	    bdd now = bdd_ithvar(v);
+	    bdd next = bdd_ithvar(v + 1);
+	    bdd x = recurse(node->child());
+	    fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp));
+	    /*
+	      `x | next', doesn't actually encode the fact that x
+	      should be fulfilled eventually.  We ensure this by
+	      creating a new generalized Büchi accepting set, Acc[x],
+	      and leave out of this set any transition going off NOW
+	      without checking X.  Such accepting conditions are
+	      checked for during the emptiness check.
+	    */
+	    fact_.declare_accepting_condition(x | !now, node->child());
+	    res_ = now;
+	    return;
+	  }
+	case unop::G:
+	  {
+	    bdd child = recurse(node->child());
+	    // If G occurs at the top of the formula we don't
+	    // need Now/Next variables.  We just constrain
+	    // the relation so that the child always happens.
+	    // This saves 2 BDD variables.
+	    if (root_)
+	      {
+		fact_.constrain_relation(child);
+		res_ = child;
+		return;
+	      }
+	    // Gx  <=>  x && XGx
+	    int v = fact_.create_state(node);
+	    bdd now = bdd_ithvar(v);
+	    bdd next = bdd_ithvar(v + 1);
+	    fact_.constrain_relation(bdd_apply(now, child & next,
+					       bddop_biimp));
+	    res_ = now;
+	    return;
+	  }
+	case unop::Not:
+	  {
+	    res_ = bdd_not(recurse(node->child()));
+	    return;
+	  }
+	case unop::X:
+	  {
+	    int v = fact_.create_state(node->child());
+	    bdd now = bdd_ithvar(v);
+	    bdd next = bdd_ithvar(v + 1);
+	    fact_.constrain_relation(bdd_apply(now, recurse(node->child()),
+					       bddop_biimp));
+	    res_ = next;
+	    return;
+	  }
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const binop* node)
+    {
+      bdd f1 = recurse(node->first());
+      bdd f2 = recurse(node->second());
+
+      switch (node->op())
+	{
+	case binop::Xor:
+	  res_ = bdd_apply(f1, f2, bddop_xor);
+	  return;
+	case binop::Implies:
+	  res_ = bdd_apply(f1, f2, bddop_imp);
+	  return;
+	case binop::Equiv:
+	  res_ = bdd_apply(f1, f2, bddop_biimp);
+	  return;
+	case binop::U:
+	  {
+	    /*
+	       f1 U f2 <=> f2 | (f1 & X(f1 U f2))
+	       In other words:
+		   now <=> f2 | (f1 & next)
+	    */
+	    int v = fact_.create_state(node);
+	    bdd now = bdd_ithvar(v);
+	    bdd next = bdd_ithvar(v + 1);
+	    fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next),
+					       bddop_biimp));
+	    /*
+	      The rightmost conjunction, f1 & next, doesn't actually
+	      encode the fact that f2 should be fulfilled eventually.
+	      We declare an accepting condition for this purpose (see
+	      the comment in the unop::F case).
+	    */
+	    fact_.declare_accepting_condition(f2 | !now, node->second());
+	    res_ = now;
+	    return;
+	  }
+	case binop::R:
+	  {
+	    /*
+	       f1 R f2 <=> f2 & (f1 | X(f1 U f2))
+	       In other words:
+		   now <=> f2 & (f1 | next)
+	    */
+	    int v = fact_.create_state(node);
+	    bdd now = bdd_ithvar(v);
+	    bdd next = bdd_ithvar(v + 1);
+	    fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next),
+					       bddop_biimp));
+	    res_ = now;
+	    return;
+	  }
+	}
+      /* Unreachable code.  */
+      assert(0);
+    }
+
+    void
+    visit(const multop* node)
+    {
+      int op = -1;
+      bool root = false;
+      switch (node->op())
+	{
+	case multop::And:
+	  op = bddop_and;
+	  res_ = bddtrue;
+	  // When the root formula is a conjunction it's ok to
+	  // consider all children as root formulae.  This allows the
+	  // root-G trick to save many more variable.  (See the
+	  // translation of G.)
+	  root = root_;
+	  break;
+	case multop::Or:
+	  op = bddop_or;
+	  res_ = bddfalse;
+	  break;
+	}
+      assert(op != -1);
+      unsigned s = node->size();
+      for (unsigned n = 0; n < s; ++n)
+	{
+	  res_ = bdd_apply(res_, recurse(node->nth(n), root), op);
+	}
+    }
+
+    bdd
+    recurse(const formula* f, bool root = false)
+    {
+      ltl_trad_visitor v(fact_, root);
+      f->accept(v);
+      return v.result();
+    }
+
+  private:
+    bdd res_;
+    tgba_bdd_concrete_factory& fact_;
+    bool root_;
+  };
+
+  tgba_bdd_concrete*
+  ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict)
+  {
+    // Normalize the formula.  We want all the negations on
+    // the atomic propositions.  We also suppress logic
+    // abbreviations such as <=>, =>, or XOR, since they
+    // would involve negations at the BDD level.
+    const ltl::formula* f1 = ltl::unabbreviate_logic(f);
+    const ltl::formula* f2 = ltl::negative_normal_form(f1);
+    ltl::destroy(f1);
+
+    // Traverse the formula and draft the automaton in a factory.
+    tgba_bdd_concrete_factory fact(dict);
+    ltl_trad_visitor v(fact, true);
+    f2->accept(v);
+    ltl::destroy(f2);
+    fact.finish();
+
+    // Finally setup the resulting automaton.
+    return new tgba_bdd_concrete(fact, v.result());
+  }
+}