From c882eadda6de479b8bcc52eaa00b159471e3cd40 Mon Sep 17 00:00:00 2001 From: Ala-Eddine Ben-Salem Date: Wed, 23 Nov 2011 12:24:25 +0100 Subject: [PATCH] New Automata: TGTA (Transition-based Generalized TA) * src/ta/Makefile.am, src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/tgbta.cc, src/ta/tgbta.hh, src/ta/tgbtaexplicit.cc, src/ta/tgbtaexplicit.hh, src/ta/tgbtaproduct.cc, src/ta/tgbtaproduct.hh, src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh, src/taalgos/sba2ta.cc, src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh, src/tgbatest/ltl2tgba.cc: Implementation of TGTA, a new kind of automata combining ideas from TGBA and TA. --- src/ta/Makefile.am | 11 +- src/ta/taexplicit.cc | 47 ++++--- src/ta/taexplicit.hh | 16 +-- src/ta/taproduct.cc | 2 +- src/ta/tgbta.cc | 35 +++++ src/ta/tgbta.hh | 44 +++++++ src/ta/tgbtaexplicit.cc | 98 ++++++++++++++ src/ta/tgbtaexplicit.hh | 66 ++++++++++ src/ta/tgbtaproduct.cc | 258 +++++++++++++++++++++++++++++++++++++ src/ta/tgbtaproduct.hh | 110 ++++++++++++++++ src/taalgos/emptinessta.cc | 143 +++++++++++--------- src/taalgos/emptinessta.hh | 8 +- src/taalgos/sba2ta.cc | 13 +- src/taalgos/tgba2ta.cc | 168 ++++++++++++++++++------ src/taalgos/tgba2ta.hh | 6 +- src/tgbatest/ltl2tgba.cc | 48 +++++-- 16 files changed, 921 insertions(+), 152 deletions(-) create mode 100644 src/ta/tgbta.cc create mode 100644 src/ta/tgbta.hh create mode 100644 src/ta/tgbtaexplicit.cc create mode 100644 src/ta/tgbtaexplicit.hh create mode 100644 src/ta/tgbtaproduct.cc create mode 100644 src/ta/tgbtaproduct.hh diff --git a/src/ta/Makefile.am b/src/ta/Makefile.am index 11de1047b..75b4df8bd 100644 --- a/src/ta/Makefile.am +++ b/src/ta/Makefile.am @@ -25,11 +25,18 @@ tadir = $(pkgincludedir)/ta ta_HEADERS = \ ta.hh \ + taexplicit.hh \ taproduct.hh \ - taexplicit.hh + tgbta.hh \ + tgbtaexplicit.hh \ + tgbtaproduct.hh + noinst_LTLIBRARIES = libta.la libta_la_SOURCES = \ ta.cc \ taproduct.cc \ - taexplicit.cc + tgbta.cc \ + tgbtaexplicit.cc \ + taexplicit.cc \ + tgbtaproduct.cc diff --git a/src/ta/taexplicit.cc b/src/ta/taexplicit.cc index 138cc3ae0..18a5e77f5 100644 --- a/src/ta/taexplicit.cc +++ b/src/ta/taexplicit.cc @@ -18,6 +18,15 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +//#define TRACE + +#include +#ifdef TRACE +#define trace std::clog +#else +#define trace while (0) std::clog +#endif + #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "taexplicit.hh" @@ -71,7 +80,9 @@ namespace spot state* ta_explicit_succ_iterator::current_state() const { + trace << "***ta_explicit_succ_iterator::current_state() if(done()) =***" << done() << std::endl; assert(!done()); + trace << "***ta_explicit_succ_iterator::current_state() (*i_)->condition =***" << (*i_)->condition << std::endl; state_ta_explicit* s = (*i_)->dest; return s; } @@ -125,7 +136,8 @@ namespace spot } void - state_ta_explicit::add_transition(state_ta_explicit::transition* t) + state_ta_explicit::add_transition(state_ta_explicit::transition* t, + bool add_at_beginning) { if (transitions_ == 0) transitions_ = new transitions; @@ -153,8 +165,17 @@ namespace spot if (!transition_found) { - transitions_condition->push_back(t); - transitions_->push_back(t); + if (add_at_beginning) + { + transitions_condition->push_front(t); + transitions_->push_front(t); + } + else + { + transitions_condition->push_back(t); + transitions_->push_back(t); + } + } else { @@ -245,7 +266,7 @@ namespace spot size_t state_ta_explicit::hash() const { - return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id()); + return wang32_hash(tgba_state_->hash()); } state_ta_explicit* @@ -353,7 +374,6 @@ namespace spot delete tgba_; } - state_ta_explicit* ta_explicit::add_state(state_ta_explicit* s) { @@ -377,7 +397,7 @@ namespace spot if (get_artificial_initial_state() != 0) if (add_state.second) create_transition((state_ta_explicit*) get_artificial_initial_state(), - condition, s); + condition, bddfalse, s); } @@ -392,27 +412,16 @@ namespace spot } - 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; - t->acceptance_conditions = bddfalse; - source->add_transition(t); - - } void ta_explicit::create_transition(state_ta_explicit* source, bdd condition, - bdd acceptance_conditions, state_ta_explicit* dest) + bdd acceptance_conditions, state_ta_explicit* dest, bool add_at_beginning) { state_ta_explicit::transition* t = new state_ta_explicit::transition; t->dest = dest; t->condition = condition; t->acceptance_conditions = acceptance_conditions; - source->add_transition(t); + source->add_transition(t, add_at_beginning); } diff --git a/src/ta/taexplicit.hh b/src/ta/taexplicit.hh index ded8ffe91..bde2b3f68 100644 --- a/src/ta/taexplicit.hh +++ b/src/ta/taexplicit.hh @@ -53,13 +53,11 @@ namespace spot void add_to_initial_states_set(state* s, bdd condition = bddfalse); - void - create_transition(state_ta_explicit* source, bdd condition, - state_ta_explicit* dest); void create_transition(state_ta_explicit* source, bdd condition, - bdd acceptance_conditions, state_ta_explicit* dest); + bdd acceptance_conditions, state_ta_explicit* dest, + bool add_at_beginning = false); void delete_stuttering_transitions(); @@ -132,7 +130,6 @@ namespace spot return all_acceptance_conditions_;; } - private: // Disallow copy. ta_explicit(const ta_explicit& other); @@ -179,6 +176,11 @@ namespace spot virtual state_ta_explicit* clone() const; + virtual + void destroy() const + { + } + virtual ~state_ta_explicit() { @@ -192,7 +194,7 @@ namespace spot get_transitions(bdd condition) const; void - add_transition(transition* t); + add_transition(transition* t, bool add_at_beginning = false); const state* get_tgba_state() const; @@ -221,8 +223,6 @@ namespace spot void free_transitions(); - - private: const state* tgba_state_; const bdd tgba_condition_; diff --git a/src/ta/taproduct.cc b/src/ta/taproduct.cc index 1f16d2bfd..6092eb548 100644 --- a/src/ta/taproduct.cc +++ b/src/ta/taproduct.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2010 Laboratoire de Recherche et Developpement +// Copyright (C) 2011 Laboratoire de Recherche et Developpement // de l Epita (LRDE). // // diff --git a/src/ta/tgbta.cc b/src/ta/tgbta.cc new file mode 100644 index 000000000..14734d800 --- /dev/null +++ b/src/ta/tgbta.cc @@ -0,0 +1,35 @@ +// Copyright (C) 2012 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. + +#include "tgbta.hh" + + +namespace spot +{ + + tgbta::tgbta() + {}; + tgbta::~tgbta() + {}; + + +} + + diff --git a/src/ta/tgbta.hh b/src/ta/tgbta.hh new file mode 100644 index 000000000..e6a915405 --- /dev/null +++ b/src/ta/tgbta.hh @@ -0,0 +1,44 @@ +// Copyright (C) 2010, 2011 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_TGBTA_HH +# define SPOT_TA_TGBTA_HH + +#include "tgba/tgba.hh" + +namespace spot +{ + class tgbta : public tgba + { + + protected: + tgbta(); + public: + + virtual + ~tgbta(); + virtual tgba_succ_iterator* + succ_iter_by_changeset(const spot::state* s, bdd change_set) const =0; + + }; + +} + +#endif // SPOT_TA_TGBTA_HH diff --git a/src/ta/tgbtaexplicit.cc b/src/ta/tgbtaexplicit.cc new file mode 100644 index 000000000..9f55c35a4 --- /dev/null +++ b/src/ta/tgbtaexplicit.cc @@ -0,0 +1,98 @@ +// Copyright (C) 2010, 2011 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 "tgbtaexplicit.hh" +#include "tgba/formula2bdd.hh" +#include "misc/bddop.hh" +#include "ltlvisit/tostring.hh" + +#include "tgba/bddprint.hh" + +namespace spot +{ + + + tgbta_explicit::tgbta_explicit(const tgba* tgba, bdd all_acceptance_conditions, + state_ta_explicit* artificial_initial_state) : + ta_explicit(tgba, all_acceptance_conditions, artificial_initial_state) + { + } + + + state* + tgbta_explicit::get_init_state() const + { + return ta_explicit::get_artificial_initial_state(); + } + + tgba_succ_iterator* + tgbta_explicit::succ_iter(const spot::state* state, + const spot::state* global_state, + const tgba* global_automaton) const + { + return ta_explicit::succ_iter(state); + } + + bdd + tgbta_explicit::compute_support_conditions(const spot::state* in) const + { + return get_tgba()->support_conditions(((state_ta_explicit*) in)->get_tgba_state()); + } + + bdd + tgbta_explicit::compute_support_variables(const spot::state* in) const + { + return get_tgba()->support_variables(((state_ta_explicit*) in)->get_tgba_state()); + } + + bdd_dict* + tgbta_explicit::get_dict() const + { + return ta_explicit::get_dict(); + } + + bdd + tgbta_explicit::all_acceptance_conditions() const + { + + return ta_explicit::all_acceptance_conditions(); + } + + bdd + tgbta_explicit::neg_acceptance_conditions() const + { + return get_tgba()->neg_acceptance_conditions(); + } + + std::string + tgbta_explicit::format_state(const spot::state* s) const + { + return ta_explicit::format_state(s); + } + + + spot::tgba_succ_iterator* tgbta_explicit::succ_iter_by_changeset(const spot::state* s, bdd change_set) const + { + return ta_explicit::succ_iter(s,change_set); + } + +} diff --git a/src/ta/tgbtaexplicit.hh b/src/ta/tgbtaexplicit.hh new file mode 100644 index 000000000..68f659704 --- /dev/null +++ b/src/ta/tgbtaexplicit.hh @@ -0,0 +1,66 @@ +// Copyright (C) 2010, 2011 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_TGBTAEXPLICIT_HH +# define SPOT_TA_TGBTAEXPLICIT_HH + +#include "misc/hash.hh" +#include +#include "tgba/tgba.hh" +#include +#include "ltlast/formula.hh" +#include +#include "misc/bddlt.hh" +#include "taexplicit.hh" +#include "tgbta.hh" + +namespace spot +{ + class tgbta_explicit : public tgbta, public ta_explicit + { + public: + tgbta_explicit(const tgba* tgba, bdd all_acceptance_conditions, + state_ta_explicit* artificial_initial_state) ; + + // tgba interface + virtual spot::state* get_init_state() const; + virtual tgba_succ_iterator* + succ_iter(const spot::state* local_state, + const spot::state* global_state = 0, + const tgba* global_automaton = 0) const; + virtual bdd_dict* get_dict() const; + + virtual bdd all_acceptance_conditions() const; + virtual bdd neg_acceptance_conditions() const; + + virtual std::string format_state(const spot::state* s) const; + + virtual tgba_succ_iterator* succ_iter_by_changeset(const spot::state* s, bdd change_set) const; + protected: + virtual bdd compute_support_conditions(const spot::state* state) const; + virtual bdd compute_support_variables(const spot::state* state) const; + + }; + + + +} + +#endif // SPOT_TA_TGBTAEXPLICIT_HH diff --git a/src/ta/tgbtaproduct.cc b/src/ta/tgbtaproduct.cc new file mode 100644 index 000000000..1ea7c3174 --- /dev/null +++ b/src/ta/tgbtaproduct.cc @@ -0,0 +1,258 @@ +// Copyright (C) 2012 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. + + +//#define TRACE + +#include +#ifdef TRACE +#define trace std::clog +#else +#define trace while (0) std::clog +#endif + +#include "tgbtaproduct.hh" +#include +#include +#include "misc/hashfunc.hh" +#include "kripke/kripke.hh" + +namespace spot +{ + + //////////////////////////////////////////////////////////// + // tgbta_succ_iterator_product + + + //////////////////////////////////////////////////////////// + // tgbta_product + + tgbta_product::tgbta_product(const kripke* left, const tgbta* right) : + tgba_product(left, right) + { + } + + state* + tgbta_product::get_init_state() const + { + fixed_size_pool* p = const_cast (&pool_); + return new (p->allocate()) state_product(left_->get_init_state(), + right_->get_init_state(), p); + } + + tgba_succ_iterator* + tgbta_product::succ_iter(const state* local_state, const state* global_state, + const tgba* global_automaton) const + { + const state_product* s = down_cast (local_state); + assert(s); + + fixed_size_pool* p = const_cast (&pool_); + + return new tgbta_succ_iterator_product(s, (kripke*) left_, + (tgbta *) right_, p); + } + + //////////////////////////////////////////////////////////// + // tgbtgbta_succ_iterator_product + tgbta_succ_iterator_product::tgbta_succ_iterator_product( + const state_product* s, const kripke* k, const tgbta* t, + fixed_size_pool* pool) : + source_(s), tgbta_(t), kripke_(k), pool_(pool) + { + + state * tgbta_init_state = tgbta_->get_init_state(); + if ((s->right())->compare(tgbta_init_state) == 0) + source_ = 0; + + if (source_ == 0) + { + kripke_succ_it_ = 0; + kripke_current_dest_state = kripke_->get_init_state(); + current_condition_ + = kripke_->state_condition(kripke_current_dest_state); + tgbta_succ_it_ = tgbta_->succ_iter_by_changeset( + tgbta_init_state, current_condition_); + tgbta_succ_it_->first(); + trace + << "*** tgbta_succ_it_->done() = ***" << tgbta_succ_it_->done() + << std::endl; + + } + else + { + kripke_source_condition = kripke_->state_condition(s->left()); + kripke_succ_it_ = kripke_->succ_iter(s->left()); + kripke_current_dest_state = 0; + tgbta_succ_it_ = 0; + } + + tgbta_init_state->destroy(); + current_state_ = 0; + } + + tgbta_succ_iterator_product::~tgbta_succ_iterator_product() + { + // ta_->free_state(current_state_); + if (current_state_ != 0) + current_state_->destroy(); + current_state_ = 0; + delete tgbta_succ_it_; + delete kripke_succ_it_; + if (kripke_current_dest_state != 0) + kripke_current_dest_state->destroy(); + } + + void + tgbta_succ_iterator_product::step_() + { + if (!tgbta_succ_it_->done()) + tgbta_succ_it_->next(); + if (tgbta_succ_it_->done()) + { + delete tgbta_succ_it_; + tgbta_succ_it_ = 0; + next_kripke_dest(); + } + } + + void + tgbta_succ_iterator_product::next_kripke_dest() + { + if (!kripke_succ_it_) + return; + + if (kripke_current_dest_state == 0) + { + kripke_succ_it_->first(); + } + else + { + kripke_current_dest_state->destroy(); + kripke_current_dest_state = 0; + kripke_succ_it_->next(); + } + + // If one of the two successor sets is empty initially, we reset + // kripke_succ_it_, so that done() can detect this situation easily. (We + // choose to reset kripke_succ_it_ because this variable is already used by + // done().) + if (kripke_succ_it_->done()) + { + delete kripke_succ_it_; + kripke_succ_it_ = 0; + return; + } + + kripke_current_dest_state = kripke_succ_it_->current_state(); + bdd kripke_current_dest_condition = kripke_->state_condition( + kripke_current_dest_state); + + current_condition_ = bdd_setxor(kripke_source_condition, + kripke_current_dest_condition); + tgbta_succ_it_ = tgbta_->succ_iter_by_changeset(source_->right(), + current_condition_); + tgbta_succ_it_->first(); + + } + + void + tgbta_succ_iterator_product::first() + { + + next_kripke_dest(); + trace + << "*** first() .... if(done()) = ***" << done() << std::endl; + if (!done()) + find_next_succ_(); + + } + + void + tgbta_succ_iterator_product::next() + { + current_state_->destroy(); + current_state_ = 0; + + step_(); + + trace + << "*** next() .... if(done()) = ***" << done() << std::endl; + + if (!done()) + find_next_succ_(); + + } + + void + tgbta_succ_iterator_product::find_next_succ_() + { + + while (!done()) + { + if (!tgbta_succ_it_->done()) + { + current_state_ = new (pool_->allocate()) state_product( + kripke_current_dest_state->clone(), + tgbta_succ_it_->current_state(), pool_); + current_acceptance_conditions_ + = tgbta_succ_it_->current_acceptance_conditions(); + return; + } + + step_(); + } + } + + bool + tgbta_succ_iterator_product::done() const + { + if (source_ == 0) + { + return !tgbta_succ_it_ || tgbta_succ_it_->done(); + } + else + { + return !kripke_succ_it_ || kripke_succ_it_->done(); + } + + } + + state_product* + tgbta_succ_iterator_product::current_state() const + { + trace + << "*** current_state() .... if(done()) = ***" << done() << std::endl; + return current_state_->clone(); + } + + bdd + tgbta_succ_iterator_product::current_condition() const + { + return current_condition_; + } + + bdd + tgbta_succ_iterator_product::current_acceptance_conditions() const + { + return current_acceptance_conditions_; + } + +} diff --git a/src/ta/tgbtaproduct.hh b/src/ta/tgbtaproduct.hh new file mode 100644 index 000000000..4ee82632c --- /dev/null +++ b/src/ta/tgbtaproduct.hh @@ -0,0 +1,110 @@ +// Copyright (C) 2011 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 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_TGBTA_TGBAPRODUCT_HH +# define SPOT_TGBTA_TGBAPRODUCT_HH + +#include "tgba/tgba.hh" +#include "tgba/tgbaproduct.hh" +#include "misc/fixpool.hh" +#include "kripke/kripke.hh" +#include "tgbta.hh" + +namespace spot +{ + + /// \brief A lazy product. (States are computed on the fly.) + class tgbta_product : public tgba_product + { + public: + + tgbta_product(const kripke* left, const tgbta* right); + + virtual state* + get_init_state() const; + + virtual tgba_succ_iterator* + succ_iter(const state* local_state, const state* global_state = 0, + const tgba* global_automaton = 0) const; + + + }; + + /// \brief Iterate over the successors of a product computed on the fly. + class tgbta_succ_iterator_product : public tgba_succ_iterator + { + public: + tgbta_succ_iterator_product(const state_product* s, const kripke* k, const tgbta* tgbta, fixed_size_pool* pool); + + virtual + ~tgbta_succ_iterator_product(); + + // iteration + void + first(); + void + next(); + bool + done() const; + + // inspection + state_product* + current_state() const; + bdd + current_condition() const; + + bdd + current_acceptance_conditions() const; + + private: + //@{ + /// Internal routines to advance to the next successor. + void + step_(); + void + find_next_succ_(); + + void + next_kripke_dest(); + + //@} + + protected: + const state_product* source_; + const tgbta* tgbta_; + const kripke* kripke_; + fixed_size_pool* pool_; + tgba_succ_iterator* tgbta_succ_it_; + tgba_succ_iterator* kripke_succ_it_; + state_product* current_state_; + bdd current_condition_; + bdd current_acceptance_conditions_; + bdd kripke_source_condition; + state * kripke_current_dest_state; + + + }; + +} + +#endif // SPOT_TGBTA_TGBAPRODUCT_HH diff --git a/src/taalgos/emptinessta.cc b/src/taalgos/emptinessta.cc index f187e98d3..98a372684 100644 --- a/src/taalgos/emptinessta.cc +++ b/src/taalgos/emptinessta.cc @@ -73,8 +73,7 @@ namespace spot // it is also used as a key in H. std::stack todo; - // * init: the set of the depth-first search initial states - std::stack init_set; + Sgi::hash_map colour; @@ -89,44 +88,44 @@ namespace spot bool livelock_acceptance_states_not_found = true; - const ta::states_set_t init_states_set = a_->get_initial_states_set(); + bool activate_heuristic = (is_full_2_pass_ == disable_second_pass); - ta::states_set_t::const_iterator it; - for (it = init_states_set.begin(); it != init_states_set.end(); it++) + // Setup depth-first search from initial states. + const ta* ta_ = a_->get_ta(); + const kripke* kripke_ = a_->get_kripke(); + state* kripke_init_state = kripke_->get_init_state(); + bdd kripke_init_state_condition = kripke_->state_condition( + kripke_init_state); + + spot::state* artificial_initial_state = ta_->get_artificial_initial_state(); + + ta_succ_iterator* ta_init_it_ = ta_->succ_iter(artificial_initial_state, + kripke_init_state_condition); + kripke_init_state->destroy(); + for (ta_init_it_->first(); !ta_init_it_->done(); ta_init_it_->next()) { - state* init_state = (*it); - init_set.push(init_state); - } + state_ta_product* init = new state_ta_product( + (ta_init_it_->current_state()), kripke_init_state->clone()); - while (!init_set.empty()) - { - // Setup depth-first search from initial states. + numbered_state_heap::state_index_p h_init = h->find(init); - { - state* init = init_set.top(); - init_set.pop(); + if (h_init.first) + continue; - numbered_state_heap::state_index_p h_init = h->find(init); + h->insert(init, ++num); + scc.push(num); + arc.push(bddfalse); - if (h_init.first) - continue; + ta_succ_iterator* iter = a_->succ_iter(init); + iter->first(); + todo.push(pair_state_iter(init, iter)); - h->insert(init, ++num); - scc.push(num); - arc.push(bddfalse); + inc_depth(); - ta_succ_iterator* iter = a_->succ_iter(init); - iter->first(); - todo.push(pair_state_iter(init, iter)); - - inc_depth(); - - //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(init)) - livelock_roots.push(init); - - } + //push potential root of live-lock accepting cycle + if (activate_heuristic && a_->is_livelock_accepting_state(init)) + livelock_roots.push(init); while (!todo.empty()) { @@ -169,8 +168,8 @@ namespace spot *spi.second = -std::abs(*spi.second); // Backtrack livelock_roots. - if (!livelock_roots.empty() && !livelock_roots.top()->compare( - curr)) + if (activate_heuristic && !livelock_roots.empty() + && !livelock_roots.top()->compare(curr)) livelock_roots.pop(); // When backtracking the root of an SSCC, we must also @@ -249,7 +248,7 @@ namespace spot inc_depth(); //push potential root of live-lock accepting cycle - if (a_->is_livelock_accepting_state(dest) + if (activate_heuristic && a_->is_livelock_accepting_state(dest) && !is_stuttering_transition) livelock_roots.push(dest); @@ -276,7 +275,7 @@ namespace spot bool acc = false; trace - << "***PASS 1: CYCLE***" << std::endl; + << "***PASS 1: CYCLE***" << std::endl; while (threshold < scc.top().index) { @@ -309,27 +308,32 @@ namespace spot if (is_accepting_sscc) { trace - << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " << a_->is_livelock_accepting_state(curr) << std::endl; + << "PASS 1: SUCCESS : a_->is_livelock_accepting_state(curr): " + << a_->is_livelock_accepting_state(curr) << std::endl; trace - << "PASS 1: scc.top().condition : " << bdd_format_accset(a_->get_dict(), - scc.top().condition) << std::endl; + << "PASS 1: scc.top().condition : " << bdd_format_accset( + a_->get_dict(), scc.top().condition) << std::endl; trace - << "PASS 1: a_->all_acceptance_conditions() : " << (scc.top().condition == a_->all_acceptance_conditions()) << std::endl; + << "PASS 1: a_->all_acceptance_conditions() : " + << ( a_->all_acceptance_conditions()) << std::endl; + trace + << "PASS 1 CYCLE and (scc.top().condition == a_->all_acceptance_conditions()) : " + << (scc.top().condition == a_->all_acceptance_conditions()) << std::endl; trace - << "PASS 1: bddtrue : " << (a_->all_acceptance_conditions()== - bddtrue) << std::endl; + << "PASS 1: bddtrue : " << (a_->all_acceptance_conditions() + == bddtrue) << std::endl; trace - << "PASS 1: bddfalse : " << (a_->all_acceptance_conditions()== - bddfalse) << std::endl; + << "PASS 1: bddfalse : " << (a_->all_acceptance_conditions() + == bddfalse) << std::endl; - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); return true; } //ADDLINKS - if (!is_full_2_pass_ && a_->is_livelock_accepting_state(curr) + if (activate_heuristic && a_->is_livelock_accepting_state(curr) && is_stuttering_transition) { trace @@ -348,7 +352,7 @@ namespace spot if (heuristic_livelock_detection(dest, h, h_livelock_root, liveset_curr)) { - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); return true; } @@ -359,7 +363,7 @@ namespace spot if (heuristic_livelock_detection(succ, h, h_livelock_root, liveset_curr)) { - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); return true; } @@ -370,7 +374,7 @@ namespace spot } - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); if (disable_second_pass || livelock_acceptance_states_not_found) return false; @@ -431,23 +435,23 @@ namespace spot std::stack todo; // * init: the set of the depth-first search initial states - std::stack init_set; + std::queue ta_init_it_; const ta::states_set_t init_states_set = a_->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); - init_set.push(init_state); + ta_init_it_.push(init_state); } - while (!init_set.empty()) + while (!ta_init_it_.empty()) { // Setup depth-first search from initial states. { - state* init = init_set.top(); - init_set.pop(); + state* init = ta_init_it_.front(); + ta_init_it_.pop(); numbered_state_heap::state_index_p h_init = h->find(init); if (h_init.first) @@ -540,7 +544,7 @@ namespace spot if (!is_stuttering_transition) { - init_set.push(dest); + ta_init_it_.push(dest); continue; } @@ -568,7 +572,7 @@ namespace spot if (t->is_livelock_accepting_state(self_loop_state)) { - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); trace << "PASS 2: SUCCESS" << std::endl; return true; @@ -612,7 +616,7 @@ namespace spot sscc.rem().splice(sscc.rem().end(), rem); if (sscc.top().is_accepting) { - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); trace << "PASS 2: SUCCESS" << std::endl; return true; @@ -620,20 +624,20 @@ namespace spot } } - clear(h, todo, init_set); + clear(h, todo, ta_init_it_); return false; } void ta_check::clear(numbered_state_heap* h, std::stack todo, - std::stack init_states) + std::queue init_states) { set_states(states() + h->size()); while (!init_states.empty()) { - a_->free_state(init_states.top()); + a_->free_state(init_states.front()); init_states.pop(); } @@ -647,6 +651,27 @@ namespace spot delete h; } + + void + ta_check::clear(numbered_state_heap* h, std::stack todo, + spot::ta_succ_iterator* init_states_it) + { + + set_states(states() + h->size()); + + delete init_states_it; + + // Release all iterators in TODO. + while (!todo.empty()) + { + delete todo.top().second; + todo.pop(); + dec_depth(); + } + delete h; + } + + std::ostream& ta_check::print_stats(std::ostream& os) const { diff --git a/src/taalgos/emptinessta.hh b/src/taalgos/emptinessta.hh index 9e1861f71..60a8d4421 100644 --- a/src/taalgos/emptinessta.hh +++ b/src/taalgos/emptinessta.hh @@ -29,6 +29,7 @@ #include "tgbaalgos/gtec/nsheap.hh" #include "tgbaalgos/emptiness_stats.hh" #include +#include namespace spot { @@ -69,8 +70,13 @@ namespace spot protected: void - clear(numbered_state_heap* h, std::stack todo, std::stack< + clear(numbered_state_heap* h, std::stack todo, std::queue< spot::state*> init_set); + + void + clear(numbered_state_heap* h, std::stack todo, + spot::ta_succ_iterator* init_states_it); + bool heuristic_livelock_detection(const state * stuttering_succ, numbered_state_heap* h, int h_livelock_root, std::setcreate_transition(source, bdd_setxor( source->get_tgba_condition(), - dest->get_tgba_condition()), dest); + dest->get_tgba_condition()), bddfalse, dest); } } @@ -154,12 +154,7 @@ namespace spot state_ta_explicit* artificial_livelock_accepting_state) { - state_ta_explicit* artificial_livelock_accepting_state_added = - testing_automata->add_state(artificial_livelock_accepting_state); - - // unique artificial_livelock_accepting_state - assert(artificial_livelock_accepting_state_added - == artificial_livelock_accepting_state); + testing_automata->add_state(artificial_livelock_accepting_state); ta::states_set_t states_set = testing_automata->get_states_set(); ta::states_set_t::iterator it; @@ -182,7 +177,7 @@ namespace spot { state_ta_explicit* dest = (*it_trans)->dest; - if (dest->is_livelock_accepting_state() && !dest->is_accepting_state()) + if (dest->is_livelock_accepting_state()) { conditions_to_livelock_accepting_states->insert( (*it_trans)->condition); @@ -214,7 +209,7 @@ namespace spot != conditions_to_livelock_accepting_states->end(); it_conditions++) { - testing_automata->create_transition(source, (*it_conditions), + testing_automata->create_transition(source, (*it_conditions),bddfalse, artificial_livelock_accepting_state); } diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc index 9a4f5f330..134c6d8fe 100644 --- a/src/taalgos/tgba2ta.cc +++ b/src/taalgos/tgba2ta.cc @@ -18,7 +18,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. -#define TRACE +//#define TRACE #include #ifdef TRACE @@ -27,8 +27,6 @@ #define trace while (0) std::clog #endif - - #include "ltlast/atomic_prop.hh" #include "ltlast/constant.hh" #include "tgba/formula2bdd.hh" @@ -41,36 +39,25 @@ #include #include "tgba2ta.hh" #include "taalgos/statessetbuilder.hh" +#include "ta/tgbtaexplicit.hh" using namespace std; namespace spot { - ta* - tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_, + ta_explicit* + build_ta(ta_explicit* ta, bdd atomic_propositions_set_, bool artificial_initial_state_mode, bool artificial_livelock_accepting_state_mode, bool degeneralized) { - ta_explicit* ta; std::stack todo; + const tgba* tgba_ = ta->get_tgba(); // build Initial states set: state* tgba_init_state = tgba_->get_init_state(); - if (artificial_initial_state_mode) - { - state_ta_explicit* ta_init_state = new state_ta_explicit( - tgba_init_state->clone(), bddtrue, true); - - ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(),ta_init_state); - } - else - { - ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions()); - } - bdd tgba_condition = tgba_->support_conditions(tgba_init_state); bdd satone_tgba_condition; @@ -174,8 +161,8 @@ namespace spot { state_ta_explicit* artificial_livelock_accepting_state = - new state_ta_explicit(ta->get_tgba()->get_init_state(), bddfalse, - false, false, true, 0); + new state_ta_explicit(ta->get_tgba()->get_init_state(), bddtrue, + false, false, true, 0); add_artificial_livelock_accepting_state(ta, artificial_livelock_accepting_state); @@ -186,6 +173,34 @@ namespace spot } + ta_explicit* + tgba_to_ta(const tgba* tgba_, bdd atomic_propositions_set_, + bool artificial_initial_state_mode, + bool artificial_livelock_accepting_state_mode, bool degeneralized) + { + ta_explicit* ta; + + state* tgba_init_state = tgba_->get_init_state(); + if (artificial_initial_state_mode) + { + state_ta_explicit* ta_init_state = new state_ta_explicit( + tgba_init_state->clone(), bddfalse, true); + + ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions(), + ta_init_state); + } + else + { + ta = new spot::ta_explicit(tgba_, tgba_->all_acceptance_conditions()); + } + tgba_init_state->destroy(); + + // build ta automata: + build_ta(ta, atomic_propositions_set_, artificial_initial_state_mode, + artificial_livelock_accepting_state_mode, degeneralized); + return ta; + } + void add_artificial_livelock_accepting_state(ta_explicit* testing_automata, state_ta_explicit* artificial_livelock_accepting_state) @@ -219,8 +234,13 @@ namespace spot { state_ta_explicit* dest = (*it_trans)->dest; + state_ta_explicit::transitions* dest_trans = + (dest)->get_transitions(); + bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + + //TODO TA++ if (dest->is_livelock_accepting_state() - && !dest->is_accepting_state()) + && (!dest->is_accepting_state() || dest_trans_empty)) { conditions_to_livelock_accepting_states->insert( (*it_trans)->condition); @@ -228,9 +248,7 @@ namespace spot } //remove hole successors states - state_ta_explicit::transitions* dest_trans = - (dest)->get_transitions(); - bool dest_trans_empty = dest_trans == 0 || dest_trans->empty(); + if (dest_trans_empty) { source->get_transitions((*it_trans)->condition)->remove( @@ -253,7 +271,7 @@ namespace spot { testing_automata->create_transition(source, (*it_conditions), - artificial_livelock_accepting_state); + bddfalse, artificial_livelock_accepting_state); } } @@ -276,7 +294,7 @@ namespace spot scc_stack_ta sscc; // * arc, a stack of acceptance conditions between each of these SCC, - std::stack arc; + std::stack arc; // * h: a hash of all visited nodes, with their order, // (it is called "Hash" in Couvreur's paper) @@ -313,7 +331,7 @@ namespace spot state_ta_explicit* init = down_cast (init_set.top()); init_set.pop(); - state_ta_explicit* init_clone = init->clone(); + state_ta_explicit* init_clone = init; numbered_state_heap::state_index_p h_init = h->find(init_clone); if (h_init.first) @@ -335,7 +353,7 @@ namespace spot state* curr = todo.top().first; - numbered_state_heap::state_index_p spi = h->find(curr->clone()); + numbered_state_heap::state_index_p spi = h->find(curr); // If we have reached a dead component, ignore it. if (*spi.second == -1) { @@ -356,7 +374,7 @@ namespace spot // fill rem with any component removed, numbered_state_heap::state_index_p spi = - h->index(curr->clone()); + h->index(curr); assert(spi.first); sscc.rem().push_front(curr); @@ -369,14 +387,14 @@ namespace spot { // removing states std::list::iterator i; - bool is_livelock_accepting_sscc = (sscc.top().is_accepting - && (sscc.rem().size() > 1)) || (sscc.top().condition - == testing_automata->all_acceptance_conditions()); + bool is_livelock_accepting_sscc = (sscc.rem().size() > 1) + && ((sscc.top().is_accepting) || (sscc.top().condition + == testing_automata->all_acceptance_conditions())); for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i) { numbered_state_heap::state_index_p spi = h->index( - (*i)->clone()); + (*i)); assert(spi.first->compare(*i) == 0); assert(*spi.second != -1); *spi.second = -1; @@ -421,7 +439,7 @@ namespace spot bool is_stuttering_transition = testing_automata->get_state_condition(curr) == testing_automata->get_state_condition(dest); - state* dest_clone = dest->clone(); + state* dest_clone = dest; spi = h->find(dest_clone); // Is this a new state? @@ -452,8 +470,8 @@ namespace spot if (*spi.second == -1) continue; - trace - << "***compute_livelock_acceptance_states: CYCLE***" << std::endl; + trace << "***compute_livelock_acceptance_states: CYCLE***" + << std::endl; if (!curr->compare(dest)) { @@ -461,10 +479,13 @@ namespace spot down_cast (curr); assert(self_loop_state); - if (testing_automata->is_accepting_state(self_loop_state)) + if (testing_automata->is_accepting_state(self_loop_state) + || (acc_cond + == testing_automata->all_acceptance_conditions())) self_loop_state->set_livelock_accepting_state(true); trace - << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" << std::endl; + << "***compute_livelock_acceptance_states: CYCLE: self_loop_state***" + << std::endl; } @@ -483,7 +504,6 @@ namespace spot std::list rem; bool acc = false; - while (threshold < sscc.top().index) { assert(!sscc.empty()); @@ -496,7 +516,6 @@ namespace spot arc.pop(); } - // Note that we do not always have // threshold == sscc.top().index // after this loop, the SSCC whose index is threshold might have @@ -514,4 +533,73 @@ namespace spot delete h; } + + tgbta_explicit* + tgba_to_tgbta(const tgba* tgba_, bdd atomic_propositions_set_) + { + + state* tgba_init_state = tgba_->get_init_state(); + state_ta_explicit* ta_init_state = new state_ta_explicit( + tgba_init_state->clone(), bddfalse, true); + tgba_init_state->destroy(); + + tgbta_explicit* tgbta = new spot::tgbta_explicit(tgba_, + tgba_->all_acceptance_conditions(), ta_init_state); + + // build ta automata: + build_ta(tgbta, atomic_propositions_set_, true, true, false); + + trace << "***tgba_to_tgbta: POST build_ta***" << std::endl; + + // adapt a ta automata to build tgbta automata : + ta::states_set_t states_set = tgbta->get_states_set(); + ta::states_set_t::iterator it; + tgba_succ_iterator* initial_states_iter = tgbta->succ_iter( + tgbta->get_artificial_initial_state()); + initial_states_iter->first(); + if (initial_states_iter->done()) + return tgbta; + bdd first_state_condition = (initial_states_iter)->current_condition(); + delete initial_states_iter; + + bdd bdd_stutering_transition = bdd_setxor(first_state_condition, + first_state_condition); + + for (it = states_set.begin(); it != states_set.end(); it++) + { + + state_ta_explicit* state = static_cast (*it); + + state_ta_explicit::transitions* trans = state->get_transitions(); + if (state->is_livelock_accepting_state()) + { + + bool trans_empty = (trans == 0 || trans->empty()); + if (trans_empty) + { + trace + << "***tgba_to_tgbta: PRE if (state->is_livelock_accepting_state()) ... create_transition ***" + << std::endl; + tgbta->create_transition(state, bdd_stutering_transition, + tgbta->all_acceptance_conditions(), state); + trace + << "***tgba_to_tgbta: POST if (state->is_livelock_accepting_state()) ... create_transition ***" + << std::endl; + + } + //state->set_livelock_accepting_state(false); + } + + if (state->compare(tgbta->get_artificial_initial_state())) + tgbta->create_transition(state, bdd_stutering_transition, bddfalse, + state); + + trace << "***tgba_to_tgbta: POST create_transition ***" << std::endl; + + } + + return tgbta; + + } + } diff --git a/src/taalgos/tgba2ta.hh b/src/taalgos/tgba2ta.hh index 4e37e9857..f0930500f 100644 --- a/src/taalgos/tgba2ta.hh +++ b/src/taalgos/tgba2ta.hh @@ -30,10 +30,11 @@ #include #include "misc/bddlt.hh" #include "ta/taexplicit.hh" +#include "ta/tgbtaexplicit.hh" namespace spot { - ta* + ta_explicit* tgba_to_ta(const tgba* tgba_to_convert, bdd atomic_propositions_set, bool artificial_initial_state_mode = true, bool artificial_livelock_accepting_state_mode = false, @@ -46,6 +47,9 @@ namespace spot add_artificial_livelock_accepting_state(ta_explicit* testing_automata, state_ta_explicit* artificial_livelock_accepting_state); + tgbta_explicit* + tgba_to_tgbta(const tgba* tgba_to_convert, bdd atomic_propositions_set); + } #endif // SPOT_TGBAALGOS_SBA2TA_HH diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 336bae24d..c6543d344 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -292,6 +292,9 @@ syntax(char* prog) << std::endl << std::endl << " -in Translate an LTL formula into a Testing automata without artificial initial state" + << std::endl + << std::endl + << " -TGBTA Translate an LTL formula into a TGBTA" << std::endl; @@ -354,6 +357,7 @@ main(int argc, char** argv) bool reduction_dir_sim = false; spot::tgba* temp_dir_sim = 0; bool ta_opt = false; + bool tgbta_opt = false; bool opt_with_artificial_livelock = false; bool opt_with_artificial_initial_state = true; @@ -693,6 +697,10 @@ main(int argc, char** argv) ta_opt = true; opt_minimize = true; } + else if (!strcmp(argv[formula_index], "-TGBTA")) + { + tgbta_opt = true; + } else if (!strcmp(argv[formula_index], "-lv")) { opt_with_artificial_livelock = true; @@ -1088,6 +1096,20 @@ main(int argc, char** argv) break; } +//TA + 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( + (a->get_dict())->var_map[*i]); + + atomic_props_set_bdd &= atomic_prop; + + } + delete aps; if (ta_opt) { @@ -1097,22 +1119,19 @@ main(int argc, char** argv) // 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( - (a->get_dict())->var_map[*i]); - atomic_props_set_bdd &= atomic_prop; + spot::ta* testing_automata = 0; + if (tgbta_opt) + { + testing_automata = (spot::ta_explicit *) tgba_to_tgbta(a, atomic_props_set_bdd); - } - delete aps; + } + else { + testing_automata = tgba_to_ta(a, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock, degeneralize_opt == DegenSBA); - spot::ta* testing_automata = tgba_to_ta(a, atomic_props_set_bdd, opt_with_artificial_initial_state, opt_with_artificial_livelock, degeneralize_opt == DegenSBA); - spot::ta* testing_automata_nm = 0; + } + spot::ta* testing_automata_nm = 0; if (opt_minimize) { testing_automata_nm = testing_automata; testing_automata = minimize_ta(testing_automata); @@ -1141,6 +1160,11 @@ main(int argc, char** argv) degeneralized = 0; output = -1; + } else if (tgbta_opt) + { + a = tgba_to_tgbta(a, atomic_props_set_bdd); + to_free = a; + } spot::tgba* product_degeneralized = 0;