* configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs.

* src/Makefile.am (SUBDIRS): Add tgbatest.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file.
* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc
and tgbaexplicit.hh.
* src/tgbatest/Makefile.am, src/tgbatest/defs.in,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.

ChangeLog

@@ -1,3 +1,13 @@
+2003-06-05  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
+
+	* configure.ac: Output src/tgbatest/Makefile and src/tgbatest/defs.
+	* src/Makefile.am (SUBDIRS): Add tgbatest.
+	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc: New file.
+	* src/tgba/Makefile.am (libtgba_la_SOURCES): Add tgbaexplicit.cc
+	and tgbaexplicit.hh.
+	* src/tgbatest/Makefile.am, src/tgbatest/defs.in, 
+	src/tgbatest/explicit.cc, src/tgbatest/explicit.test: New files.
+
 2003-06-04  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
 	* src/ltlparse/ltlparse.yy (result): Suppress unused definition.

configure.ac

@@ -33,6 +33,8 @@ AC_CONFIG_FILES([
   src/ltlvisit/Makefile
   src/tgba/Makefile
   src/tgbaalgos/Makefile
+  src/tgbatest/Makefile
+  src/tgbatest/defs
   src/misc/Makefile
   wrap/Makefile
 ])

src/Makefile.am

@@ -1,9 +1,9 @@
 AUTOMAKE_OPTIONS = subdir-objects
 
-# List directories in the order they must be built.  
+# List directories in the order they must be built.
 # Keep tests at the end.
 SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse tgba tgbaalgos . \
-	  ltltest
+	  ltltest tgbatest
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =

src/tgba/Makefile.am

@@ -35,4 +35,6 @@ libtgba_la_SOURCES = \
   tgbabddtranslatefactory.cc \
   tgbabddtranslatefactory.hh \
   tgbabddtranslateproxy.cc \
-  tgbabddtranslateproxy.hh
+  tgbabddtranslateproxy.hh \
+  tgbaexplicit.cc \
+  tgbaexplicit.hh

src/tgba/succiter.hh

@@ -27,7 +27,7 @@ namespace spot
     /// \brief Position the iterator on the first successor (if any).
     ///
     /// This method can be called several times to make multiple
-    /// passes over successors.  
+    /// passes over successors.
     ///
     /// \warning One should always call \c done() to
     /// ensure there is a successor, even after \c first().  A

src/tgba/tgbaexplicit.cc

