diff --git a/README b/README index 5e6f249ad..dda77999f 100644 --- a/README +++ b/README @@ -171,7 +171,6 @@ src/ Sources for libspot. ta/ TA objects and cousins (TGTA). taalgos/ Algorithms on TA/TGTA. tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/. - evtgba*/ Ignore these for now. eltlparse/ Parser for ELTL formulae. eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/. saba/ SABA (State-labeled Alternating Büchi Automata) objects. @@ -223,7 +222,7 @@ End: LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL - LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm + LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC LocalWords: formulae optimizations kripkeparse kripketest Automata LocalWords: neverparse ltlcounter ltlclasses parallelizing automata diff --git a/configure.ac b/configure.ac index 24f705b9b..a29cb3c9d 100644 --- a/configure.ac +++ b/configure.ac @@ -131,11 +131,6 @@ AC_CONFIG_FILES([ src/eltlparse/Makefile src/eltltest/defs src/eltltest/Makefile - src/evtgbaalgos/Makefile - src/evtgba/Makefile - src/evtgbaparse/Makefile - src/evtgbatest/defs - src/evtgbatest/Makefile src/kripke/Makefile src/ltlast/Makefile src/ltlenv/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index ad6daf042..78de8ff2c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,6 +1,6 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). +## Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et +## Développement de l'Epita (LRDE). ## 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. @@ -26,10 +26,9 @@ AUTOMAKE_OPTIONS = subdir-objects # end, after building '.' (since the current directory contains # libspot.la needed by the tests) SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \ - tgbaalgos tgbaparse ta taalgos evtgba evtgbaalgos \ - evtgbaparse kripke saba sabaalgos neverparse kripkeparse \ - . bin ltltest eltltest tgbatest evtgbatest sabatest sanity \ - kripketest + tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \ + neverparse kripkeparse . bin ltltest eltltest tgbatest \ + sabatest sanity kripketest lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -47,9 +46,6 @@ libspot_la_LIBADD = \ taalgos/libtaalgos.la \ tgbaparse/libtgbaparse.la \ neverparse/libneverparse.la \ - evtgba/libevtgba.la \ - evtgbaalgos/libevtgbaalgos.la \ - evtgbaparse/libevtgbaparse.la \ saba/libsaba.la \ sabaalgos/libsabaalgos.la \ kripke/libkripke.la \ diff --git a/src/evtgba/.cvsignore b/src/evtgba/.cvsignore deleted file mode 100644 index 799fc9785..000000000 --- a/src/evtgba/.cvsignore +++ /dev/null @@ -1,6 +0,0 @@ -.deps -.libs -*.lo -*.la -Makefile -Makefile.in diff --git a/src/evtgba/.gitignore b/src/evtgba/.gitignore deleted file mode 100644 index 799fc9785..000000000 --- a/src/evtgba/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -.deps -.libs -*.lo -*.la -Makefile -Makefile.in diff --git a/src/evtgba/Makefile.am b/src/evtgba/Makefile.am deleted file mode 100644 index 9c509c2b5..000000000 --- a/src/evtgba/Makefile.am +++ /dev/null @@ -1,39 +0,0 @@ -## Copyright (C) 2011 Laboratoire de Recherche et Developpement de -## l'Epita (LRDE). -## 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 3 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 this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(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 deleted file mode 100644 index c91bc6a14..000000000 --- a/src/evtgba/evtgba.cc +++ /dev/null @@ -1,67 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index c56ed9c1d..000000000 --- a/src/evtgba/evtgba.hh +++ /dev/null @@ -1,69 +0,0 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#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 - /// that 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 deleted file mode 100644 index 6b4a5667f..000000000 --- a/src/evtgba/evtgbaiter.hh +++ /dev/null @@ -1,48 +0,0 @@ -// Copyright (C) 2004, 2005 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 3 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 this program. If not, see . - -#ifndef SPOT_EVTGBA_EVTGBAITER_HH -# define SPOT_EVTGBA_EVTGBAITER_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_EVTGBAITER_HH diff --git a/src/evtgba/explicit.cc b/src/evtgba/explicit.cc deleted file mode 100644 index 7b6b03c7d..000000000 --- a/src/evtgba/explicit.cc +++ /dev/null @@ -1,284 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE) -// 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 3 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 this program. If not, see . - -#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 = - down_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 = - down_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 = - down_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 = - down_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 deleted file mode 100644 index 913bb411f..000000000 --- a/src/evtgba/explicit.hh +++ /dev/null @@ -1,110 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index c69239dea..000000000 --- a/src/evtgba/product.cc +++ /dev/null @@ -1,461 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement de -// l'Epita (LRDE) -// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#include "product.hh" -#include "misc/hashfunc.hh" -#include "misc/modgray.hh" -#include -#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) - s_[j]->destroy(); - 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 = - down_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 - { - size_t res = 0; - for (int i = 0; i != n_; ++i) - res ^= wang32_hash(s_[i]->hash()); - 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 = - down_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 = - down_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 = - down_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 deleted file mode 100644 index 188191e37..000000000 --- a/src/evtgba/product.hh +++ /dev/null @@ -1,69 +0,0 @@ -// Copyright (C) 2009 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#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 - /// that 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 deleted file mode 100644 index b58a1e607..000000000 --- a/src/evtgba/symbol.cc +++ /dev/null @@ -1,107 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index 07b83170a..000000000 --- a/src/evtgba/symbol.hh +++ /dev/null @@ -1,124 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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_; - } - - 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 deleted file mode 100644 index 799fc9785..000000000 --- a/src/evtgbaalgos/.cvsignore +++ /dev/null @@ -1,6 +0,0 @@ -.deps -.libs -*.lo -*.la -Makefile -Makefile.in diff --git a/src/evtgbaalgos/.gitignore b/src/evtgbaalgos/.gitignore deleted file mode 100644 index 799fc9785..000000000 --- a/src/evtgbaalgos/.gitignore +++ /dev/null @@ -1,6 +0,0 @@ -.deps -.libs -*.lo -*.la -Makefile -Makefile.in diff --git a/src/evtgbaalgos/Makefile.am b/src/evtgbaalgos/Makefile.am deleted file mode 100644 index 17a9befa4..000000000 --- a/src/evtgbaalgos/Makefile.am +++ /dev/null @@ -1,38 +0,0 @@ -## Copyright (C) 2011 Laboratoire de Recherche et Developpement de -## l'Epita (LRDE). -## 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 3 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 this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) - -evtgbaalgosdir = $(pkgincludedir)/evtgbaalgos - -evtgbaalgos_HEADERS = \ - dotty.hh \ - reachiter.hh \ - save.hh \ - tgba2evtgba.hh - -noinst_LTLIBRARIES = libevtgbaalgos.la -libevtgbaalgos_la_SOURCES = \ - dotty.cc \ - reachiter.cc \ - save.cc \ - tgba2evtgba.cc diff --git a/src/evtgbaalgos/dotty.cc b/src/evtgbaalgos/dotty.cc deleted file mode 100644 index eae1e7f92..000000000 --- a/src/evtgbaalgos/dotty.cc +++ /dev/null @@ -1,91 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index 11438403c..000000000 --- a/src/evtgbaalgos/dotty.hh +++ /dev/null @@ -1,32 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index 692d38f10..000000000 --- a/src/evtgbaalgos/reachiter.cc +++ /dev/null @@ -1,160 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#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; - ptr->destroy(); - } - } - - 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); - current->destroy(); - } - } - 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 deleted file mode 100644 index 5c8e8343e..000000000 --- a/src/evtgbaalgos/reachiter.hh +++ /dev/null @@ -1,119 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100644 index 8c738853c..000000000 --- a/src/evtgbaalgos/save.cc +++ /dev/null @@ -1,102 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#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)); - s->destroy(); - } - 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; - dest->destroy(); - } - } - - private: - std::ostream& os_; - - void - output_acc_set(const symbol_set& ss) const - { - // Store all formated acceptance condition in a set to sort - // them in the output. - typedef std::set acc_set; - acc_set acc; - for (symbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i) - acc.insert(automata_->format_acceptance_condition(*i)); - for (acc_set::const_iterator i = acc.begin(); i != acc.end(); ++i) - os_ << " " << quote_unless_bare_word(*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 deleted file mode 100644 index fd498c282..000000000 --- a/src/evtgbaalgos/save.hh +++ /dev/null @@ -1,32 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc deleted file mode 100644 index 1c8c17717..000000000 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ /dev/null @@ -1,152 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#include "tgba2evtgba.hh" -#include "tgba/tgba.hh" -#include "evtgba/explicit.hh" -#include "tgbaalgos/reachiter.hh" -#include "ltlvisit/tostring.hh" - -namespace spot -{ - namespace - { - class tgba_to_evtgba_iter: - public tgba_reachable_iterator_depth_first - { - public: - tgba_to_evtgba_iter(const tgba* a) - : tgba_reachable_iterator_depth_first(a) - { - res = new evtgba_explicit; - } - - ~tgba_to_evtgba_iter() - { - } - - virtual void - start() - { - const rsymbol_set ss = - acc_to_symbol_set(aut_->all_acceptance_conditions()); - for (rsymbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i) - res->declare_acceptance_condition(*i); - } - - virtual void - process_state(const state* s, int n, tgba_succ_iterator*) - { - std::string str = this->aut_->format_state(s); - name_[n] = str; - if (n == 1) - res->set_init_state(str); - } - - virtual void - process_link(const state*, int in, - const state*, int out, - const tgba_succ_iterator* si) - { - // We might need to format out before process_state is called. - name_map_::const_iterator i = name_.find(out); - if (i == name_.end()) - { - const state* s = si->current_state(); - process_state(s, out, 0); - s->destroy(); - } - - rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions()); - - bdd all = si->current_condition(); - while (all != bddfalse) - { - bdd one = bdd_satone(all); - all -= one; - while (one != bddfalse) - { - bdd low = bdd_low(one); - if (low == bddfalse) - { - const ltl::formula* v = - aut_->get_dict()->bdd_map[bdd_var(one)].f; - res->add_transition(name_[in], - to_string(v), - ss, - name_[out]); - break; - } - else - { - one = low; - } - } - assert(one != bddfalse); - } - } - - evtgba_explicit* res; - protected: - typedef std::map name_map_; - name_map_ name_; - - rsymbol_set - acc_to_symbol_set(bdd acc) const - { - rsymbol_set ss; - while (acc != bddfalse) - { - bdd one = bdd_satone(acc); - acc -= one; - while (one != bddfalse) - { - bdd low = bdd_low(one); - if (low == bddfalse) - { - const ltl::formula* v = - aut_->get_dict()->bdd_map[bdd_var(one)].f; - ss.insert(rsymbol(to_string(v))); - break; - } - else - { - one = low; - } - } - assert(one != bddfalse); - } - return ss; - } - - }; - - } // anonymous - - evtgba_explicit* - tgba_to_evtgba(const tgba* a) - { - tgba_to_evtgba_iter i(a); - i.run(); - return i.res; - } -} // spot diff --git a/src/evtgbaalgos/tgba2evtgba.hh b/src/evtgbaalgos/tgba2evtgba.hh deleted file mode 100644 index 195256c7b..000000000 --- a/src/evtgbaalgos/tgba2evtgba.hh +++ /dev/null @@ -1,35 +0,0 @@ -// 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 3 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 this program. If not, see . - -#ifndef SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH -# define SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH - -namespace spot -{ - class tgba; - class evtgba_explicit; - - /// \brief Convert a tgba into an evtgba. - /// - /// (This cannot be done on-the-fly because the alphabet of a tgba - /// as unknown beforehand.) - evtgba_explicit* tgba_to_evtgba(const tgba* a); -} - -#endif // SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH diff --git a/src/evtgbaparse/.cvsignore b/src/evtgbaparse/.cvsignore deleted file mode 100644 index 9a1c7773f..000000000 --- a/src/evtgbaparse/.cvsignore +++ /dev/null @@ -1,13 +0,0 @@ -.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/.gitignore b/src/evtgbaparse/.gitignore deleted file mode 100644 index 9a1c7773f..000000000 --- a/src/evtgbaparse/.gitignore +++ /dev/null @@ -1,13 +0,0 @@ -.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 deleted file mode 100644 index 55934693b..000000000 --- a/src/evtgbaparse/Makefile.am +++ /dev/null @@ -1,64 +0,0 @@ -## Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et -## Développement de l'Epita (LRDE). -## Copyright (C) 2004, 2006 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 3 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 this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT -# Disable -Werror because too many versions of flex yield warnings. -AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) - -evtgbaparsedir = $(pkgincludedir)/evtgbaparse - -evtgbaparse_HEADERS = \ - public.hh \ - location.hh \ - position.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 -Wall -Werror --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 deleted file mode 100644 index 171e9d7ed..000000000 --- a/src/evtgbaparse/evtgbaparse.yy +++ /dev/null @@ -1,156 +0,0 @@ -/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -** de l'Epita (LRDE). -** Copyright (C) 2004, 2005, 2006 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 3 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 this program. If not, see . -*/ -%language "C++" -%locations -%defines -%name-prefix "evtgbayy" -%debug -%error-verbose - -%code requires -{ -#include -#include "public.hh" -#include "evtgba/symbol.hh" -} - -%parse-param {spot::evtgba_parse_error_list &error_list} -%parse-param {spot::evtgba_explicit* &result} -%union -{ - int token; - std::string* str; - spot::rsymbol_set* symset; -} - -%code -{ -/* 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" -} - -%token STRING UNTERMINATED_STRING -%token IDENT -%type strident string -%type acc_list -%token ACC_DEF -%token INIT_DEF - -%destructor { delete $$; } - -%printer { debug_stream() << *$$; } - -%% -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 - { - $$ = $1; - 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 -evtgbayy::parser::error(const location_type& location, - const std::string& message) -{ - 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(evtgbayy::location(), - std::string("Cannot open file ") + name)); - return 0; - } - evtgba_explicit* result = new evtgba_explicit(); - evtgbayy::parser parser(error_list, result); - parser.set_debug_level(debug); - parser.parse(); - evtgbayyclose(); - return result; - } -} - -// Local Variables: -// mode: c++ -// End: diff --git a/src/evtgbaparse/evtgbascan.ll b/src/evtgbaparse/evtgbascan.ll deleted file mode 100644 index 0029f0b3a..000000000 --- a/src/evtgbaparse/evtgbascan.ll +++ /dev/null @@ -1,110 +0,0 @@ -/* Copyright (C) 2011, Laboratoire de Recherche et Développement de -** l'Epita (LRDE). -** Copyright (C) 2004, 2005 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 3 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 this program. If not, see . -*/ -%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_NEVER_INTERACTIVE 1 - -typedef evtgbayy::parser::token token; -%} - -eol \n|\r|\n\r|\r\n - -%% - -%{ - yylloc->step (); -%} - -acc[ \t]*= return token::ACC_DEF; -init[ \t]*= return token::INIT_DEF; - -[a-zA-Z_.][a-zA-Z0-9_.]* { - yylval->str = new std::string(yytext); - return token::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 token::STRING; - } - \\["\\] yylval->str->append(1, yytext[1]); - [^"\\]+ yylval->str->append(yytext, yyleng); - <> { - BEGIN(INITIAL); - return token::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; - } - else - { - yyin = fopen (name.c_str (), "r"); - if (!yyin) - return 1; - } - return 0; - } - - void - evtgbayyclose() - { - fclose(yyin); - } -} diff --git a/src/evtgbaparse/fmterror.cc b/src/evtgbaparse/fmterror.cc deleted file mode 100644 index ca84c0d1d..000000000 --- a/src/evtgbaparse/fmterror.cc +++ /dev/null @@ -1,42 +0,0 @@ -// Copyright (C) 2003, 2004, 2005 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 3 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 this program. If not, see . - -#include -#include "public.hh" - -namespace spot -{ - bool - format_evtgba_parse_errors(std::ostream& os, - const std::string& filename, - 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 (filename != "-") - os << 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 deleted file mode 100644 index deab799f9..000000000 --- a/src/evtgbaparse/parsedecl.hh +++ /dev/null @@ -1,39 +0,0 @@ -// Copyright (C) 2003, 2004, 2005 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 3 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 this program. If not, see . - -#ifndef SPOT_EVTGBAPARSE_PARSEDECL_HH -# define SPOT_EVTGBAPARSE_PARSEDECL_HH - -#include -#include "evtgbaparse.hh" -#include "location.hh" - -# define YY_DECL \ - int evtgbayylex (evtgbayy::parser::semantic_type *yylval, \ - evtgbayy::location *yylloc) -YY_DECL; - -namespace spot -{ - int evtgbayyopen(const std::string& name); - void evtgbayyclose(); -} - - -#endif // SPOT_EVTGBAPARSE_PARSEDECL_HH diff --git a/src/evtgbaparse/public.hh b/src/evtgbaparse/public.hh deleted file mode 100644 index 89f304764..000000000 --- a/src/evtgbaparse/public.hh +++ /dev/null @@ -1,69 +0,0 @@ -// Copyright (C) 2003, 2004, 2005, 2006 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 3 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 this program. If not, see . - -#ifndef SPOT_EVTGBAPARSE_PUBLIC_HH -# define SPOT_EVTGBAPARSE_PUBLIC_HH - -# include "evtgba/explicit.hh" -// Unfortunately Bison 2.3 uses the same guards in all parsers :( -# undef BISON_LOCATION_HH -# undef BISON_POSITION_HH -# include "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 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 filename The filename that should appear in the diagnostics. - /// \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, - const std::string& filename, - evtgba_parse_error_list& error_list); -} - -#endif // SPOT_EVTGBAPARSE_PUBLIC_HH diff --git a/src/evtgbatest/.cvsignore b/src/evtgbatest/.cvsignore deleted file mode 100644 index 021385811..000000000 --- a/src/evtgbatest/.cvsignore +++ /dev/null @@ -1,10 +0,0 @@ -.deps -Makefile -Makefile.in -defs -explicit -.libs -readsave -product -*.ps -*.dot diff --git a/src/evtgbatest/.gitignore b/src/evtgbatest/.gitignore deleted file mode 100644 index 6aded371c..000000000 --- a/src/evtgbatest/.gitignore +++ /dev/null @@ -1,15 +0,0 @@ -.deps -Makefile -Makefile.in -defs -explicit -.libs -readsave -product -*.ps -*.dot -expected -input* -ltl2evtgba -stdout -*.err diff --git a/src/evtgbatest/Makefile.am b/src/evtgbatest/Makefile.am deleted file mode 100644 index a44d64e83..000000000 --- a/src/evtgbatest/Makefile.am +++ /dev/null @@ -1,51 +0,0 @@ -## Copyright (C) 2011 Laboratoire de Recherche et Developpement de -## l'Epita (LRDE). -## 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 3 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 this program. If not, see . - -AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = ../libspot.la - -check_SCRIPTS = defs -# Keep this sorted alphabetically. -check_PROGRAMS = \ - ltl2evtgba \ - explicit \ - product \ - readsave - -# Keep this sorted alphabetically. -ltl2evtgba_SOURCES = ltl2evtgba.cc -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 \ - ltl2evtgba.test - -EXTRA_DIST = $(TESTS) - -distclean-local: - rm -rf $(TESTS:.test=.dir) diff --git a/src/evtgbatest/defs.in b/src/evtgbatest/defs.in deleted file mode 100644 index ee215e8c9..000000000 --- a/src/evtgbatest/defs.in +++ /dev/null @@ -1,78 +0,0 @@ -# -*- shell-script -*- -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2003, 2004, 2006 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 3 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 this program. If not, see . - -# 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'. -if test -z "$srcdir"; then - # 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 -} - -echo "== Running test $0" - -me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'` - -testSubDir=$me.dir -chmod -R a+rwx $testSubDir > /dev/null 2>&1 -rm -rf $testSubDir > /dev/null 2>&1 -mkdir $testSubDir -cd $testSubDir - -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 --log-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 -} - -set -x diff --git a/src/evtgbatest/explicit.cc b/src/evtgbatest/explicit.cc deleted file mode 100644 index 261646c85..000000000 --- a/src/evtgbatest/explicit.cc +++ /dev/null @@ -1,56 +0,0 @@ -// 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 3 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 this program. If not, see . - -#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 deleted file mode 100755 index 079b5701d..000000000 --- a/src/evtgbatest/explicit.test +++ /dev/null @@ -1,47 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# Copyright (C) 2004, 2005 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 3 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 this program. If not, see . - - -. ./defs - -set -e - -run 0 ../explicit > 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/ltl2evtgba.cc b/src/evtgbatest/ltl2evtgba.cc deleted file mode 100644 index 8182e2617..000000000 --- a/src/evtgbatest/ltl2evtgba.cc +++ /dev/null @@ -1,137 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// 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 3 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 this program. If not, see . - -#include -#include -#include -#include -#include "ltlast/allnodes.hh" -#include "ltlparse/public.hh" -#include "evtgbaparse/public.hh" -#include "evtgbaalgos/save.hh" -#include "evtgbaalgos/dotty.hh" -#include "evtgbaalgos/tgba2evtgba.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " [-d] [-D] formula" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc < 2) - syntax(argv[0]); - - bool debug_opt = false; - bool dotty_opt = false; - - bool post_branching = false; - bool fair_loop_approx = false; - - int formula_index = 1; - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::ltl::atomic_prop_set* unobservables = new spot::ltl::atomic_prop_set; - - while (formula_index < argc && argv[formula_index][0] == '-') - { - if (!strcmp(argv[formula_index], "-d")) - { - debug_opt = true; - } - else if (!strcmp(argv[formula_index], "-D")) - { - dotty_opt = true; - } - else if (!strcmp(argv[formula_index], "-L")) - { - fair_loop_approx = true; - } - else if (!strcmp(argv[formula_index], "-p")) - { - post_branching = true; - } - else if (!strncmp(argv[formula_index], "-U", 2)) - { - // Parse -U's argument. - const char* tok = strtok(argv[formula_index] + 2, ", \t;"); - while (tok) - { - unobservables->insert - (static_cast(env.require(tok))); - tok = strtok(0, ", \t;"); - } - } - else - { - syntax(argv[0]); - } - ++formula_index; - } - - if (formula_index == argc) - syntax(argv[0]); - - spot::bdd_dict* dict = new spot::bdd_dict(); - - const spot::ltl::formula* f = 0; - - { - spot::ltl::parse_error_list pel; - f = spot::ltl::parse(argv[formula_index], pel, env, debug_opt); - exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index], - pel); - } - - if (f) - { - spot::tgba* a = spot::ltl_to_tgba_fm(f, dict, false, true, - post_branching, - fair_loop_approx, unobservables); - - f->destroy(); - spot::evtgba* e = spot::tgba_to_evtgba(a); - - if (dotty_opt) - spot::dotty_reachable(std::cout, e); - else - spot::evtgba_save_reachable(std::cout, e); - - delete e; - delete a; - } - - for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin(); - i != unobservables->end(); ++i) - (*i)->destroy(); - delete unobservables; - - delete dict; - - return exit_code; -} diff --git a/src/evtgbatest/ltl2evtgba.test b/src/evtgbatest/ltl2evtgba.test deleted file mode 100755 index ac553d928..000000000 --- a/src/evtgbatest/ltl2evtgba.test +++ /dev/null @@ -1,49 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# 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 3 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 this program. If not, see . - - -. ./defs - -set -e - -check () -{ - run 0 ../ltl2evtgba "$1" - run 0 ../ltl2evtgba -Uun1,un2,un3 "$1" -} - -# We don't check the output, but just running these might be enough to -# trigger assertions. - -check a -check 'a U b' -check 'X a' -check 'a & b & c' -check 'a | b | (c U (d & (g U (h ^ i))))' -check 'Xa & (b U !a) & (b U !a)' -check 'Fa & Xb & GFc & Gd' -check 'Fa & Xa & GFc & Gc' -check 'Fc & X(a | Xb) & GF(a | Xb) & Gc' -check 'a R (b R c)' -check '(a U b) U (c U d)' - -check '((Xp2)U(X(1)))&(p1 R(p2 R p0))' diff --git a/src/evtgbatest/product.cc b/src/evtgbatest/product.cc deleted file mode 100644 index d5bdcc932..000000000 --- a/src/evtgbatest/product.cc +++ /dev/null @@ -1,104 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2004, 2005 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 3 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 this program. If not, see . - -#include -#include -#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 (filename_index < argc && argv[filename_index][0] == '-') - { - 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, - argv[filename_index], - 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 deleted file mode 100755 index 8e628fad6..000000000 --- a/src/evtgbatest/product.test +++ /dev/null @@ -1,67 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# 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 3 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 this program. If not, see . - - -. ./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 - -cat >expected <<\EOF -acc = Acc1 Acc2 Acc3; -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 deleted file mode 100644 index 08d3e30ae..000000000 --- a/src/evtgbatest/readsave.cc +++ /dev/null @@ -1,73 +0,0 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2004, 2005 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 3 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 this program. If not, see . - -#include -#include -#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, argv[filename_index], - 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 deleted file mode 100755 index 2278f5653..000000000 --- a/src/evtgbatest/readsave.test +++ /dev/null @@ -1,53 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement -# de l'Epita (LRDE). -# 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 3 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 this program. If not, see . - - -. ./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 - -diff stdout expected - -mv stdout input -run 0 ../readsave input > stdout - -diff input stdout - -rm input stdout expected