diff --git a/ChangeLog b/ChangeLog index 402614fd3..e78f128fd 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,25 @@ 2004-10-22 Alexandre Duret-Lutz + Preliminary support for Event-based GBA. + * src/evtgba/Makefile.am, src/evtgba/evtgba.cc, + src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh, + src/evtgba/explicit.cc, src/evtgba/explicit.hh, + src/evtgba/product.cc, src/evtgba/product.hh, + src/evtgba/symbol.cc, src/evtgba/symbol.hh, + src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc, + src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc, + src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc, + src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am, + src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, + src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh, + src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am, + src/evtgbatest/defs.in, src/evtgbatest/explicit.cc, + src/evtgbatest/explicit.test, src/evtgbatest/product.cc, + src/evtgbatest/product.test, src/evtgbatest/readsave.cc, + src/evtgbatest/readsave.test: New files. + * configure.ac: Create the Makefiles in these new subdirectories. + * src/Makefile.am: Recurse them. + * src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word): New function. diff --git a/configure.ac b/configure.ac index 1cfef9786..a1f9c79d9 100644 --- a/configure.ac +++ b/configure.ac @@ -64,6 +64,11 @@ AC_CONFIG_FILES([ iface/gspn/Makefile iface/gspn/defs src/Makefile + src/evtgba/Makefile + src/evtgbaalgos/Makefile + src/evtgbaparse/Makefile + src/evtgbatest/Makefile + src/evtgbatest/defs src/ltlast/Makefile src/ltlenv/Makefile src/ltlparse/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 22c7488f1..8d7f096dd 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -23,8 +23,10 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. # Keep tests at the end. -SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse tgba tgbaalgos tgbaparse . \ - ltltest tgbatest sanity +SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse \ + tgba tgbaalgos tgbaparse \ + evtgba evtgbaalgos evtgbaparse . \ + ltltest tgbatest evtgbatest sanity lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -37,6 +39,10 @@ libspot_la_LIBADD = \ ltlast/libltlast.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ - tgbaparse/libtgbaparse.la + tgbaparse/libtgbaparse.la \ + evtgba/libevtgba.la \ + evtgbaalgos/libevtgbaalgos.la \ + evtgbaparse/libevtgbaparse.la + # Dummy C++ source to cause C++ linking. nodist_EXTRA_libspot_la_SOURCES = _.cc diff --git a/src/evtgba/.cvsignore b/src/evtgba/.cvsignore new file mode 100644 index 000000000..799fc9785 --- /dev/null +++ b/src/evtgba/.cvsignore @@ -0,0 +1,6 @@ +.deps +.libs +*.lo +*.la +Makefile +Makefile.in diff --git a/src/evtgba/Makefile.am b/src/evtgba/Makefile.am new file mode 100644 index 000000000..53ddc8932 --- /dev/null +++ b/src/evtgba/Makefile.am @@ -0,0 +1,39 @@ +## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +evtgbadir = $(pkgincludedir)/evtgba + +evtgba_HEADERS = \ + evtgba.hh \ + evtgbaiter.hh \ + explicit.hh \ + product.hh \ + symbol.hh + +noinst_LTLIBRARIES = libevtgba.la +libevtgba_la_SOURCES = \ + evtgba.cc \ + explicit.cc \ + product.cc \ + symbol.cc diff --git a/src/evtgba/evtgba.cc b/src/evtgba/evtgba.cc new file mode 100644 index 000000000..556a03206 --- /dev/null +++ b/src/evtgba/evtgba.cc @@ -0,0 +1,69 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "evtgba.hh" +#include "misc/escape.hh" +#include "misc/bareword.hh" + +namespace spot +{ + evtgba::evtgba() + { + } + + evtgba::~evtgba() + { + } + + std::string + evtgba::format_label(const symbol* symbol) const + { + return symbol->name(); + } + + std::string + evtgba::format_acceptance_condition(const symbol* symbol) const + { + return symbol->name(); + } + + std::string + evtgba::format_acceptance_conditions(const symbol_set& symset) const + { + std::ostringstream o; + symbol_set::const_iterator i = symset.begin(); + if (i != symset.end()) + { + o << '{'; + for (;;) + { + o << quote_unless_bare_word(format_acceptance_condition(*i)); + if (++i == symset.end()) + break; + o << ", "; + } + o << '}'; + } + return o.str(); + } + +} diff --git a/src/evtgba/evtgba.hh b/src/evtgba/evtgba.hh new file mode 100644 index 000000000..7955f1aa1 --- /dev/null +++ b/src/evtgba/evtgba.hh @@ -0,0 +1,69 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBA_EVTGBA_HH +# define SPOT_EVTGBA_EVTGBA_HH + +#include "tgba/state.hh" +#include "evtgbaiter.hh" + +namespace spot +{ + // FIXME: doc me + class evtgba + { + protected: + evtgba(); + + public: + virtual ~evtgba(); + + virtual evtgba_iterator* init_iter() const = 0; + virtual evtgba_iterator* succ_iter(const state* s) const = 0; + virtual evtgba_iterator* pred_iter(const state* s) const = 0; + + /// \brief Format the state as a string for printing. + /// + /// This formating is the responsability of the automata + /// who owns the state. + virtual std::string format_state(const state* state) const = 0; + + virtual std::string format_label(const symbol* symbol) const; + virtual std::string format_acceptance_condition(const symbol* symbol) const; + virtual std::string + format_acceptance_conditions(const symbol_set& symset) const; + + /// \brief Return the set of all acceptance conditions used + /// by this automaton. + /// + /// The goal of the emptiness check is to ensure that + /// a strongly connected component walks through each + /// of these acceptiong conditions. I.e., the union + /// of the acceptiong conditions of all transition in + /// the SCC should be equal to the result of this function. + virtual const symbol_set& all_acceptance_conditions() const = 0; + + virtual const symbol_set& alphabet() const = 0; + }; + +} + +#endif // SPOT_EVTGBA_EVTGBA_HH diff --git a/src/evtgba/evtgbaiter.hh b/src/evtgba/evtgbaiter.hh new file mode 100644 index 000000000..0f9709bdd --- /dev/null +++ b/src/evtgba/evtgbaiter.hh @@ -0,0 +1,50 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBA_ITER_HH +# define SPOT_EVTGBA_ITER_HH + +#include "tgba/state.hh" +#include "symbol.hh" +#include "evtgbaiter.hh" + +namespace spot +{ + // FIXME: doc me + class evtgba_iterator + { + public: + virtual + ~evtgba_iterator() + { + } + + virtual void first() = 0; + virtual void next() = 0; + virtual bool done() const = 0; + + virtual const state* current_state() const = 0; + virtual const symbol* current_label() const = 0; + virtual symbol_set current_acceptance_conditions() const = 0; + }; +} + +#endif // SPOT_EVTGBA_ITER_HH diff --git a/src/evtgba/explicit.cc b/src/evtgba/explicit.cc new file mode 100644 index 000000000..446624498 --- /dev/null +++ b/src/evtgba/explicit.cc @@ -0,0 +1,284 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "explicit.hh" +#include "misc/bareword.hh" +#include "misc/escape.hh" + +namespace spot +{ + const evtgba_explicit::state* + state_evtgba_explicit::get_state() const + { + return state_; + } + + int + state_evtgba_explicit::compare(const spot::state* other) const + { + const state_evtgba_explicit* o = + dynamic_cast(other); + assert(o); + return o->get_state() - get_state(); + } + + size_t + state_evtgba_explicit::hash() const + { + return + reinterpret_cast(get_state()) - static_cast(0); + } + + state_evtgba_explicit* + state_evtgba_explicit::clone() const + { + return new state_evtgba_explicit(*this); + } + + namespace + { + class evtgba_explicit_iterator: public evtgba_iterator + { + public: + evtgba_explicit_iterator(const evtgba_explicit::transition_list* s) + : s_(s), i_(s_->end()) + { + } + + virtual + ~evtgba_explicit_iterator() + { + } + + virtual void first() + { + i_ = s_->begin(); + } + + virtual void + next() + { + ++i_; + } + + virtual bool + done() const + { + return i_ == s_->end(); + } + + virtual const symbol* + current_label() const + { + return (*i_)->label; + } + + virtual symbol_set + current_acceptance_conditions() const + { + return (*i_)->acceptance_conditions; + } + protected: + const evtgba_explicit::transition_list* s_; + evtgba_explicit::transition_list::const_iterator i_; + }; + + + + class evtgba_explicit_iterator_fw: public evtgba_explicit_iterator + { + public: + evtgba_explicit_iterator_fw(const evtgba_explicit::transition_list* s) + : evtgba_explicit_iterator(s) + { + } + + virtual + ~evtgba_explicit_iterator_fw() + { + } + + const state* + current_state() const + { + return new state_evtgba_explicit((*i_)->out); + } + }; + + class evtgba_explicit_iterator_bw: public evtgba_explicit_iterator + { + public: + evtgba_explicit_iterator_bw(const evtgba_explicit::transition_list* s) + : evtgba_explicit_iterator(s) + { + } + + virtual + ~evtgba_explicit_iterator_bw() + { + } + + const state* + current_state() const + { + return new state_evtgba_explicit((*i_)->in); + } + }; + } + + evtgba_explicit::evtgba_explicit() + { + } + + evtgba_explicit::~evtgba_explicit() + { + for (transition_list::const_iterator i = init_states_.begin(); + i != init_states_.end(); ++i) + delete *i; + for (ns_map::const_iterator j = name_state_map_.begin(); + j != name_state_map_.end(); ++j) + { + for (transition_list::const_iterator i = j->second->out.begin(); + i != j->second->out.end(); ++i) + delete *i; + delete j->second; + } + for (symbol_set::const_iterator i = alphabet_.begin(); + i != alphabet_.end(); ++i) + (*i)->unref(); + for (symbol_set::const_iterator i = acc_set_.begin(); + i != acc_set_.end(); ++i) + (*i)->unref(); + } + + evtgba_iterator* + evtgba_explicit::init_iter() const + { + return new evtgba_explicit_iterator_fw(&init_states_); + } + + evtgba_iterator* + evtgba_explicit::succ_iter(const spot::state* s) const + { + const state_evtgba_explicit* u = + dynamic_cast(s); + assert(u); + return new evtgba_explicit_iterator_fw(&u->get_state()->out); + } + + evtgba_iterator* + evtgba_explicit::pred_iter(const spot::state* s) const + { + const state_evtgba_explicit* u = + dynamic_cast(s); + assert(u); + return new evtgba_explicit_iterator_fw(&u->get_state()->in); + } + + std::string + evtgba_explicit::format_state(const spot::state* s) const + { + const state_evtgba_explicit* u = + dynamic_cast(s); + assert(u); + sn_map::const_iterator i = state_name_map_.find(u->get_state()); + assert(i != state_name_map_.end()); + return i->second; + } + + const symbol_set& + evtgba_explicit::all_acceptance_conditions() const + { + return acc_set_; + } + + const symbol_set& + evtgba_explicit::alphabet() const + { + return alphabet_; + } + + evtgba_explicit::state* + evtgba_explicit::declare_state(const std::string& name) + { + ns_map::const_iterator i = name_state_map_.find(name); + if (i != name_state_map_.end()) + return i->second; + state* s = new state; + name_state_map_[name] = s; + state_name_map_[s] = name; + return s; + } + + evtgba_explicit::transition* + evtgba_explicit::add_transition(const std::string& source, + const rsymbol& label, + rsymbol_set acc, + const std::string& dest) + { + state* in = declare_state(source); + state* out = declare_state(dest); + transition* t = new transition; + t->in = in; + t->label = label; + t->out = out; + in->out.push_back(t); + out->in.push_back(t); + + for (rsymbol_set::const_iterator i = acc.begin(); i != acc.end(); ++i) + { + const symbol* s = *i; + t->acceptance_conditions.insert(s); + declare_acceptance_condition(*i); + } + + if (alphabet_.find(t->label) == alphabet_.end()) + { + alphabet_.insert(t->label); + t->label->ref(); + } + + return t; + } + + void + evtgba_explicit::declare_acceptance_condition(const rsymbol& acc) + { + const symbol* s = acc; + if (acc_set_.find(s) == acc_set_.end()) + { + acc_set_.insert(s); + s->ref(); + } + } + + + void + evtgba_explicit::set_init_state(const std::string& name) + { + transition* t = new transition; + t->in = 0; + t->out = declare_state(name); + t->label = 0; + init_states_.push_back(t); + } + +} diff --git a/src/evtgba/explicit.hh b/src/evtgba/explicit.hh new file mode 100644 index 000000000..d16e3a24c --- /dev/null +++ b/src/evtgba/explicit.hh @@ -0,0 +1,112 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBA_EXPLICIT_HH +# define SPOT_EVTGBA_EXPLICIT_HH + +#include "evtgba.hh" +#include +#include "misc/hash.hh" + +namespace spot +{ + // FIXME: doc me + class evtgba_explicit: public evtgba + { + public: + struct transition; + typedef std::list transition_list; + struct state + { + transition_list in, out; + }; + + /// Explicit transitions (used by spot::evtgba_explicit). + struct transition + { + const symbol* label; + symbol_set acceptance_conditions; + state* in; + state* out; + }; + + evtgba_explicit(); + virtual ~evtgba_explicit(); + + // evtgba interface + virtual evtgba_iterator* init_iter() const; + virtual evtgba_iterator* succ_iter(const spot::state* s) const; + virtual evtgba_iterator* pred_iter(const spot::state* s) const; + virtual std::string format_state(const spot::state* state) const; + virtual const symbol_set& all_acceptance_conditions() const; + virtual const symbol_set& alphabet() const; + + transition* add_transition(const std::string& source, + const rsymbol& label, + rsymbol_set acc, + const std::string& dest); + /// \brief Designate \a name as initial state. + /// + /// Can be called multiple times in case there is several initial states. + void set_init_state(const std::string& name); + void declare_acceptance_condition(const rsymbol& acc); + protected: + + state* declare_state(const std::string& name); + + typedef Sgi::hash_map ns_map; + typedef Sgi::hash_map > sn_map; + + ns_map name_state_map_; + sn_map state_name_map_; + + symbol_set acc_set_; + symbol_set alphabet_; + transition_list init_states_; + }; + + /// States used by spot::tgba_evtgba_explicit. + class state_evtgba_explicit : public spot::state + { + public: + state_evtgba_explicit(const evtgba_explicit::state* s) + : state_(s) + { + } + + virtual int compare(const spot::state* other) const; + virtual size_t hash() const; + virtual state_evtgba_explicit* clone() const; + + virtual ~state_evtgba_explicit() + { + } + + const evtgba_explicit::state* get_state() const; + private: + const evtgba_explicit::state* state_; + }; + +} + +#endif // SPOT_EVTGBA_EXPLICIT_HH diff --git a/src/evtgba/product.cc b/src/evtgba/product.cc new file mode 100644 index 000000000..1f16f06c1 --- /dev/null +++ b/src/evtgba/product.cc @@ -0,0 +1,471 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "product.hh" +#include "misc/modgray.hh" +#include +#include + +namespace spot +{ + namespace + { + class evtgba_product_state: public state + { + public: + evtgba_product_state(state const* const* s, int n) + : s_(s), n_(n) + { + } + + ~evtgba_product_state() + { + for (int j = 0; j < n_; ++j) + delete s_[j]; + delete[] s_; + } + + state const* + nth(int n) const + { + assert(n < n_); + return s_[n]; + } + + state const* const* + all() const + { + return s_; + } + + int + compare(const state* other) const + { + const evtgba_product_state* s = + dynamic_cast(other); + assert(s); + assert(s->n_ == n_); + for (int i = 0; i < n_; ++i) + { + int res = s_[i]->compare(s->nth(i)); + if (res) + return res; + } + return 0; + } + + size_t + hash() const + { + // We assume that size_t has at least 32bits. + size_t res = 0; + for (int i = 0; i != n_; ++i) + { + size_t key = s_[i]->hash(); + + // Thomas Wang's 32 bit hash Function + // http://www.concentric.net/~Ttwang/tech/inthash.htm + key += ~(key << 15); + key ^= (key >> 10); + key += (key << 3); + key ^= (key >> 6); + key += ~(key << 11); + key ^= (key >> 16); + + res ^= key; + } + return res; + } + + evtgba_product_state* + clone() const + { + state const** s = new state const*[n_]; + memcpy(s, s_, n_ * sizeof(*s_)); + return new evtgba_product_state(s, n_); + } + + + private: + state const* const* s_; + int n_; + }; + + + class evtgba_product_init_iterator: + public evtgba_iterator, private loopless_modular_mixed_radix_gray_code + { + public: + evtgba_product_init_iterator(evtgba_iterator* const* op, int n) + : loopless_modular_mixed_radix_gray_code(n), op_(op), n_(n), done_(0) + { + for (int j = 0; j < n_; ++j) + { + op_[j]->first(); + if (op_[j]->done()) + ++done_; + } + } + + ~evtgba_product_init_iterator() + { + for (int j = 0; j < n_; ++j) + delete op_[j]; + delete[] op_; + } + + virtual void + first() + { + loopless_modular_mixed_radix_gray_code::first(); + step_(); + } + + virtual void + next() + { + loopless_modular_mixed_radix_gray_code::next(); + step_(); + } + + virtual bool + done() const + { + return loopless_modular_mixed_radix_gray_code::done(); + } + + virtual const state* + current_state() const + { + state const** s = new state const*[n_]; + for (int j = 0; j < n_; ++j) + s[j] = op_[j]->current_state(); + return new evtgba_product_state(s, n_); + } + + virtual const symbol* + current_label() const + { + assert(0); + return 0; + } + + virtual symbol_set + current_acceptance_conditions() const + { + assert(0); + symbol_set s; + return s; + } + + private: + + void + pre_update(int j) + { + if (op_[j]->done()) + --done_; + } + + void + post_update(int j) + { + if (op_[j]->done()) + ++done_; + } + + virtual void + a_first(int j) + { + pre_update(j); + op_[j]->first(); + post_update(j); + } + + virtual void + a_next(int j) + { + pre_update(j); + op_[j]->next(); + post_update(j); + } + + virtual bool + a_last(int j) const + { + return op_[j]->done(); + } + + void + step_() + { + while (done_ && !loopless_modular_mixed_radix_gray_code::done()) + loopless_modular_mixed_radix_gray_code::next(); + } + + evtgba_iterator* const* op_; + const int n_; + int done_; // number of iterator for which done() is true. + }; + + class evtgba_product_iterator: + public evtgba_iterator, private loopless_modular_mixed_radix_gray_code + { + public: + evtgba_product_iterator(evtgba_iterator* const* op, int n, + state const* const* from, + const evtgba_product::common_symbol_table& cst) + : loopless_modular_mixed_radix_gray_code(n), op_(op), n_(n), + from_(from), cst_(cst) + { + count_pointer_ = new int*[n]; + for (int j = 0; j < n; ++j) + count_pointer_[j] = 0; + } + + virtual + ~evtgba_product_iterator() + { + delete[] count_pointer_; + for (int j = 0; j < n_; ++j) + delete op_[j]; + delete[] op_; + } + + virtual void + first() + { + loopless_modular_mixed_radix_gray_code::first(); + step_(); + } + + virtual void + next() + { + loopless_modular_mixed_radix_gray_code::next(); + step_(); + } + + virtual bool + done() const + { + return loopless_modular_mixed_radix_gray_code::done(); + } + + virtual const state* + current_state() const + { + state const** s = new state const*[n_]; + for (int j = 0; j < n_; ++j) + { + if (op_[j]->done()) + s[j] = from_[j]->clone(); + else + s[j] = op_[j]->current_state(); + } + return new evtgba_product_state(s, n_); + } + + virtual const symbol* + current_label() const + { + return lcm_.begin()->first; + } + + virtual symbol_set + current_acceptance_conditions() const + { + symbol_set s; + for (int j = 0; j < n_; ++j) + if (!op_[j]->done()) + { + symbol_set t = op_[j]->current_acceptance_conditions(); + s.insert(t.begin(), t.end()); + } + return s; + } + + private: + + void + pre_update(int j) + { + if (!--*count_pointer_[j]) + lcm_.erase(op_[j]->current_label()); + count_pointer_[j] = 0; + } + + void + post_update(int j) + { + if (!op_[j]->done()) + { + count_pointer_[j] = &lcm_[op_[j]->current_label()]; + ++*count_pointer_[j]; + } + } + + virtual void + a_first(int j) + { + if (count_pointer_[j]) + pre_update(j); + op_[j]->first(); + post_update(j); + } + + virtual void + a_next(int j) + { + pre_update(j); + op_[j]->next(); + post_update(j); + } + + virtual bool + a_last(int j) const + { + return op_[j]->done(); + } + + void + step_() + { + while (!loopless_modular_mixed_radix_gray_code::done()) + { + if (lcm_.size() == 1) + { + const symbol* l = lcm_.begin()->first; + const std::set& s = cst_.find(l)->second; + std::set::const_iterator i; + for (i = s.begin(); i != s.end(); ++i) + if (op_[*i]->done()) + break; + if (i == s.end()) + return; + } + loopless_modular_mixed_radix_gray_code::next(); + } + } + + evtgba_iterator* const* op_; + int n_; + state const* const* from_; + const evtgba_product::common_symbol_table& cst_; + typedef std::map label_count_map; + label_count_map lcm_; + int** count_pointer_; + }; + + } // anonymous + + + evtgba_product::evtgba_product(const evtgba_product_operands& op) + : op_(op) + { + int n = 0; + for (evtgba_product_operands::const_iterator i = op.begin(); + i != op.end(); ++i, ++n) + { + const symbol_set& al = (*i)->alphabet(); + alphabet_.insert(al.begin(), al.end()); + const symbol_set& ac = (*i)->all_acceptance_conditions(); + all_acc_.insert(ac.begin(), ac.end()); + + for (symbol_set::const_iterator j = al.begin(); j != al.end(); ++j) + common_symbols_[*j].insert(n); + } + } + + evtgba_product::~evtgba_product() + { + } + + evtgba_iterator* + evtgba_product::init_iter() const + { + int n = op_.size(); + evtgba_iterator** it = new evtgba_iterator *[n]; + for (int i = 0; i < n; ++i) + it[i] = op_[i]->init_iter(); + + return new evtgba_product_init_iterator(it, n); + } + + evtgba_iterator* + evtgba_product::succ_iter(const state* st) const + { + const evtgba_product_state* s = + dynamic_cast(st); + assert(s); + + int n = op_.size(); + + evtgba_iterator** it = new evtgba_iterator *[n]; + for (int i = 0; i < n; ++i) + it[i] = op_[i]->succ_iter(s->nth(i)); + + return new evtgba_product_iterator(it, n, s->all(), common_symbols_); + } + + evtgba_iterator* + evtgba_product::pred_iter(const state* st) const + { + const evtgba_product_state* s = + dynamic_cast(st); + assert(s); + + int n = op_.size(); + + evtgba_iterator** it = new evtgba_iterator *[n]; + for (int i = 0; i < n; ++i) + it[i] = op_[i]->pred_iter(s->nth(i)); + + return new evtgba_product_iterator(it, n, s->all(), common_symbols_); + } + + std::string + evtgba_product::format_state(const state* st) const + { + const evtgba_product_state* s = + dynamic_cast(st); + int n = op_.size(); + std::string res = "<" + op_[0]->format_state(s->nth(0)); + + for (int i = 1; i < n; ++i) + res = res + ", " + op_[i]->format_state(s->nth(i)); + + return res + ">"; + } + + const symbol_set& + evtgba_product::all_acceptance_conditions() const + { + return all_acc_; + } + + const symbol_set& + evtgba_product::alphabet() const + { + return alphabet_; + } + +} diff --git a/src/evtgba/product.hh b/src/evtgba/product.hh new file mode 100644 index 000000000..e7db45332 --- /dev/null +++ b/src/evtgba/product.hh @@ -0,0 +1,69 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBA_PRODUCT_HH +# define SPOT_EVTGBA_PRODUCT_HH + +#include "evtgba/evtgba.hh" +#include + +namespace spot +{ + // FIXME: doc me + class evtgba_product: public evtgba + { + public: + typedef std::vector evtgba_product_operands; + evtgba_product(const evtgba_product_operands& op); + virtual ~evtgba_product(); + + virtual evtgba_iterator* init_iter() const; + virtual evtgba_iterator* succ_iter(const state* s) const; + virtual evtgba_iterator* pred_iter(const state* s) const; + + /// \brief Format the state as a string for printing. + /// + /// This formating is the responsability of the automata + /// who owns the state. + virtual std::string format_state(const state* state) const; + + /// \brief Return the set of all acceptance conditions used + /// by this automaton. + /// + /// The goal of the emptiness check is to ensure that + /// a strongly connected component walks through each + /// of these acceptiong conditions. I.e., the union + /// of the acceptiong conditions of all transition in + /// the SCC should be equal to the result of this function. + virtual const symbol_set& all_acceptance_conditions() const; + virtual const symbol_set& alphabet() const; + + typedef std::map > common_symbol_table; + private: + const evtgba_product_operands op_; + symbol_set alphabet_; + symbol_set all_acc_; + common_symbol_table common_symbols_; + }; + +} + +#endif // SPOT_EVTGBA_PRODUCT_HH diff --git a/src/evtgba/symbol.cc b/src/evtgba/symbol.cc new file mode 100644 index 000000000..2c1231f21 --- /dev/null +++ b/src/evtgba/symbol.cc @@ -0,0 +1,109 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "symbol.hh" +#include + +namespace spot +{ + symbol::map symbol::instances_; + + symbol::symbol(const std::string* name) + : name_(name), refs_(1) + { + } + + symbol::~symbol() + { + map::iterator i = instances_.find(name()); + assert (i != instances_.end()); + instances_.erase(i); + } + + const symbol* + symbol::instance(const std::string& name) + { + map::iterator i = instances_.find(name); + if (i != instances_.end()) + { + const symbol* s = i->second; + s->ref(); + return s; + } + // Convoluted insertion because we want the NAME member of the + // value to point to the key. + i = instances_.insert(map::value_type(name, 0)).first; + i->second = new symbol(&i->first); + return i->second; + } + + const std::string& + symbol::name() const + { + return *name_; + } + + void + symbol::ref() const + { + ++refs_; + } + + void + symbol::unref() const + { + assert(refs_ > 0); + --refs_; + if (!refs_) + delete this; + } + + int + symbol::ref_count_() const + { + return refs_; + } + + unsigned + symbol::instance_count() + { + return instances_.size(); + } + + std::ostream& + symbol::dump_instances(std::ostream& os) + { + for (map::iterator i = instances_.begin(); i != instances_.end(); ++i) + { + os << i->second << " = " << i->second->ref_count_() + << " * symbol(" << i->second->name() << ")" << std::endl; + } + return os; + } + + + + + + + +} diff --git a/src/evtgba/symbol.hh b/src/evtgba/symbol.hh new file mode 100644 index 000000000..34ff78f20 --- /dev/null +++ b/src/evtgba/symbol.hh @@ -0,0 +1,126 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBA_SYMBOL_HH +# define SPOT_EVTGBA_SYMBOL_HH + +#include +#include +#include +#include + +namespace spot +{ + class symbol + { + public: + static const symbol* instance(const std::string& name); + const std::string& name() const; + + /// Number of instantiated atomic propositions. For debugging. + static unsigned instance_count(); + /// List all instances of atomic propositions. For debugging. + static std::ostream& dump_instances(std::ostream& os); + + void ref() const; + void unref() const; + + protected: + int ref_count_() const; + symbol(const std::string* name); + ~symbol(); + typedef std::map map; + static map instances_; + private: + symbol(const symbol&); /// Undefined. + const std::string* name_; + mutable int refs_; + }; + + class rsymbol + { + public: + rsymbol(const symbol* s): s_(s) + { + } + + rsymbol(const std::string& s): s_(symbol::instance(s)) + { + } + + rsymbol(const char* s): s_(symbol::instance(s)) + { + } + + rsymbol(const rsymbol& rs): s_(rs.s_) + { + s_->ref(); + } + + ~rsymbol() + { + s_->unref(); + } + + operator const symbol*() const + { + return s_; + } + + const rsymbol& + operator=(const rsymbol& rs) + { + if (this != &rs) + { + this->~rsymbol(); + new (this) rsymbol(rs); + } + return *this; + } + + bool + operator==(const rsymbol& rs) const + { + return s_ == rs.s_; + } + + bool + operator!=(const rsymbol& rs) const + { + return s_ != rs.s_; + } + + bool + operator<(const rsymbol& rs) const + { + return s_ < rs.s_; + } + + private: + const symbol* s_; + }; + + typedef std::set symbol_set; + typedef std::set rsymbol_set; + +} + +#endif // SPOT_EVTGBA_SYMBOL_HH diff --git a/src/evtgbaalgos/.cvsignore b/src/evtgbaalgos/.cvsignore new file mode 100644 index 000000000..799fc9785 --- /dev/null +++ b/src/evtgbaalgos/.cvsignore @@ -0,0 +1,6 @@ +.deps +.libs +*.lo +*.la +Makefile +Makefile.in diff --git a/src/evtgbaalgos/Makefile.am b/src/evtgbaalgos/Makefile.am new file mode 100644 index 000000000..a9c799141 --- /dev/null +++ b/src/evtgbaalgos/Makefile.am @@ -0,0 +1,36 @@ +## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +evtgbaalgosdir = $(pkgincludedir)/evtgbaalgos + +evtgbaalgos_HEADERS = \ + dotty.hh \ + reachiter.hh \ + save.hh + +noinst_LTLIBRARIES = libevtgbaalgos.la +libevtgbaalgos_la_SOURCES = \ + dotty.cc \ + reachiter.cc \ + save.cc diff --git a/src/evtgbaalgos/dotty.cc b/src/evtgbaalgos/dotty.cc new file mode 100644 index 000000000..bba60ecf4 --- /dev/null +++ b/src/evtgbaalgos/dotty.cc @@ -0,0 +1,93 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "evtgba/evtgba.hh" +#include "dotty.hh" +#include "reachiter.hh" +#include "misc/escape.hh" +#include "misc/bareword.hh" + +namespace spot +{ + namespace + { + class dotty_bfs : public evtgba_reachable_iterator_breadth_first + { + public: + dotty_bfs(const evtgba* a, std::ostream& os) + : evtgba_reachable_iterator_breadth_first(a), os_(os) + { + } + + void + start(int n) + { + os_ << "digraph G {" << std::endl; + for (int i = 0; i < n;) + { + ++i; + os_ << " \"*" << i + << "\" [label=\"\", style=invis, height=0]" << std::endl; + os_ << " \"*" << i << "\" -> " << i << std::endl; + } + } + + void + end() + { + os_ << "}" << std::endl; + } + + void + process_state(const state* s, int n, evtgba_iterator*) + { + os_ << " " << n << " [label=" + << quote_unless_bare_word(automata_->format_state(s)) + << "]" << std::endl; + } + + void + process_link(int in, int out, const evtgba_iterator* si) + { + os_ << " " << in << " -> " << out << " [label=\""; + escape_str(os_, automata_->format_label(si->current_label())) + << "\\n"; + escape_str(os_, automata_->format_acceptance_conditions + (si->current_acceptance_conditions())) + << "\"]" << std::endl; + } + + private: + std::ostream& os_; + }; + } + + std::ostream& + dotty_reachable(std::ostream& os, const evtgba* g) + { + dotty_bfs d(g, os); + d.run(); + return os; + } + + +} diff --git a/src/evtgbaalgos/dotty.hh b/src/evtgbaalgos/dotty.hh new file mode 100644 index 000000000..8b7186f36 --- /dev/null +++ b/src/evtgbaalgos/dotty.hh @@ -0,0 +1,34 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAALGOS_DOTTY_HH +# define SPOT_EVTGBAALGOS_DOTTY_HH + +#include "evtgba/evtgba.hh" +#include + +namespace spot +{ + /// \brief Print reachable states in dot format. + std::ostream& dotty_reachable(std::ostream& os, const evtgba* g); +} + +#endif // SPOT_EVTGBAALGOS_DOTTY_HH diff --git a/src/evtgbaalgos/reachiter.cc b/src/evtgbaalgos/reachiter.cc new file mode 100644 index 000000000..60432c06e --- /dev/null +++ b/src/evtgbaalgos/reachiter.cc @@ -0,0 +1,160 @@ +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "reachiter.hh" + +namespace spot +{ + // evtgba_reachable_iterator + ////////////////////////////////////////////////////////////////////// + + evtgba_reachable_iterator::evtgba_reachable_iterator(const evtgba* a) + : automata_(a) + { + } + + evtgba_reachable_iterator::~evtgba_reachable_iterator() + { + seen_map::const_iterator s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + delete ptr; + } + } + + void + evtgba_reachable_iterator::run() + { + int n = 0; + + evtgba_iterator* i = automata_->init_iter(); + for (i->first(); !i->done(); i->next()) + { + const state* dest = i->current_state(); + add_state(dest); + seen[dest] = ++n; + } + delete i; + start(n); + + const state* t; + while ((t = next_state())) + { + assert(seen.find(t) != seen.end()); + int tn = seen[t]; + evtgba_iterator* si = automata_->succ_iter(t); + process_state(t, tn, si); + for (si->first(); !si->done(); si->next()) + { + const state* current = si->current_state(); + seen_map::const_iterator s = seen.find(current); + if (s == seen.end()) + { + seen[current] = ++n; + add_state(current); + process_link(tn, n, si); + } + else + { + process_link(tn, s->second, si); + delete current; + } + } + delete si; + } + end(); + } + + void + evtgba_reachable_iterator::start(int) + { + } + + void + evtgba_reachable_iterator::end() + { + } + + void + evtgba_reachable_iterator::process_state(const state*, int, evtgba_iterator*) + { + } + + void + evtgba_reachable_iterator::process_link(int, int, const evtgba_iterator*) + { + } + + // evtgba_reachable_iterator_depth_first + ////////////////////////////////////////////////////////////////////// + + evtgba_reachable_iterator_depth_first:: + evtgba_reachable_iterator_depth_first(const evtgba* a) + : evtgba_reachable_iterator(a) + { + } + + void + evtgba_reachable_iterator_depth_first::add_state(const state* s) + { + todo.push(s); + } + + const state* + evtgba_reachable_iterator_depth_first::next_state() + { + if (todo.empty()) + return 0; + const state* s = todo.top(); + todo.pop(); + return s; + } + + // evtgba_reachable_iterator_breadth_first + ////////////////////////////////////////////////////////////////////// + + evtgba_reachable_iterator_breadth_first:: + evtgba_reachable_iterator_breadth_first(const evtgba* a) + : evtgba_reachable_iterator(a) + { + } + + void + evtgba_reachable_iterator_breadth_first::add_state(const state* s) + { + todo.push_back(s); + } + + const state* + evtgba_reachable_iterator_breadth_first::next_state() + { + if (todo.empty()) + return 0; + const state* s = todo.front(); + todo.pop_front(); + return s; + } + +} diff --git a/src/evtgbaalgos/reachiter.hh b/src/evtgbaalgos/reachiter.hh new file mode 100644 index 000000000..dadb4a7d4 --- /dev/null +++ b/src/evtgbaalgos/reachiter.hh @@ -0,0 +1,121 @@ +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAALGOS_REACHITER_HH +# define SPOT_EVTGBAALGOS_REACHITER_HH + +#include "misc/hash.hh" +#include "evtgba/evtgba.hh" +#include +#include + +namespace spot +{ + /// \brief Iterate over all reachable states of a spot::evtgba. + class evtgba_reachable_iterator + { + public: + evtgba_reachable_iterator(const evtgba* a); + virtual ~evtgba_reachable_iterator(); + + /// \brief Iterate over all reachable states of a spot::evtgba. + /// + /// This is a template method that will call add_state(), next_state(), + /// start(), end(), process_state(), and process_link(), while it + /// iterate over state. + void run(); + + /// \name Todo list management. + /// + /// spot::evtgba_reachable_iterator_depth_first and + /// spot::evtgba_reachable_iterator_breadth_first offer two precanned + /// implementations for these functions. + /// \{ + /// \brief Called by run() to register newly discovered states. + virtual void add_state(const state* s) = 0; + /// \brief Called by run() to obtain the + virtual const state* next_state() = 0; + /// \} + + /// \brief Called by run() before starting its iteration. + /// + /// \param n The number of initial states. + virtual void start(int n); + /// Called by run() once all states have been explored. + virtual void end(); + + /// Called by run() to process a state. + /// + /// \param s The current state. + /// \param n An unique number assigned to \a s. + /// \param si The spot::evtgba_iterator for \a s. + virtual void process_state(const state* s, int n, evtgba_iterator* si); + /// Called by run() to process a transition. + /// + /// \param in The source state number. + /// \param out The destination state number. + /// \param si The spot::evtgba_iterator positionned on the current + /// transition. + virtual void process_link(int in, int out, const evtgba_iterator* si); + + protected: + const evtgba* automata_; ///< The spot::evtgba to explore. + + typedef Sgi::hash_map seen_map; + seen_map seen; ///< States already seen. + }; + + /// \brief An implementation of spot::evtgba_reachable_iterator that browses + /// states depth first. + class evtgba_reachable_iterator_depth_first: + public evtgba_reachable_iterator + { + public: + evtgba_reachable_iterator_depth_first(const evtgba* a); + + virtual void add_state(const state* s); + virtual const state* next_state(); + + protected: + std::stack todo; ///< A stack of states yet to explore. + }; + + /// \brief An implementation of spot::evtgba_reachable_iterator that browses + /// states breadth first. + class evtgba_reachable_iterator_breadth_first: + public evtgba_reachable_iterator + { + public: + evtgba_reachable_iterator_breadth_first(const evtgba* a); + + virtual void add_state(const state* s); + virtual const state* next_state(); + + protected: + std::deque todo; ///< A queue of states yet to explore. + }; + + +} + + +#endif // SPOT_EVTGBAALGOS_REACHITER_HH diff --git a/src/evtgbaalgos/save.cc b/src/evtgbaalgos/save.cc new file mode 100644 index 000000000..b6de64ef4 --- /dev/null +++ b/src/evtgbaalgos/save.cc @@ -0,0 +1,98 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "save.hh" +#include "reachiter.hh" +#include "misc/bareword.hh" + +namespace spot +{ + namespace + { + class save_bfs: public evtgba_reachable_iterator_breadth_first + { + public: + save_bfs(const evtgba* a, std::ostream& os) + : evtgba_reachable_iterator_breadth_first(a), os_(os) + { + } + + void + start(int) + { + os_ << "acc ="; + output_acc_set(automata_->all_acceptance_conditions()); + os_ << ";" << std::endl; + os_ << "init ="; + evtgba_iterator* i = automata_->init_iter(); + for (i->first(); !i->done(); i->next()) + { + const state* s = i->current_state(); + os_ << " " << quote_unless_bare_word(automata_->format_state(s)); + delete s; + } + os_ << ";" << std::endl; + delete i; + } + + void + process_state(const state* s, int, evtgba_iterator* si) + { + std::string cur = quote_unless_bare_word(automata_->format_state(s)); + for (si->first(); !si->done(); si->next()) + { + const state* dest = si->current_state(); + os_ << cur << ", " + << quote_unless_bare_word(automata_->format_state(dest)) + << ", " + << quote_unless_bare_word(automata_ + ->format_label(si->current_label())) + << ","; + output_acc_set(si->current_acceptance_conditions()); + os_ << ";" << std::endl; + delete dest; + } + } + + private: + std::ostream& os_; + + void + output_acc_set(const symbol_set& ss) const + { + for (symbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i) + os_ << " " + << quote_unless_bare_word(automata_ + ->format_acceptance_condition(*i)); + } + + }; + } + + std::ostream& + evtgba_save_reachable(std::ostream& os, const evtgba* g) + { + save_bfs b(g, os); + b.run(); + return os; + } +} diff --git a/src/evtgbaalgos/save.hh b/src/evtgbaalgos/save.hh new file mode 100644 index 000000000..f24565f9e --- /dev/null +++ b/src/evtgbaalgos/save.hh @@ -0,0 +1,34 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAALGOS_SAVE_HH +# define SPOT_EVTGBAALGOS_SAVE_HH + +#include "evtgba/evtgba.hh" +#include + +namespace spot +{ + /// \brief Save reachable states in text format. + std::ostream& evtgba_save_reachable(std::ostream& os, const evtgba* g); +} + +#endif // SPOT_EVTGBAALGOS_SAVE_HH diff --git a/src/evtgbaparse/.cvsignore b/src/evtgbaparse/.cvsignore new file mode 100644 index 000000000..9a1c7773f --- /dev/null +++ b/src/evtgbaparse/.cvsignore @@ -0,0 +1,13 @@ +.deps +Makefile +Makefile.in +location.hh +evtgbaparse.cc +evtgbaparse.hh +evtgbaparse.output +evtgbascan.cc +position.hh +stack.hh +*.lo +*.la +.libs diff --git a/src/evtgbaparse/Makefile.am b/src/evtgbaparse/Makefile.am new file mode 100644 index 000000000..5c1bf3840 --- /dev/null +++ b/src/evtgbaparse/Makefile.am @@ -0,0 +1,61 @@ +## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +evtgbaparsedir = $(pkgincludedir)/evtgbaparse + +evtgbaparse_HEADERS = \ + public.hh + +noinst_LTLIBRARIES = libevtgbaparse.la + +EVTGBAPARSE_YY = evtgbaparse.yy +FROM_EVTGBAPARSE_YY_MAIN = evtgbaparse.cc +FROM_EVTGBAPARSE_YY_OTHERS = \ + stack.hh \ + position.hh \ + location.hh \ + evtgbaparse.hh + +FROM_EVTGBAPARSE_YY = $(FROM_EVTGBAPARSE_YY_MAIN) $(FROM_EVTGBAPARSE_YY_OTHERS) + +BUILT_SOURCES = $(FROM_EVTGBAPARSE_YY) +MAINTAINERCLEANFILES = $(FROM_EVTGBAPARSE_YY) + +$(FROM_EVTGBAPARSE_YY_MAIN): $(srcdir)/$(EVTGBAPARSE_YY) +## We must cd into $(srcdir) first because if we tell bison to read +## $(srcdir)/$(EVTGBAPARSE_YY), it will also use the value of $(srcdir)/ +## in the generated include statements. + cd $(srcdir) && \ + bison --defines --locations --skeleton=lalr1.cc --report=all \ + $(EVTGBAPARSE_YY) -o $(FROM_EVTGBAPARSE_YY_MAIN) +$(FROM_EVTGBAPARSE_YY_OTHERS): $(EVTGBAPARSE_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_EVTGBAPARSE_YY_MAIN) + +EXTRA_DIST = $(EVTGBAPARSE_YY) + +libevtgbaparse_la_SOURCES = \ + evtgbascan.ll \ + fmterror.cc \ + $(FROM_EVTGBAPARSE_YY) \ + parsedecl.hh diff --git a/src/evtgbaparse/evtgbaparse.yy b/src/evtgbaparse/evtgbaparse.yy new file mode 100644 index 000000000..a5a24abbc --- /dev/null +++ b/src/evtgbaparse/evtgbaparse.yy @@ -0,0 +1,153 @@ +/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +** département Systèmes Répartis Coopératifs (SRC), Université Pierre +** et Marie Curie. +** +** This file is part of Spot, a model checking library. +** +** Spot is free software; you can redistribute it and/or modify it +** under the terms of the GNU General Public License as published by +** the Free Software Foundation; either version 2 of the License, or +** (at your option) any later version. +** +** Spot is distributed in the hope that it will be useful, but WITHOUT +** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +** or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +** License for more details. +** +** You should have received a copy of the GNU General Public License +** along with Spot; see the file COPYING. If not, write to the Free +** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +** 02111-1307, USA. +*/ +%{ +#include +#include "public.hh" +#include "evtgba/symbol.hh" +%} + +%parse-param {spot::evtgba_parse_error_list &error_list} +%parse-param {spot::evtgba_explicit* &result} +%debug +%error-verbose +%union +{ + int token; + std::string* str; + spot::rsymbol_set* symset; +} + +%{ +/* evtgbaparse.hh and parsedecl.hh include each other recursively. + We mut ensure that YYSTYPE is declared (by the above %union) + before parsedecl.hh uses it. */ +#include "parsedecl.hh" + +/* Ugly hack so that Bison use tgbayylex, not yylex. + (%name-prefix doesn't work for the lalr1.cc skeleton + at the time of writing.) */ +#define yylex evtgbayylex +%} + +%token STRING UNTERMINATED_STRING +%token IDENT +%type strident string +%type acc_list +%token ACC_DEF +%token INIT_DEF + +%% +evtgba: lines + +/* At least one line. */ +lines: line + | lines line + ; + +line: strident ',' strident ',' strident ',' acc_list ';' + { + result->add_transition(*$1, *$5, *$7, *$3); + delete $1; + delete $5; + delete $3; + delete $7; + } + | ACC_DEF acc_decl ';' + | INIT_DEF init_decl ';' + ; + +string: STRING + | UNTERMINATED_STRING + { + error_list.push_back(spot::evtgba_parse_error(@1, + "unterminated string")); + } + +strident: string | IDENT + +acc_list: + { + $$ = new spot::rsymbol_set; + } + | acc_list strident + { + $1->insert(spot::rsymbol(*$2)); + delete $2; + } + ; + +acc_decl: + | acc_decl strident + { + result->declare_acceptance_condition(*$2); + delete $2; + } + ; + +init_decl: + | init_decl strident + { + result->set_init_state(*$2); + delete $2; + } + ; + +%% + +void +yy::Parser::print_() +{ + if (looka_ == STRING || looka_ == IDENT) + YYCDEBUG << " '" << *value.str << "'"; +} + +void +yy::Parser::error_() +{ + error_list.push_back(spot::evtgba_parse_error(location, message)); +} + +namespace spot +{ + evtgba_explicit* + evtgba_parse(const std::string& name, + evtgba_parse_error_list& error_list, + bool debug) + { + if (evtgbayyopen(name)) + { + error_list.push_back + (evtgba_parse_error(yy::Location(), + std::string("Cannot open file ") + name)); + return 0; + } + evtgba_explicit* result = new evtgba_explicit(); + evtgbayy::Parser parser(debug, yy::Location(), error_list, result); + parser.parse(); + evtgbayyclose(); + return result; + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/evtgbaparse/evtgbascan.ll b/src/evtgbaparse/evtgbascan.ll new file mode 100644 index 000000000..a25dd3e64 --- /dev/null +++ b/src/evtgbaparse/evtgbascan.ll @@ -0,0 +1,119 @@ +/* Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +** département Systèmes Répartis Coopératifs (SRC), Université Pierre +** et Marie Curie. +** +** This file is part of Spot, a model checking library. +** +** Spot is free software; you can redistribute it and/or modify it +** under the terms of the GNU General Public License as published by +** the Free Software Foundation; either version 2 of the License, or +** (at your option) any later version. +** +** Spot is distributed in the hope that it will be useful, but WITHOUT +** ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +** or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +** License for more details. +** +** You should have received a copy of the GNU General Public License +** along with Spot; see the file COPYING. If not, write to the Free +** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +** 02111-1307, USA. +*/ +%option noyywrap +%option prefix="evtgbayy" +%option outfile="lex.yy.c" +%x STATE_STRING + +%{ +#include +#include "evtgbaparse/parsedecl.hh" + +#define YY_USER_ACTION \ + yylloc->columns(yyleng); + +#define YY_USER_INIT \ + do { \ + yylloc->begin.filename = current_file; \ + yylloc->end.filename = current_file; \ + } while (0) + +#define YY_NEVER_INTERACTIVE 1 + +static std::string current_file; + +%} + +eol \n|\r|\n\r|\r\n + +%% + +%{ + yylloc->step (); +%} + +acc[ \t]*= return ACC_DEF; +init[ \t]*= return INIT_DEF; + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->str = new std::string(yytext); + return IDENT; + } + + /* discard whitespace */ +{eol} yylloc->lines(yyleng); yylloc->step(); +[ \t]+ yylloc->step(); + +\" { + yylval->str = new std::string; + BEGIN(STATE_STRING); + } + +. return *yytext; + + /* Handle \" and \\ in strings. */ +{ + \" { + BEGIN(INITIAL); + return STRING; + } + \\["\\] yylval->str->append(1, yytext[1]); + [^"\\]+ yylval->str->append(yytext, yyleng); + <> { + BEGIN(INITIAL); + return UNTERMINATED_STRING; + } +} + +%{ + /* Dummy use of yyunput to shut up a gcc warning. */ + (void) &yyunput; +%} + +%% + +namespace spot +{ + int + evtgbayyopen(const std::string &name) + { + if (name == "-") + { + yyin = stdin; + current_file = "standard input"; + } + else + { + yyin = fopen (name.c_str (), "r"); + current_file = name; + if (!yyin) + return 1; + } + return 0; + } + + void + evtgbayyclose() + { + fclose(yyin); + } +} diff --git a/src/evtgbaparse/fmterror.cc b/src/evtgbaparse/fmterror.cc new file mode 100644 index 000000000..2469a47dd --- /dev/null +++ b/src/evtgbaparse/fmterror.cc @@ -0,0 +1,42 @@ +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "public.hh" + +namespace spot +{ + bool + format_evtgba_parse_errors(std::ostream& os, + evtgba_parse_error_list& error_list) + { + bool printed = false; + spot::evtgba_parse_error_list::iterator it; + for (it = error_list.begin(); it != error_list.end(); ++it) + { + if (it->first.begin.filename != "") + os << it->first << ": "; + os << it->second << std::endl; + printed = true; + } + return printed; + } +} diff --git a/src/evtgbaparse/parsedecl.hh b/src/evtgbaparse/parsedecl.hh new file mode 100644 index 000000000..8843c1f8d --- /dev/null +++ b/src/evtgbaparse/parsedecl.hh @@ -0,0 +1,53 @@ +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAPARSE_PARSEDECL_HH +# define SPOT_EVTGBAPARSE_PARSEDECL_HH + +#include +#include "evtgbaparse.hh" +#include "location.hh" + +# define YY_DECL \ + int evtgbayylex (yystype *yylval, yy::Location *yylloc) +YY_DECL; + +namespace spot +{ + int evtgbayyopen(const std::string& name); + void evtgbayyclose(); +} + + +// Gross kludge to compile yy::Parser in another namespace (tgbayy::) +// but still use yy::Location. The reason is that Bison's C++ +// skeleton does not support anything close to %name-prefix at the +// moment. All parser are named yy::Parser which makes it somewhat +// difficult to define multiple parsers. +namespace evtgbayy +{ + using namespace yy; +} +#define yy evtgbayy + + + +#endif // SPOT_EVTGBAPARSE_PARSEDECL_HH diff --git a/src/evtgbaparse/public.hh b/src/evtgbaparse/public.hh new file mode 100644 index 000000000..232b589df --- /dev/null +++ b/src/evtgbaparse/public.hh @@ -0,0 +1,68 @@ +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_EVTGBAPARSE_PUBLIC_HH +# define SPOT_EVTGBAPARSE_PUBLIC_HH + +# include "evtgba/explicit.hh" +# include "ltlparse/location.hh" +# include +# include +# include +# include + +namespace spot +{ + /// \brief A parse diagnostic with its location. + typedef std::pair evtgba_parse_error; + /// \brief A list of parser diagnostics, as filled by parse. + typedef std::list evtgba_parse_error_list; + + /// \brief Build a spot::evtgba_explicit from a text file. + /// \param filename The name of the file to parse. + /// \param error_list A list that will be filled with + /// parse errors that occured during parsing. + /// \param dict The BDD dictionary where to use. + /// \param env The environment into which parsing should take place. + /// \param debug When true, causes the parser to trace its execution. + /// \return A pointer to the evtgba built from \a filename, or + /// 0 if the file could not be opened. + /// + /// Note that the parser usually tries to recover from errors. It can + /// return an non zero value even if it encountered error during the + /// parsing of \a filename. If you want to make sure \a filename + /// was parsed succesfully, check \a error_list for emptiness. + /// + /// \warning This function is not reentrant. + evtgba_explicit* evtgba_parse(const std::string& filename, + evtgba_parse_error_list& error_list, + bool debug = false); + + /// \brief Format diagnostics produced by spot::evtgba_parse. + /// \param os Where diagnostics should be output. + /// \param error_list The error list filled by spot::ltl::parse while + /// parsing \a ltl_string. + /// \return \c true iff any diagnostic was output. + bool format_evtgba_parse_errors(std::ostream& os, + evtgba_parse_error_list& error_list); +} + +#endif // SPOT_EVTGBAPARSE_PUBLIC_HH diff --git a/src/evtgbatest/.cvsignore b/src/evtgbatest/.cvsignore new file mode 100644 index 000000000..021385811 --- /dev/null +++ b/src/evtgbatest/.cvsignore @@ -0,0 +1,10 @@ +.deps +Makefile +Makefile.in +defs +explicit +.libs +readsave +product +*.ps +*.dot diff --git a/src/evtgbatest/Makefile.am b/src/evtgbatest/Makefile.am new file mode 100644 index 000000000..d991a0434 --- /dev/null +++ b/src/evtgbatest/Makefile.am @@ -0,0 +1,45 @@ +## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +## département Systèmes Répartis Coopératifs (SRC), Université Pierre +## et Marie Curie. +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) +LDADD = ../libspot.la + +check_SCRIPTS = defs +# Keep this sorted alphabetically. +check_PROGRAMS = \ + explicit \ + product \ + readsave + +# Keep this sorted alphabetically. +explicit_SOURCES = explicit.cc +product_SOURCES = product.cc +readsave_SOURCES = readsave.cc + +# Keep this sorted by STRENGTH. Test basic things first, +# because such failures will be easier to diagnose and fix. +TESTS = \ + explicit.test \ + readsave.test \ + product.test + +EXTRA_DIST = $(TESTS) diff --git a/src/evtgbatest/defs.in b/src/evtgbatest/defs.in new file mode 100644 index 000000000..106f785bb --- /dev/null +++ b/src/evtgbatest/defs.in @@ -0,0 +1,79 @@ +# -*- shell-script -*- +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + +# 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@' +top_builddir='@top_builddir@' +LBTT="@LBTT@" +LBTT_TRANSLATE="@LBTT_TRANSLATE@" +VALGRIND='@VALGRIND@' + +run() +{ + expected_exitcode=$1 + shift + exitcode=0 + if test -n "$VALGRIND"; then + exec 6>valgrind.err + GLIBCPP_FORCE_NEW=1 \ + ../../libtool --mode=execute \ + $VALGRIND --tool=memcheck --leak-check=yes --logfile-fd=6 -q "$@" || + exitcode=$? + cat valgrind.err 1>&2 + test -z "`sed 1q valgrind.err`" || exit 50 + rm -f valgrind.err + else + "$@" || exitcode=$? + fi + test $exitcode = $expected_exitcode || exit 1 +} + +# Turn on shell traces when VERBOSE=x. +if test "x$VERBOSE" = xx; then + set -x +else + : +fi diff --git a/src/evtgbatest/explicit.cc b/src/evtgbatest/explicit.cc new file mode 100644 index 000000000..27e045a4f --- /dev/null +++ b/src/evtgbatest/explicit.cc @@ -0,0 +1,58 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include "evtgba/explicit.hh" +#include "evtgbaalgos/dotty.hh" + +int +main() +{ + { + const spot::rsymbol a1("a1"); + const spot::rsymbol a2("a2"); + const spot::rsymbol a3("a3"); + + { + spot::rsymbol_set s1; + spot::rsymbol_set s2; + s2.insert(a1); + spot::rsymbol_set s3; + s3.insert(a3); + s3.insert(a2); + + spot::evtgba_explicit* a = new spot::evtgba_explicit(); + + a->add_transition("state 0", "e1", s1, "state 1"); + a->add_transition("state 1", "e2", s2, "state 2"); + a->add_transition("state 2", "e3", s3, "state 1"); + + a->set_init_state("state 0"); + a->set_init_state("state 2"); + + spot::dotty_reachable(std::cout, a); + + delete a; + } + } + spot::symbol::dump_instances(std::cout); +} diff --git a/src/evtgbatest/explicit.test b/src/evtgbatest/explicit.test new file mode 100755 index 000000000..4bec875b6 --- /dev/null +++ b/src/evtgbatest/explicit.test @@ -0,0 +1,49 @@ +#!/bin/sh +# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +run 0 ./explicit > stdout + +perl -pi -e 's/a3, a2/a2, a3/;' stdout + +cat >expected <<\EOF +digraph G { + "*1" [label="", style=invis, height=0] + "*1" -> 1 + "*2" [label="", style=invis, height=0] + "*2" -> 2 + 1 [label="state 0"] + 1 -> 3 [label="e1\n"] + 2 [label="state 2"] + 2 -> 3 [label="e3\n{a2, a3}"] + 3 [label="state 1"] + 3 -> 2 [label="e2\n{a1}"] +} +EOF + +diff stdout expected + +rm stdout expected diff --git a/src/evtgbatest/product.cc b/src/evtgbatest/product.cc new file mode 100644 index 000000000..2e3d1524c --- /dev/null +++ b/src/evtgbatest/product.cc @@ -0,0 +1,99 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include "evtgbaparse/public.hh" +#include "evtgbaalgos/save.hh" +#include "evtgbaalgos/dotty.hh" +#include "evtgba/product.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] [-D] filenames..." << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug = false; + bool dotty = false; + int filename_index = 1; + + while (argv[filename_index][0] == '-' && filename_index < argc) + { + if (!strcmp(argv[filename_index], "-d")) + debug = true; + else if (!strcmp(argv[filename_index], "-D")) + dotty = true; + else + syntax(argv[0]); + ++filename_index; + } + + if (filename_index == argc) + syntax(argv[0]); + + spot::evtgba_product::evtgba_product_operands op; + + while (filename_index < argc) + { + spot::evtgba_parse_error_list pel; + spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], + pel, debug); + + exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); + + if (a) + { + op.push_back(a); + } + else + { + exit_code = 1; + } + + ++filename_index; + } + + if (op.empty()) + return exit_code; + + spot::evtgba_product p(op); + + if (dotty) + spot::dotty_reachable(std::cout, &p); + else + spot::evtgba_save_reachable(std::cout, &p); + + for (spot::evtgba_product::evtgba_product_operands::iterator i = op.begin(); + i != op.end(); ++i) + delete *i; + + return exit_code; +} diff --git a/src/evtgbatest/product.test b/src/evtgbatest/product.test new file mode 100755 index 000000000..38bf5766e --- /dev/null +++ b/src/evtgbatest/product.test @@ -0,0 +1,69 @@ +#!/bin/sh +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +cat >input1 <<\EOF +acc = ; +init = s1; +s1, s2, a, ; +s2, s1, d, ; +EOF + +cat >input2 <<\EOF +acc = Acc3 ; +init = t1; +t1, t2, a, ; +t2, t3, b, ; +t3, t1, c, Acc2; +EOF + +cat >input3 <<\EOF +acc = Acc1 Acc2 ; +init = u1 u2; +u1, u2, c, Acc1; +u2, u1, b, Acc2; +EOF + +run 0 ./product input1 input2 input3 >stdout + +perl -pi -e 's/Acc2 Acc1/Acc1 Acc2/g;' stdout + +cat >expected <<\EOF +acc = Acc3 Acc1 Acc2; +init = "" ""; +"", "", a,; +"", "", a,; +"", "", d,; +"", "", b, Acc2; +"", "", d,; +"", "", c, Acc1 Acc2; +"", "", d,; +"", "", b, Acc2; +"", "", d,; +"", "", c, Acc1 Acc2; +EOF + +diff stdout expected diff --git a/src/evtgbatest/readsave.cc b/src/evtgbatest/readsave.cc new file mode 100644 index 000000000..1b8bb0ac6 --- /dev/null +++ b/src/evtgbatest/readsave.cc @@ -0,0 +1,70 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include +#include "evtgbaparse/public.hh" +#include "evtgbaalgos/save.hh" + +void +syntax(char* prog) +{ + std::cerr << prog << " [-d] filename" << std::endl; + exit(2); +} + +int +main(int argc, char** argv) +{ + int exit_code = 0; + + if (argc < 2) + syntax(argv[0]); + + bool debug = false; + int filename_index = 1; + + if (!strcmp(argv[1], "-d")) + { + debug = true; + if (argc < 3) + syntax(argv[0]); + filename_index = 2; + } + + spot::evtgba_parse_error_list pel; + spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index], + pel, debug); + + exit_code = spot::format_evtgba_parse_errors(std::cerr, pel); + + if (a) + { + spot::evtgba_save_reachable(std::cout, a); + delete a; + } + else + { + exit_code = 1; + } + + return exit_code; +} diff --git a/src/evtgbatest/readsave.test b/src/evtgbatest/readsave.test new file mode 100755 index 000000000..93338d432 --- /dev/null +++ b/src/evtgbatest/readsave.test @@ -0,0 +1,59 @@ +#!/bin/sh +# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +# département Systèmes Répartis Coopératifs (SRC), Université Pierre +# et Marie Curie. +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 2 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with Spot; see the file COPYING. If not, write to the Free +# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +# 02111-1307, USA. + + +. ./defs + +set -e + +cat >input <<\EOF +acc = d; +init = s1; +s1, "s2", e1, c; +"s2", "state 3", "\"he\\llo\"", c; +"state 3", "s1",e4,; +EOF + +./readsave input > stdout + +cat >expected <<\EOF +acc = c d; +init = s1; +s1, s2, e1, c; +s2, "state 3", "\"he\\llo\"", c; +"state 3", s1, e4,; +EOF + +# Sort out some possible inversions in the output. +# (The order is not guaranteed by SPOT.) +sed 's/d c/c d/g' stdout > tmp_ && mv tmp_ stdout + +diff stdout expected + +mv stdout input +run 0 ./readsave input > stdout + +sed 's/d c/c d/g' stdout > tmp_ && mv tmp_ stdout + +diff input stdout + +rm input stdout expected