@@ -0,0 +1,190 @@
+#include "ltlast/atomic_prop.hh"
+#include "tgbaexplicit.hh"
+#include <cassert>
+
+namespace spot
+{
+
+  ////////////////////////////////////////
+  // tgba_explicit_succ_iterator
+
+  tgba_explicit_succ_iterator::tgba_explicit_succ_iterator
+  (const tgba_explicit::state* s)
+    : s_(s)
+  {
+  }
+
+  void 
+  tgba_explicit_succ_iterator::first()
+  {
+    i_ = s_->begin();
+  }
+
+  void 
+  tgba_explicit_succ_iterator::next()
+  {
+    ++i_;
+  }
+
+  bool 
+  tgba_explicit_succ_iterator::done()
+  {
+    return i_ == s_->end();
+  }
+
+  state_explicit* 
+  tgba_explicit_succ_iterator::current_state()
+  {
+    return new state_explicit((*i_)->dest);
+  }
+
+  bdd 
+  tgba_explicit_succ_iterator::current_condition()
+  {
+    return (*i_)->condition;
+  }
+
+  bdd 
+  tgba_explicit_succ_iterator::current_promise()
+  {
+    return (*i_)->promise;
+  }
+
+
+  ////////////////////////////////////////
+  // state_explicit
+
+  const tgba_explicit::state* 
+  state_explicit::get_state() const
+  {
+    return state_;
+  }
+
+  int
+  state_explicit::compare(const spot::state* other) const
+  {
+    const state_explicit* o = dynamic_cast<const state_explicit*>(other);
+    assert(o);
+    return o->get_state() - get_state();
+  }
+
+  ////////////////////////////////////////
+  // tgba_explicit
+
+
+  tgba_explicit::tgba_explicit()
+    : init_(0)
+  {
+  }
+
+  tgba_explicit::~tgba_explicit()
+  {
+    ns_map::iterator i;
+    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+      {
+	tgba_explicit::state::iterator i2;
+	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	  delete *i2;
+	delete i->second;
+      }
+  }
+  
+  tgba_explicit::state*
+  tgba_explicit::add_state(const std::string& name)
+  {
+    ns_map::iterator i = name_state_map_.find(name);
+    if (i == name_state_map_.end())
+      {
+	tgba_explicit::state* s = new tgba_explicit::state;
+	name_state_map_[name] = s;
+	state_name_map_[s] = name;
+
+	// The first state we add is the inititial state.
+	if (! init_)
+	  init_ = s;
+
+	return s;
+      }
+    return i->second;
+  }
+
+  tgba_explicit::transition*
+  tgba_explicit::create_transition(const std::string& source, 
+				   const std::string& dest)
+  {
+    tgba_explicit::state* s = add_state(source);
+    tgba_explicit::state* d = add_state(dest);
+    transition* t = new transition;
+    t->dest = d;
+    t->condition = bddtrue;
+    t->promise = bddtrue;
+    s->push_back(t);
+    return t;
+  }
+
+  void tgba_explicit::add_condition(transition* t, ltl::formula* f)
+  {
+    assert(dynamic_cast<ltl::atomic_prop*>(f));
+    tgba_bdd_dict::fv_map::iterator i = dict_.var_map.find(f);
+    int v;
+    if (i == dict_.var_map.end())
+      {
+	v = create_node();
+	dict_.var_map[f] = v;
+	dict_.var_formula_map[v] = f;
+      }
+    else
+      {
+	v = i->second;
+      }
+    t->condition &= ithvar(v);
+  }
+
+  void tgba_explicit::add_promise(transition* t, ltl::formula* f)
+  {
+    tgba_bdd_dict::fv_map::iterator i = dict_.prom_map.find(f);
+    int v;
+    if (i == dict_.prom_map.end())
+      {
+	v = create_node();
+	dict_.prom_map[f] = v;
+	dict_.prom_formula_map[v] = f;
+      }
+    else
+      {
+	v = i->second;
+      }
+    t->promise &= ithvar(v);
+  }
+
+  state* 
+  tgba_explicit::get_init_state() const
+  {
+    return new state_explicit(init_);
+  }
+
+  tgba_succ_iterator* 
+  tgba_explicit::succ_iter(const spot::state* state) const
+  {
+    const state_explicit* s = dynamic_cast<const state_explicit*>(state);
+    assert(s);
+    return new tgba_explicit_succ_iterator(s->get_state());
+  }
+    
+  const tgba_bdd_dict& 
+  tgba_explicit::get_dict() const
+  {
+    return dict_;
+  }
+
+  std::string 
+  tgba_explicit::format_state(const spot::state* s) const
+  {
+    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
+    assert(se);
+    sn_map::const_iterator i = state_name_map_.find(se->get_state());
+    assert(i != state_name_map_.end());
+    return i->second;
+  }
+
+}

src/tgba/tgbaexplicit.hh

@@ -0,0 +1,101 @@
+#ifndef SPOT_TGBA_TGBAEXPLICIT_HH
+# define SPOT_TGBA_TGBAEXPLICIT_HH
+
+#include <list>
+#include <map>
+#include "tgba.hh"
+#include "ltlast/formula.hh"
+#include "bddfactory.hh"
+
+namespace spot
+{
+  // Forward declarations.  See below.
+  class state_explicit;
+  class tgba_explicit_succ_iterator;
+
+  /// Explicit representation of a spot::tgba.
+  class tgba_explicit : public tgba, public bdd_factory
+  {
+  public:
+    tgba_explicit();
+
+    struct transition;
+    typedef std::list<transition*> state;
+    struct transition
+    {
+      bdd condition;
+      bdd promise;
+      state* dest;
+    };
+
+    transition*
+    create_transition(const std::string& source, const std::string& dest);
+
+    void add_condition(transition* t, ltl::formula* f);
+    void add_promise(transition* t, ltl::formula* f);
+
+    // tgba interface
+    virtual ~tgba_explicit();
+    virtual spot::state* get_init_state() const;
+    virtual tgba_succ_iterator*
+    succ_iter(const spot::state* state) const;
+    virtual const tgba_bdd_dict& get_dict() const;
+    virtual std::string format_state(const spot::state* state) const;
+
+  protected:
+    state* add_state(const std::string& name);
+    typedef std::map<const std::string, tgba_explicit::state*> ns_map;
+    typedef std::map<const tgba_explicit::state*, std::string> sn_map;
+    ns_map name_state_map_;
+    sn_map state_name_map_;
+    tgba_bdd_dict dict_;
+    tgba_explicit::state* init_;
+  };
+
+
+  class state_explicit : public spot::state
+  {
+  public:
+    state_explicit(const tgba_explicit::state* s)
+      : state_(s)
+    {
+    }
+
+    virtual int compare(const spot::state* other) const;
+
+    virtual ~state_explicit()
+    {
+    }
+
+    const tgba_explicit::state* get_state() const;
+  private:
+    const tgba_explicit::state* state_;
+  };
+
+
+  class tgba_explicit_succ_iterator : public tgba_succ_iterator
+  {
+  public:
+    tgba_explicit_succ_iterator(const tgba_explicit::state* s);
+
+    virtual
+    ~tgba_explicit_succ_iterator()
+    {
+    }
+
+    virtual void first();
+    virtual void next();
+    virtual bool done();
+
+    virtual state_explicit* current_state();
+    virtual bdd current_condition();
+    virtual bdd current_promise();
+
+  private:
+    const tgba_explicit::state* s_;
+    tgba_explicit::state::const_iterator i_;
+  };
+
+}
+
+#endif // SPOT_TGBA_TGBAEXPLICIT_HH

