diff --git a/configure.ac b/configure.ac index c863b26a9..bf61e9db7 100644 --- a/configure.ac +++ b/configure.ac @@ -154,6 +154,8 @@ AC_CONFIG_FILES([ src/tgbaalgos/gtec/Makefile src/tgbaalgos/Makefile src/tgba/Makefile + src/taalgos/Makefile + src/ta/Makefile src/tgbaparse/Makefile src/tgbatest/defs src/tgbatest/Makefile diff --git a/src/Makefile.am b/src/Makefile.am index 46898d037..824ec2fbd 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,7 +1,8 @@ -## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +## -*- coding: utf-8 -*- +## Copyright (C) 2009, 2010, 2012 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 +## département Systèmes Répartis Coopératifs (SRC), Université Pierre ## et Marie Curie. ## ## This file is part of Spot, a model checking library. @@ -25,11 +26,12 @@ AUTOMAKE_OPTIONS = subdir-objects # List directories in the order they must be built. Keep tests at the # end, after building '.' (since the current directory contains -# libspot.la needed by the tests). +# libspot.la needed by the tests) SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \ - tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke \ - saba sabaalgos neverparse kripkeparse . ltltest eltltest \ - tgbatest evtgbatest sabatest sanity kripketest + tgbaalgos tgbaparse ta taalgos evtgba evtgbaalgos \ + evtgbaparse kripke saba sabaalgos neverparse kripkeparse \ + . ltltest eltltest tgbatest evtgbatest sabatest sanity \ + kripketest lib_LTLIBRARIES = libspot.la libspot_la_SOURCES = @@ -43,6 +45,8 @@ libspot_la_LIBADD = \ eltlparse/libeltlparse.la \ tgba/libtgba.la \ tgbaalgos/libtgbaalgos.la \ + ta/libta.la \ + taalgos/libtaalgos.la \ tgbaparse/libtgbaparse.la \ neverparse/libneverparse.la \ evtgba/libevtgba.la \ diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am new file mode 100644 index 000000000..9a9850143 --- /dev/null +++ b/src/ta/Makefile.am @@ -0,0 +1,32 @@ +## Copyright (C) 2010 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). +## +## This file is part of Spot, a model checking library. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +tadir = $(pkgincludedir)/ta + +ta_HEADERS = \ + ta.hh \ + taexplicit.hh + +noinst_LTLIBRARIES = libta.la +libta_la_SOURCES = \ + taexplicit.cc diff --git a/src/ta/ta.hh b/src/ta/ta.hh new file mode 100644 index 000000000..244d8a213 --- /dev/null +++ b/src/ta/ta.hh @@ -0,0 +1,158 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TA_TA_HH +# define SPOT_TA_TA_HH + +#include + +#include +#include "misc/bddlt.hh" +#include "tgba/state.hh" +#include "tgba/succiter.hh" +#include "tgba/bdddict.hh" + +namespace spot +{ + // Forward declarations. See below. + class ta_succ_iterator; + + /// ta representation of a Testing Automata + class ta + { + + public: + virtual + ~ta() + { + } + + typedef std::set states_set_t; + + virtual const states_set_t* + get_initial_states_set() const = 0; + + virtual ta_succ_iterator* + succ_iter(const spot::state* s) const = 0; + + virtual bdd_dict* + get_dict() const = 0; + + virtual std::string + format_state(const spot::state* s) const = 0; + + virtual bool + is_accepting_state(const spot::state* s) const = 0; + + virtual bool + is_livelock_accepting_state(const spot::state* s) const = 0; + + virtual bool + is_initial_state(const spot::state* s) const = 0; + + virtual bdd + get_state_condition(const spot::state* s) const = 0; + + }; + + /// Successor iterators used by spot::ta. + class ta_succ_iterator : public tgba_succ_iterator + { + public: + virtual + ~ta_succ_iterator() + { + } + + virtual void + first() = 0; + virtual void + next() = 0; + virtual bool + done() const = 0; + + virtual state* + current_state() const = 0; + virtual bdd + current_condition() const = 0; + + + bdd + current_acceptance_conditions() const + { + assert(!done()); + return bddfalse; + } + }; + + // A stack of Strongly-Connected Components + class sscc_stack + { + public: + struct connected_component + { + public: + connected_component(int index = -1); + + /// Index of the SCC. + int index; + + bool is_accepting; + + bool is_initial; + + std::list rem; + }; + + /// Stack a new SCC with index \a index. + void + push(int index); + + /// Access the top SCC. + connected_component& + top(); + + /// Access the top SCC. + const connected_component& + top() const; + + /// Pop the top SCC. + void + pop(); + + /// How many SCC are in stack. + size_t + size() const; + + /// The \c rem member of the top SCC. + std::list& + rem(); + + /// Is the stack empty? + bool + empty() const; + + typedef std::list stack_type; + stack_type s; + }; + +} + +#endif // SPOT_TA_TA_HH diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc new file mode 100644 index 000000000..ace94522b --- /dev/null +++ b/src/ta/taexplicit.cc @@ -0,0 +1,379 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "ltlast/atomic_prop.hh" +#include "ltlast/constant.hh" +#include "taexplicit.hh" +#include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" +#include +#include "ltlvisit/tostring.hh" + +#include "tgba/bddprint.hh" + + +namespace spot +{ + + //////////////////////////////////////// + // ta_explicit_succ_iterator + + ta_explicit_succ_iterator::ta_explicit_succ_iterator(const state_ta_explicit* s) + { + transitions_ = s->get_transitions(); + } + + void + ta_explicit_succ_iterator::first() + { + i_ = transitions_->begin(); + } + + void + ta_explicit_succ_iterator::next() + { + ++i_; + } + + bool + ta_explicit_succ_iterator::done() const + { + return i_ == transitions_->end(); + } + + state* + ta_explicit_succ_iterator::current_state() const + { + assert(!done()); + state_ta_explicit* s = (*i_)->dest; + return s; + } + + bdd + ta_explicit_succ_iterator::current_condition() const + { + assert(!done()); + return (*i_)->condition; + } + + + + + //////////////////////////////////////// + // state_ta_explicit + + state_ta_explicit::transitions* + state_ta_explicit::get_transitions() const + { + return transitions_; + } + + + void + state_ta_explicit::add_transition(state_ta_explicit::transition* t){ + if(transitions_ == 0) + transitions_= new transitions; + + transitions_->push_back(t); + + } + + + const state* + state_ta_explicit::get_tgba_state() const + { + return tgba_state_; + } + + const bdd + state_ta_explicit::get_tgba_condition() const + { + return tgba_condition_; + } + + bool + state_ta_explicit::is_accepting_state() const + { + return is_accepting_state_; + } + + bool + state_ta_explicit::is_initial_state() const + { + return is_initial_state_; + } + + void + state_ta_explicit::set_accepting_state(bool is_accepting_state) + { + is_accepting_state_ = is_accepting_state; + } + + bool + state_ta_explicit::is_livelock_accepting_state() const + { + return is_livelock_accepting_state_; + } + + void + state_ta_explicit::set_livelock_accepting_state(bool is_livelock_accepting_state) + { + is_livelock_accepting_state_ = is_livelock_accepting_state; + } + + void + state_ta_explicit::set_initial_state(bool is_initial_state) + { + is_initial_state_ = is_initial_state; + } + + int + state_ta_explicit::compare(const spot::state* other) const + { + const state_ta_explicit* o = dynamic_cast (other); + assert(o); + + int compare_value = tgba_state_->compare(o->tgba_state_); + + if (compare_value != 0) + return compare_value; + + return tgba_condition_.id() - o->tgba_condition_.id(); + } + + size_t + state_ta_explicit::hash() const + { + return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id()); + } + + state_ta_explicit* + state_ta_explicit::clone() const + { + return new state_ta_explicit(*this); + } + + sscc_stack::connected_component::connected_component(int i) + { + index = i; + is_accepting = false; + is_initial = false; + } + + sscc_stack::connected_component& + sscc_stack::top() + { + return s.front(); + } + + const sscc_stack::connected_component& + sscc_stack::top() const + { + return s.front(); + } + + void + sscc_stack::pop() + { + // assert(rem().empty()); + s.pop_front(); + } + + void + sscc_stack::push(int index) + { + s.push_front(connected_component(index)); + } + + std::list& + sscc_stack::rem() + { + return top().rem; + } + + size_t + sscc_stack::size() const + { + return s.size(); + } + + bool + sscc_stack::empty() const + { + return s.empty(); + } + + //////////////////////////////////////// + // ta_explicit + + + ta_explicit::ta_explicit(const tgba* tgba_) : + tgba_(tgba_) + { + } + + ta_explicit::~ta_explicit() + { + ta::states_set_t::iterator it; + for (it = states_set_.begin(); it != states_set_.end(); it++) + { + const state_ta_explicit* s = dynamic_cast (*it); + state_ta_explicit::transitions* trans = s->get_transitions(); + state_ta_explicit::transitions::iterator it_trans; + // We don't destroy the transitions in the state's destructor because + // they are not cloned. + for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++) + { + delete *it_trans; + } + delete trans; + delete s->get_tgba_state(); + delete s; + } + + } + + state_ta_explicit* + ta_explicit::add_state(state_ta_explicit* s) + { + std::pair add_state_to_ta = + states_set_.insert(s); + + if (is_initial_state(*add_state_to_ta.first)) + initial_states_set_.insert(*add_state_to_ta.first); + + return dynamic_cast (*add_state_to_ta.first); + + } + + state_ta_explicit* + ta_explicit::add_initial_state(state_ta_explicit* s) + { + s->set_initial_state(true); + + return add_state(s); + + } + + void + ta_explicit::create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest) + { + state_ta_explicit::transition* t = new state_ta_explicit::transition; + t->dest = dest; + t->condition = condition; + source->add_transition(t); + + } + + const ta::states_set_t* + ta_explicit::get_initial_states_set() const + { + return &initial_states_set_; + + } + + bdd + ta_explicit::get_state_condition(const spot::state* initial_state) const + { + const state_ta_explicit* sta = dynamic_cast (initial_state); + return sta->get_tgba_condition(); + } + + bool + ta_explicit::is_accepting_state(const spot::state* s) const + { + const state_ta_explicit* sta = dynamic_cast (s); + return sta->is_accepting_state(); + } + + bool + ta_explicit::is_initial_state(const spot::state* s) const + { + const state_ta_explicit* sta = dynamic_cast (s); + return sta->is_initial_state(); + } + + bool + ta_explicit::is_livelock_accepting_state(const spot::state* s) const + { + const state_ta_explicit* sta = dynamic_cast (s); + return sta->is_livelock_accepting_state(); + } + + ta_succ_iterator* + ta_explicit::succ_iter(const spot::state* state) const + { + const state_ta_explicit* s = dynamic_cast (state); + assert(s); + return new ta_explicit_succ_iterator(s); + } + + bdd_dict* + ta_explicit::get_dict() const + { + return tgba_->get_dict(); + } + + const tgba* + ta_explicit::get_tgba() const + { + return tgba_; + } + + std::string + ta_explicit::format_state(const spot::state* s) const + { + const state_ta_explicit* sta = dynamic_cast (s); + assert(sta); + return tgba_->format_state(sta->get_tgba_state()) + "\n" + + bdd_format_formula(get_dict(), sta->get_tgba_condition()); + + } + + void + ta_explicit::delete_stuttering_transitions() + { + ta::states_set_t::iterator it; + for (it = states_set_.begin(); it != states_set_.end(); it++) + { + + const state_ta_explicit* source = dynamic_cast (*it); + + state_ta_explicit::transitions* trans = source->get_transitions(); + state_ta_explicit::transitions::iterator it_trans; + + for (it_trans = trans->begin(); it_trans != trans->end();) + { + if (source->get_tgba_condition() + == ((*it_trans)->dest)->get_tgba_condition()) + { + delete *it_trans; + it_trans = trans->erase(it_trans); + } + else + { + it_trans++; + } + } + } + + } + +} diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh new file mode 100644 index 000000000..f6258bc7b --- /dev/null +++ b/src/ta/taexplicit.hh @@ -0,0 +1,197 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita_explicit (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANta_explicitBILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more deta_explicitils. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TA_TAEXPLICIT_HH +# define SPOT_TA_TAEXPLICIT_HH + +#include "misc/hash.hh" +#include +#include "tgba/tgba.hh" +#include +#include "ltlast/formula.hh" +#include +#include "misc/bddlt.hh" +#include "ta.hh" + +namespace spot +{ + // Forward declarations. See below. + class state_ta_explicit; + class ta_explicit_succ_iterator; + class ta_explicit; + + + + /// ta_explicit explicit representa_explicittion of a Testing Automata_explicit + class ta_explicit : public ta + { + public: + ta_explicit(const tgba* tgba_); + + const tgba* + get_tgba() const; + + state_ta_explicit* + add_state(state_ta_explicit* s); + + state_ta_explicit* + add_initial_state(state_ta_explicit* s); + + void + create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest); + + void + delete_stuttering_transitions(); + // ta interface + virtual + ~ta_explicit(); + virtual const states_set_t* + get_initial_states_set() const; + + virtual ta_succ_iterator* + succ_iter(const spot::state* s) const; + + virtual bdd_dict* + get_dict() const; + + virtual std::string + format_state(const spot::state* s) const; + + virtual bool + is_accepting_state(const spot::state* s) const; + + virtual bool + is_livelock_accepting_state(const spot::state* s) const; + + virtual bool + is_initial_state(const spot::state* s) const; + + virtual bdd + get_state_condition(const spot::state* s) const; + + private: + // Disallow copy. + ta_explicit(const ta_explicit& other); + ta_explicit& + operator=(const ta_explicit& other); + + ta::states_set_t states_set_; + ta::states_set_t initial_states_set_; + const tgba* tgba_; + + }; + + /// states used by spot::ta_explicit. + /// \ingroup ta_ + class state_ta_explicit : public spot::state + { + public: + + struct transition + { + bdd condition; + state_ta_explicit* dest; + }; + + typedef std::list transitions; + + state_ta_explicit(const state* tgba_state, const bdd tgba_condition, + bool is_initial_state = false, bool is_accepting_state = false, + bool is_livelock_accepting_state = false, transitions* trans = 0) : + tgba_state_(tgba_state), tgba_condition_(tgba_condition), + is_initial_state_(is_initial_state), is_accepting_state_( + is_accepting_state), is_livelock_accepting_state_( + is_livelock_accepting_state), transitions_(trans) + { + } + + virtual int + compare(const spot::state* other) const; + virtual size_t + hash() const; + virtual state_ta_explicit* + clone() const; + + virtual + ~state_ta_explicit() + { + } + + transitions* + get_transitions() const; + + void + add_transition(transition* t); + + const state* + get_tgba_state() const; + const bdd + get_tgba_condition() const; + bool + is_accepting_state() const; + void + set_accepting_state(bool is_accepting_state); + bool + is_livelock_accepting_state() const; + void + set_livelock_accepting_state(bool is_livelock_accepting_state); + bool + is_initial_state() const; + void + set_initial_state(bool is_initial_state); + + private: + const state* tgba_state_; + const bdd tgba_condition_; + bool is_initial_state_; + bool is_accepting_state_; + bool is_livelock_accepting_state_; + transitions* transitions_; + + }; + + /// Successor iterators used by spot::ta_explicit. + class ta_explicit_succ_iterator : public ta_succ_iterator + { + public: + ta_explicit_succ_iterator(const state_ta_explicit* s); + + virtual void + first(); + virtual void + next(); + virtual bool + done() const; + + virtual state* + current_state() const; + virtual bdd + current_condition() const; + + + + private: + state_ta_explicit::transitions* transitions_; + state_ta_explicit::transitions::const_iterator i_; + }; + +} + +#endif // SPOT_TA_TAEXPLICIT_HH diff --git a/src/taalgos/Makefile.am b/src/taalgos/Makefile.am new file mode 100644 index 000000000..7340c8268 --- /dev/null +++ b/src/taalgos/Makefile.am @@ -0,0 +1,37 @@ +## Copyright (C) 2010 Laboratoire de Recherche et Développement +## de l'Epita (LRDE). +## +## This file is part of Spot, a model checking library.et Marie Curie. +## +## Spot is free software; you can redistribute it and/or modify it +## under the terms of the GNU General Public License as published by +## the Free Software Foundation; either version 2 of the License, or +## (at your option) any later version. +## +## Spot is distributed in the hope that it will be useful, but WITHOUT +## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +## License for more details. +## +## You should have received a copy of the GNU General Public License +## along with Spot; see the file COPYING. If not, write to the Free +## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +## 02111-1307, USA. + + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) +AM_CXXFLAGS = $(WARNING_CXXFLAGS) + +taalgosdir = $(pkgincludedir)/taalgos + +taalgos_HEADERS = \ + sba2ta.hh \ + dotty.hh \ + reachiter.hh + +noinst_LTLIBRARIES = libtaalgos.la +libtaalgos_la_SOURCES = \ + sba2ta.cc \ + dotty.cc \ + reachiter.cc + diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc new file mode 100644 index 000000000..14e95174d --- /dev/null +++ b/src/taalgos/dotty.cc @@ -0,0 +1,127 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "dotty.hh" +#include "tgba/bddprint.hh" +#include "reachiter.hh" +#include "misc/escape.hh" +#include "misc/bareword.hh" + +namespace spot +{ + namespace + { + class dotty_bfs : public ta_reachable_iterator_breadth_first + { + public: + dotty_bfs(std::ostream& os, const ta* a) : + ta_reachable_iterator_breadth_first(a), os_(os) + { + } + + void + start() + { + os_ << "digraph G {" << std::endl; + + int n = 0; + const ta::states_set_t* init_states_set = + t_automata_->get_initial_states_set(); + ta::states_set_t::const_iterator it; + + for (it = (init_states_set->begin()); it != init_states_set->end(); it++) + { + // cout << (*it).first << " => " << (*it).second << endl; + + bdd init_condition = t_automata_->get_state_condition(*it); + std::string label = bdd_format_formula(t_automata_->get_dict(), + init_condition); + ++n; + os_ << -n << " [label=\"\", style=invis, height=0]" << std::endl; + os_ << " " << -n << " -> " << n << " " << "[label=\"" + label + + "\"]" << std::endl; + + } + } + + void + end() + { + os_ << "}" << std::endl; + } + + void + process_state(const state* s, int n) + { + + std::string shape = "ellipse"; + std::string style = "solid"; + if (t_automata_->is_accepting_state(s)) + { + shape = "doublecircle"; + style = "bold"; + } + + if (t_automata_->is_livelock_accepting_state(s)) + { + shape = "octagon"; + style = "bold"; + } + if (t_automata_->is_livelock_accepting_state(s) + && t_automata_->is_accepting_state(s)) + { + shape = "doubleoctagon"; + style = "bold"; + } + + os_ << " " << n << " [label=" << quote_unless_bare_word( + t_automata_->format_state(s)) << "]" << "[shape=\"" + shape + "\"]" + << "[style=\"" + style + "\"]" << std::endl; + + } + + void + process_link(int in, int out, const tgba_succ_iterator* si) + { + + os_ << " " << in << " -> " << out << " [label=\""; + escape_str(os_, bdd_format_accset(t_automata_->get_dict(), + si->current_condition())) + + << "\"]" << std::endl; + + } + + private: + std::ostream& os_; + }; + + } + + std::ostream& + dotty_reachable(std::ostream& os, const ta* a) + { + dotty_bfs d(os, a); + d.run(); + return os; + } + +} diff --git a/src/taalgos/dotty.hh b/src/taalgos/dotty.hh new file mode 100644 index 000000000..edfbe313a --- /dev/null +++ b/src/taalgos/dotty.hh @@ -0,0 +1,35 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TAALGOS_DOTTY_HH +# define SPOT_TAALGOS_DOTTY_HH + +#include "ta/ta.hh" +#include + +namespace spot +{ + class ta; + + std::ostream& + dotty_reachable(std::ostream& os, const ta* a); +} + +#endif // SPOT_TAALGOS_DOTTY_HH diff --git a/src/taalgos/reachiter.cc b/src/taalgos/reachiter.cc new file mode 100644 index 000000000..88fb44b58 --- /dev/null +++ b/src/taalgos/reachiter.cc @@ -0,0 +1,176 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include +#include "reachiter.hh" + +#include +using namespace std; + +namespace spot +{ + // ta_reachable_iterator + ////////////////////////////////////////////////////////////////////// + + ta_reachable_iterator::ta_reachable_iterator(const ta* a) : + t_automata_(a) + { + } + ta_reachable_iterator::~ta_reachable_iterator() + { + seen_map::const_iterator s = seen.begin(); + while (s != seen.end()) + { + // Advance the iterator before deleting the "key" pointer. + const state* ptr = s->first; + ++s; + delete ptr; + } + } + + void + ta_reachable_iterator::run() + { + int n = 0; + start(); + const ta::states_set_t* init_states_set = + t_automata_->get_initial_states_set(); + ta::states_set_t::const_iterator it; + + for (it = init_states_set->begin(); it != init_states_set->end(); it++) + { + state* init_state = (*it)->clone(); + if (want_state(init_state)) + add_state(init_state); + seen[init_state] = ++n; + + } + + const state* t; + while ((t = next_state())) + { + assert(seen.find(t) != seen.end()); + int tn = seen[t]; + tgba_succ_iterator* si = t_automata_->succ_iter(t); + process_state(t, tn); + for (si->first(); !si->done(); si->next()) + { + const state* current = si->current_state()->clone(); + seen_map::const_iterator s = seen.find(current); + bool ws = want_state(current); + if (s == seen.end()) + { + seen[current] = ++n; + if (ws) + { + add_state(current); + process_link(tn, n, si); + } + } + else + { + if (ws) + process_link(tn, s->second, si); + delete current; + } + } + delete si; + } + end(); + } + + bool + ta_reachable_iterator::want_state(const state*) const + { + return true; + } + + void + ta_reachable_iterator::start() + { + } + + void + ta_reachable_iterator::end() + { + } + + void + ta_reachable_iterator::process_state(const state*, int) + { + } + + void + ta_reachable_iterator::process_link(int, int, const tgba_succ_iterator*) + { + } + + // ta_reachable_iterator_depth_first + ////////////////////////////////////////////////////////////////////// + + ta_reachable_iterator_depth_first::ta_reachable_iterator_depth_first( + const ta* a) : + ta_reachable_iterator(a) + { + } + + void + ta_reachable_iterator_depth_first::add_state(const state* s) + { + todo.push(s); + } + + const state* + ta_reachable_iterator_depth_first::next_state() + { + if (todo.empty()) + return 0; + const state* s = todo.top(); + todo.pop(); + return s; + } + + // ta_reachable_iterator_breadth_first + ////////////////////////////////////////////////////////////////////// + + ta_reachable_iterator_breadth_first::ta_reachable_iterator_breadth_first( + const ta* a) : + ta_reachable_iterator(a) + { + } + + void + ta_reachable_iterator_breadth_first::add_state(const state* s) + { + todo.push_back(s); + } + + const state* + ta_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/taalgos/reachiter.hh b/src/taalgos/reachiter.hh new file mode 100644 index 000000000..32c6702e8 --- /dev/null +++ b/src/taalgos/reachiter.hh @@ -0,0 +1,142 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TAALGOS_REACHITER_HH +# define SPOT_TAALGOS_REACHITER_HH + +#include "misc/hash.hh" +#include "ta/ta.hh" +#include +#include + +namespace spot +{ + /// \brief Iterate over all reachable states of a spot::ta. + /// \ingroup ta_generic + class ta_reachable_iterator + { + public: + ta_reachable_iterator(const ta* a); + virtual + ~ta_reachable_iterator(); + + /// \brief Iterate over all reachable states of a spot::ta. + /// + /// This is a template method that will call add_state(), next_state(), + /// start(), end(), process_state(), and process_link(), while it + /// iterates over states. + void + run(); + + /// \name Todo list management. + /// + /// spot::ta_reachable_iterator_depth_first and + /// spot::ta_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 next state to process. + virtual const state* + next_state() = 0; + /// \} + + /// Called by add_state or next_states implementations to filter + /// states. Default implementation always return true. + virtual bool + want_state(const state* s) const; + + /// Called by run() before starting its iteration. + virtual void + start(); + /// 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 A unique number assigned to \a s. + /// \param si The spot::ta_succ_iterator for \a s. + virtual void + process_state(const state* s, int n); + /// Called by run() to process a transition. + /// + /// \param in_s The source state + /// \param in The source state number. + /// \param out_s The destination state + /// \param out The destination state number. + /// \param si The spot::tgba_succ_iterator positionned on the current + /// transition. + /// + /// The in_s and out_s states are owned by the + /// spot::ta_reachable_iterator instance and destroyed when the + /// instance is destroyed. + virtual void + process_link(int in, int out, const tgba_succ_iterator* si); + + protected: + + const ta* t_automata_; ///< The spot::ta to explore. + + typedef Sgi::hash_map + seen_map; + seen_map seen; ///< States already seen. + }; + + /// \brief An implementation of spot::ta_reachable_iterator that browses + /// states depth first. + /// \ingroup ta_generic + class ta_reachable_iterator_depth_first : public ta_reachable_iterator + { + public: + ta_reachable_iterator_depth_first(const ta* 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::ta_reachable_iterator that browses + /// states breadth first. + /// \ingroup ta_generic + class ta_reachable_iterator_breadth_first : public ta_reachable_iterator + { + public: + ta_reachable_iterator_breadth_first(const ta* 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_TAALGOS_REACHITER_HH diff --git a/src/taalgos/sba2ta.cc b/src/taalgos/sba2ta.cc new file mode 100644 index 000000000..307a741c2 --- /dev/null +++ b/src/taalgos/sba2ta.cc @@ -0,0 +1,353 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "ltlast/atomic_prop.hh" +#include "ltlast/constant.hh" +#include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" +#include +#include "ltlvisit/tostring.hh" +#include +#include "tgba/bddprint.hh" +#include "tgbaalgos/gtec/nsheap.hh" +#include +#include "sba2ta.hh" + + +using namespace std; + +namespace spot +{ + + ta* + sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_) + { + + ta_explicit* ta = new spot::ta_explicit(tgba_); + + // build I set: + bdd init_condition; + bdd all_props = bddtrue; + ta::states_set_t todo; + + while ((init_condition = bdd_satoneset(all_props, atomic_propositions_set_, + bddtrue)) != bddfalse) + { + all_props -= init_condition; + state_ta_explicit* init_state = new state_ta_explicit((tgba_->get_init_state()), + init_condition, true); + ta->add_initial_state(init_state); + todo.insert(init_state); + } + + while (!todo.empty()) + { + ta::states_set_t::iterator todo_it = todo.begin(); + state_ta_explicit* source = dynamic_cast (*todo_it); + todo.erase(todo_it); + + tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter( + source->get_tgba_state()); + for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next()) + { + const state* tgba_state = tgba_succ_it->current_state(); + bdd tgba_condition = tgba_succ_it->current_condition(); + bdd satone_tgba_condition; + while ((satone_tgba_condition = bdd_satoneset(tgba_condition, + atomic_propositions_set_, bddtrue)) != bddfalse) + { + + tgba_condition -= satone_tgba_condition; + state_ta_explicit* new_dest = new state_ta_explicit(tgba_state->clone(), + satone_tgba_condition, false, tgba_->state_is_accepting( + tgba_state)); + + state_ta_explicit* dest = ta->add_state(new_dest); + + if (dest != new_dest) + { + // the state dest already exists in the testing automata + delete new_dest->get_tgba_state(); + delete new_dest; + } + else + { + todo.insert(dest); + } + + ta->create_transition(source, bdd_setxor( + source->get_tgba_condition(), dest->get_tgba_condition()), + dest); + + } + delete tgba_state; + } + delete tgba_succ_it; + + } + + compute_livelock_acceptance_states(ta); + + ta->delete_stuttering_transitions(); + + return ta; + + } + + namespace + { + typedef std::pair pair_state_iter; + } + + void + compute_livelock_acceptance_states(ta_explicit* testing_automata) + { + // We use five main data in this algorithm: + // * sscc: a stack of strongly stuttering-connected components (SSCC) + sscc_stack sscc; + + // * h: a hash of all visited nodes, with their order, + // (it is called "Hash" in Couvreur's paper) + numbered_state_heap* h = + numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states. + + // * num: the number of visited nodes. Used to set the order of each + // visited node, + int num = 0; + + // * todo: the depth-first search stack. This holds pairs of the + // form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator + // over the successors of STATE. In our use, ITERATOR should + // always be freed when TODO is popped, but STATE should not because + // it is also used as a key in H. + std::stack todo; + + // * init: the set of the depth-first search initial states + ta::states_set_t init_set; + + ta::states_set_t::const_iterator it; + for (it = (testing_automata->get_initial_states_set())->begin(); it != (testing_automata->get_initial_states_set())->end(); it++) + { + state* init_state = (*it); + init_set.insert(init_state); + + } + + while (!init_set.empty()) + { + // Setup depth-first search from an initial state. + { + ta::states_set_t::iterator init_set_it = init_set.begin(); + state_ta_explicit* init = dynamic_cast (*init_set_it); + init_set.erase(init_set_it); + state_ta_explicit* init_clone = init->clone(); + numbered_state_heap::state_index_p h_init = h->find(init_clone); + + if (h_init.first) + continue; + + h->insert(init_clone, ++num); + sscc.push(num); + sscc.top().is_accepting = testing_automata->is_accepting_state(init); + sscc.top().is_initial = testing_automata->is_initial_state(init); + tgba_succ_iterator* iter = testing_automata->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); + + } + + while (!todo.empty()) + { + + // We are looking at the next successor in SUCC. + tgba_succ_iterator* succ = todo.top().second; + + state* curr = todo.top().first; + + // If there is no more successor, backtrack. + if (succ->done()) + { + // We have explored all successors of state CURR. + + // Backtrack TODO. + todo.pop(); + + // fill rem with any component removed, + numbered_state_heap::state_index_p spi = h->index(curr->clone()); + assert(spi.first); + + sscc.rem().push_front(curr); + + // When backtracking the root of an SSCC, we must also + // remove that SSCC from the ROOT stacks. We must + // discard from H all reachable states from this SSCC. + assert(!sscc.empty()); + if (sscc.top().index == *spi.second) + { + // removing states + std::list::iterator i; + bool is_livelock_accepting_sscc = (sscc.top().is_accepting + && (sscc.rem().size() > 1)); + for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) + { + numbered_state_heap::state_index_p spi = h->index((*i)->clone()); + assert(spi.first->compare(*i)==0); + assert(*spi.second != -1); + *spi.second = -1; + if (is_livelock_accepting_sscc) + {//if it is an accepting sscc + //add the state to G (=the livelock-accepting states set) + + state_ta_explicit * livelock_accepting_state = + dynamic_cast (*i); + + livelock_accepting_state->set_livelock_accepting_state( + true); + + } + + if (sscc.top().is_initial) + {//if it is an initial sscc + //add the state to I (=the initial states set) + + state_ta_explicit * initial_state = + dynamic_cast (*i); + + testing_automata->add_initial_state(initial_state); + } + } + + is_livelock_accepting_sscc = testing_automata->is_livelock_accepting_state( + *sscc.rem().begin()); + sscc.pop(); + if (is_livelock_accepting_sscc && !sscc.empty()) + { + sscc.top().is_accepting = true; + + state_ta_explicit * livelock_accepting_state = + dynamic_cast (todo.top().first); + livelock_accepting_state->set_livelock_accepting_state( + true); + + } + if (sscc.top().is_initial && !sscc.empty()) + sscc.top().is_initial = true; + } + + delete succ; + // Do not delete CURR: it is a key in H. + continue; + } + + // Fetch the values destination state we are interested in... + state* dest = succ->current_state(); + + // ... and point the iterator to the next successor, for + // the next iteration. + succ->next(); + // We do not need SUCC from now on. + + + // Are we going to a new state through a stuttering transition? + bool is_stuttering_transition = testing_automata->get_state_condition(curr) + == testing_automata->get_state_condition(dest); + state* dest_clone = dest->clone(); + numbered_state_heap::state_index_p spi = h->find(dest_clone); + + // Is this a new state? + if (!spi.first) + { + if (!is_stuttering_transition) + { + init_set.insert(dest); + delete dest_clone; + continue; + } + + // Number it, stack it, and register its successors + // for later processing. + h->insert(dest_clone, ++num); + sscc.push(num); + sscc.top().is_accepting = testing_automata->is_accepting_state(dest); + sscc.top().is_initial = testing_automata->is_initial_state(dest); + tgba_succ_iterator* iter = testing_automata->succ_iter(dest); + iter->first(); + todo.push(pair_state_iter(dest, iter)); + continue; + } + + // If we have reached a dead component, ignore it. + if (*spi.second == -1) + continue; + + if (!curr->compare(dest)) + { + state_ta_explicit * self_loop_state = dynamic_cast (curr); + + if (testing_automata->is_accepting_state(self_loop_state)) + self_loop_state->set_livelock_accepting_state(true); + + } + + // Now this is the most interesting case. We have reached a + // state S1 which is already part of a non-dead SSCC. Any such + // non-dead SSCC has necessarily been crossed by our path to + // this state: there is a state S2 in our path which belongs + // to this SSCC too. We are going to merge all states between + // this S1 and S2 into this SSCC. + // + // This merge is easy to do because the order of the SSCC in + // ROOT is ascending: we just have to merge all SSCCs from the + // top of ROOT that have an index greater to the one of + // the SSCC of S2 (called the "threshold"). + int threshold = *spi.second; + std::list rem; + bool acc = false; + bool init = false; + while (threshold < sscc.top().index) + { + assert(!sscc.empty()); + + acc |= sscc.top().is_accepting; + init |= sscc.top().is_initial; + + rem.splice(rem.end(), sscc.rem()); + sscc.pop(); + + } + // Note that we do not always have + // threshold == sscc.top().index + // after this loop, the SSCC whose index is threshold might have + // been merged with a lower SSCC. + + // Accumulate all acceptance conditions into the merged SSCC. + sscc.top().is_accepting |= acc; + sscc.top().is_initial |= init; + + sscc.rem().splice(sscc.rem().end(), rem); + + } + + } + delete h; + + } + +} diff --git a/src/taalgos/sba2ta.hh b/src/taalgos/sba2ta.hh new file mode 100644 index 000000000..b6d97855f --- /dev/null +++ b/src/taalgos/sba2ta.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// de l Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_TGBAALGOS_SBA2TA_HH +# define SPOT_TGBAALGOS_SBA2TA_HH + +#include "misc/hash.hh" +#include +#include +#include +#include "tgba/tgbatba.hh" +#include "ltlast/formula.hh" +#include +#include "misc/bddlt.hh" +#include "ta/taexplicit.hh" + + +namespace spot +{ + ta* sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set); + + + void compute_livelock_acceptance_states(ta_explicit* testing_automata); + +} + +#endif // SPOT_TGBAALGOS_SBA2TA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 5ee00f7c1..7c6b5fe5d 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -65,6 +65,9 @@ #include "kripkeparse/public.hh" #include "tgbaalgos/simulation.hh" +#include "taalgos/sba2ta.hh" +#include "taalgos/dotty.hh" + std::string ltl_defs() { @@ -273,7 +276,13 @@ syntax(char* prog) << " -T time the different phases of the translation" << std::endl << " -v display the BDD variables used by the automaton" - << std::endl; + << std::endl + + << "Options for Testing Automata:" + << std::endl + << " -TA Translate an LTL formula into a Testing automata" + << std::endl; + exit(2); } @@ -332,7 +341,7 @@ main(int argc, char** argv) bool assume_sba = false; bool reduction_dir_sim = false; spot::tgba* temp_dir_sim = 0; - + bool ta_opt = false; for (;;) { @@ -660,6 +669,10 @@ main(int argc, char** argv) { use_timer = true; } + else if (!strcmp(argv[formula_index], "-TA")) + { + ta_opt = true; + } else if (!strcmp(argv[formula_index], "-taa")) { translation = TransTAA; @@ -1047,8 +1060,39 @@ main(int argc, char** argv) break; } + const spot::tgba* product_degeneralized = 0; + if (ta_opt) + { + spot::tgba_sba_proxy* degeneralized_new = 0; + spot::tgba_sba_proxy* degeneralized = + dynamic_cast (a); + if (degeneralized == 0) + degeneralized_new = degeneralized = new spot::tgba_sba_proxy(a); + + spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0); + + bdd atomic_props_set_bdd = bdd_true(); + for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i + != aps->end(); ++i) + { + bdd atomic_prop = bdd_ithvar( + (degeneralized->get_dict())->var_map[*i]); + + atomic_props_set_bdd &= atomic_prop; + + } + delete aps; + + spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd); + spot::dotty_reachable(std::cout, testing_automata); + delete testing_automata; + delete degeneralized_new; + output = -1; + } + + if (system) { product = product_to_free = a = new spot::tgba_product(system, a);