diff --git a/ChangeLog b/ChangeLog index 8078ad1b0..6811eabe3 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2003-06-05 Alexandre Duret-Lutz + + * 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 * src/ltlparse/ltlparse.yy (result): Suppress unused definition. diff --git a/configure.ac b/configure.ac index 06e21d761..6d88cfebc 100644 --- a/configure.ac +++ b/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 ]) diff --git a/src/Makefile.am b/src/Makefile.am index b1937282d..836996887 100644 --- a/src/Makefile.am +++ b/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 = diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index c87fdbf2d..e6d5dc387 100644 --- a/src/tgba/Makefile.am +++ b/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 diff --git a/src/tgba/succiter.hh b/src/tgba/succiter.hh index 6d8643d76..22d6eaf64 100644 --- a/src/tgba/succiter.hh +++ b/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 diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc new file mode 100644 index 000000000..53d50f44a --- /dev/null +++ b/src/tgba/tgbaexplicit.cc @@ -0,0 +1,190 @@ +#include "ltlast/atomic_prop.hh" +#include "tgbaexplicit.hh" +#include + +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(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(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(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(s); + assert(se); + sn_map::const_iterator i = state_name_map_.find(se->get_state()); + assert(i != state_name_map_.end()); + return i->second; + } + +} diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh new file mode 100644 index 000000000..f5e7922c3 --- /dev/null +++ b/src/tgba/tgbaexplicit.hh @@ -0,0 +1,101 @@ +#ifndef SPOT_TGBA_TGBAEXPLICIT_HH +# define SPOT_TGBA_TGBAEXPLICIT_HH + +#include +#include +#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 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 ns_map; + typedef std::map 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 diff --git a/src/tgbatest/.cvsignore b/src/tgbatest/.cvsignore new file mode 100644 index 000000000..be7ec17d9 --- /dev/null +++ b/src/tgbatest/.cvsignore @@ -0,0 +1,6 @@ +.deps +Makefile +Makefile.in +defs +explicit +.libs diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am new file mode 100644 index 000000000..b0bf14f38 --- /dev/null +++ b/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 diff --git a/src/tgbatest/defs.in b/src/tgbatest/defs.in new file mode 100644 index 000000000..68de36ac3 --- /dev/null +++ b/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 diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc new file mode 100644 index 000000000..dd980a845 --- /dev/null +++ b/src/tgbatest/explicit.cc @@ -0,0 +1,26 @@ +#include +#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); +} diff --git a/src/tgbatest/explicit.test b/src/tgbatest/explicit.test new file mode 100755 index 000000000..999ce9ac6 --- /dev/null +++ b/src/tgbatest/explicit.test @@ -0,0 +1,25 @@ +#!/bin/sh + +. ./defs + +set -e + +./explicit > stdout + +cat >expected < 1 + 2 [label="state 1"] + 1 -> 2 [label="T\n"] + 3 [label="state 2"] + 2 -> 3 [label="\n"] + 3 -> 1 [label="\nT"] +} +EOF + +diff stdout expected + +rm stdout expected