src/tgbatest/.cvsignore

@@ -0,0 +1,6 @@
+.deps
+Makefile
+Makefile.in
+defs
+explicit
+.libs

src/tgbatest/Makefile.am

@@ -0,0 +1,16 @@
+AM_CPPFLAGS = -I$(srcdir)/..
+LDADD = ../libspot.la
+
+check_SCRIPTS = defs
+# Keep this sorted alphabetically.
+check_PROGRAMS = \
+  explicit
+
+explicit_SOURCES = explicit.cc
+
+TESTS = \
+  explicit.test
+
+EXTRA_DIST = $(TESTS)
+
+CLEANFILES = stdout expected

src/tgbatest/defs.in

@@ -0,0 +1,35 @@
+# -*- shell-script -*-
+
+# Ensure we are running from the right directory.
+test -f ./defs || {
+   echo "defs: not found in current directory" 1>&2
+   exit 1
+}
+
+# If srcdir is not set, then we are not running from `make check', be verbose.
+if test -z "$srcdir"; then
+   test -z "$VERBOSE" && VERBOSE=x
+   # compute $srcdir.
+   srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
+   test $srcdir = $0 && srcdir=.
+fi
+
+# Ensure $srcdir is set correctly.
+test -f $srcdir/defs.in || {
+   echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
+   exit 1
+}
+
+# User can set VERBOSE to see all output.
+test -z "$VERBOSE" && exec >/dev/null 2>&1
+
+echo "== Running test $0"
+
+DOT='@DOT@'
+
+# Turn on shell traces when VERBOSE=x.
+if test "x$VERBOSE" = xx; then
+  set -x
+else
+  :
+fi

src/tgbatest/explicit.cc

@@ -0,0 +1,26 @@
+#include <iostream>
+#include "ltlenv/defaultenv.hh"
+#include "tgba/tgbaexplicit.hh"
+#include "tgbaalgos/dotty.hh"
+
+int
+main()
+{
+  spot::ltl::default_environment& e = 
+    spot::ltl::default_environment::instance();
+  spot::tgba_explicit a;
+  
+  typedef spot::tgba_explicit::transition trans;
+
+  trans* t1 = a.create_transition("state 0", "state 1");
+  trans* t2 = a.create_transition("state 1", "state 2");
+  trans* t3 = a.create_transition("state 2", "state 0");
+  a.add_condition(t2, e.require("a"));
+  a.add_condition(t3, e.require("b"));
+  a.add_condition(t3, e.require("c"));
+  a.add_promise(t1, e.require("p"));
+  a.add_promise(t1, e.require("q"));
+  a.add_promise(t2, e.require("r"));
+
+  spot::dotty_reachable(std::cout, a);
+}

src/tgbatest/explicit.test

@@ -0,0 +1,25 @@
+#!/bin/sh
+
+. ./defs
+
+set -e
+
+./explicit > stdout
+
+cat >expected <<EOF
+digraph G {
+  size="7.26,10.69"
+  0 [label="", style=invis]
+  1 [label="state 0"]
+  0 -> 1
+  2 [label="state 1"]
+  1 -> 2 [label="T\n<Prom[p]:1, Prom[q]:1>"]
+  3 [label="state 2"]
+  2 -> 3 [label="<a:1>\n<Prom[r]:1>"]
+  3 -> 1 [label="<b:1, c:1>\nT"]
+}
+EOF
+
+diff stdout expected
+
+rm stdout expected