diff --git a/bench/ltlcounter/Makefile.am b/bench/ltlcounter/Makefile.am index 543b45379..a18041d68 100644 --- a/bench/ltlcounter/Makefile.am +++ b/bench/ltlcounter/Makefile.am @@ -1,5 +1,5 @@ -# Copyright (C) 2009 Laboratoire de Recherche et Développement de -# l'EPITA (LRDE) +# Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement +# de l'EPITA (LRDE) # # This file is part of Spot, a model checking library. # @@ -18,4 +18,4 @@ EXTRA_DIST = run plot.gnu -CLEANFILES = results.fm results.lacim results.fm.eps results.lacim.eps +CLEANFILES = results.fm results.taa results.fm.eps results.taa.eps diff --git a/bench/ltlcounter/README b/bench/ltlcounter/README index aedfbb9bc..d3e30ad66 100644 --- a/bench/ltlcounter/README +++ b/bench/ltlcounter/README @@ -20,5 +20,5 @@ This benchmark used this familly of formulae to plot the performance of the ltl2tgba_fm algorithm. Studying the behaviour of ltl2tgba_fm on this class of formulae helped us to improve the translation. -Execute "./run" to compute the raw numbers, then execture +Execute "./run" to compute the raw numbers, then execute "gnuplot plot.gnu" to plot the figures. diff --git a/bench/ltlcounter/plot.gnu b/bench/ltlcounter/plot.gnu index 86a8a9e10..09b3a6106 100644 --- a/bench/ltlcounter/plot.gnu +++ b/bench/ltlcounter/plot.gnu @@ -15,11 +15,11 @@ plot 'results.fm' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ with lines title "States" -set output 'results.lacim.eps' +set output 'results.taa.eps' -plot 'results.lacim' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ +plot 'results.taa' using 1:($4+$5) '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ with filledcurve x1 title "Total Time" axes x1y2, \ - 'results.lacim' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + 'results.taa' using 1:4 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ with filledcurve x1 title "Translation Time" axes x1y2, \ - 'results.lacim' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ + 'results.taa' using 1:2 '%lf,%lf,%lf,%lf,%*lf,%*lf,%lf,%*lf,%*lf' \ with lines title "States" diff --git a/bench/ltlcounter/run b/bench/ltlcounter/run index 5ee0cd7da..6124f2d12 100755 --- a/bench/ltlcounter/run +++ b/bench/ltlcounter/run @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche -# et Développement de l'EPITA (LRDE) +# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +# Recherche et Développement de l'EPITA (LRDE) # # This file is part of Spot, a model checking library. # @@ -35,18 +35,18 @@ for n in 1 2 3 4 5 6 7 8 9 10 11 12 13; do echo $n,$states,$transitions,$time,$time2 done | tee results.fm -echo "# Benching ltl2tgba_lacim..." -echo "# the following values are also saved to file 'results.lacim'" +echo "# Benching ltl2taa..." +echo "# the following values are also saved to file 'results.taa'" echo "# time1 = translation time" echo "# time2 = exploration time" echo "# n, states, transitions, user time1, system time1, wall time1, user time1, system time2, wall time2" for n in 1 2 3 4 5 6 7; do - $LTL2TGBA -T -ks -l "`$gen --rv-counter-linear $n`" >out 2>&1 + $LTL2TGBA -T -ks -taa "`$gen --rv-counter-linear $n`" >out 2>&1 states=`sed -n 's/^states: \([0-9]*\)$/\1/p' out` transitions=`sed -n 's/^transitions: \([0-9]*\)$/\1/p' out` time=`sed -n 's/ *translating formula *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out` time2=`sed -n 's/ *producing output *| *\([0-9]*\) .*| *\([0-9]*\) .*| *\([0-9]*\) .*|.*/\1,\2,\3/p' out` echo $n,$states,$transitions,$time,$time2 -done | tee results.lacim +done | tee results.taa echo "# now run 'gnuplot plot.gnu'" diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 328e07c84..20a11daf8 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -30,19 +30,11 @@ tgba_HEADERS = \ bddprint.hh \ formula2bdd.hh \ futurecondcol.hh \ - public.hh \ sba.hh \ state.hh \ - statebdd.hh \ succiter.hh \ - succiterconcrete.hh \ taatgba.hh \ tgba.hh \ - tgbabddconcrete.hh \ - tgbabddconcretefactory.hh \ - tgbabddconcreteproduct.hh \ - tgbabddcoredata.hh \ - tgbabddfactory.hh \ tgbaexplicit.hh \ tgbagraph.hh \ tgbakvcomplement.hh \ @@ -62,14 +54,8 @@ libtgba_la_SOURCES = \ bddprint.cc \ formula2bdd.cc \ futurecondcol.cc \ - succiterconcrete.cc \ - statebdd.cc \ taatgba.cc \ tgba.cc \ - tgbabddconcrete.cc \ - tgbabddconcretefactory.cc \ - tgbabddconcreteproduct.cc \ - tgbabddcoredata.cc \ tgbaexplicit.cc \ tgbakvcomplement.cc \ tgbaproduct.cc \ diff --git a/src/tgba/public.hh b/src/tgba/public.hh deleted file mode 100644 index e1b9cd8e8..000000000 --- a/src/tgba/public.hh +++ /dev/null @@ -1,38 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// Copyright (C) 2003 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_TGBA_PUBLIC_HH -# define SPOT_TGBA_PUBLIC_HH - -// This file should not exist. -#if __GNUC__ -#ifndef SKIP_DEPRECATED_WARNING -#warning This file is deprecated. Include tgba.hh or what you need. -#endif -#endif - -# include "tgba.hh" -# include "tgbabddconcrete.hh" -# include "tgbabddconcreteproduct.hh" -# include "bddprint.hh" - -#endif // SPOT_TGBA_PUBLIC_HH diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc deleted file mode 100644 index 0b5b08158..000000000 --- a/src/tgba/statebdd.cc +++ /dev/null @@ -1,53 +0,0 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003 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 "statebdd.hh" -#include -#include - -namespace spot -{ - - int - state_bdd::compare(const state* other) const - { - // This method should not be called to compare states from different - // automata, and all states from the same automaton will use the same - // state class. - const state_bdd* o = down_cast(other); - assert(o); - return o->as_bdd().id() - state_.id(); - } - - size_t - state_bdd::hash() const - { - return state_.id(); - } - - /// Duplicate a state. - state_bdd* - state_bdd::clone() const - { - return new state_bdd(*this); - } - -} diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh deleted file mode 100644 index 355feac98..000000000 --- a/src/tgba/statebdd.hh +++ /dev/null @@ -1,57 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita. -// 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_TGBA_STATEBDD_HH -# define SPOT_TGBA_STATEBDD_HH - -#include -#include "state.hh" - -namespace spot -{ - /// A state whose representation is a BDD. - /// \ingroup tgba_representation - class SPOT_API state_bdd: public state - { - public: - state_bdd(bdd s) - : state_(s) - { - } - - /// Return the BDD part of the state. - virtual bdd - as_bdd() const - { - return state_; - } - - virtual int compare(const state* other) const; - virtual size_t hash() const; - virtual state_bdd* clone() const; - - protected: - bdd state_; ///< BDD representation of the state. - }; -} - -#endif // SPOT_TGBA_STATEBDD_HH diff --git a/src/tgba/succiterconcrete.cc b/src/tgba/succiterconcrete.cc deleted file mode 100644 index bd5df3bc0..000000000 --- a/src/tgba/succiterconcrete.cc +++ /dev/null @@ -1,193 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003 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 "succiterconcrete.hh" -#include - -namespace spot -{ - tgba_succ_iterator_concrete::~tgba_succ_iterator_concrete() - { - } - - bool - tgba_succ_iterator_concrete::first() - { - succ_set_left_ = succ_set_; - current_ = bddfalse; - if (!done()) - return next(); - else - return false; - } - - bool - tgba_succ_iterator_concrete::next() - { - assert(!done()); - // succ_set_ is the set of successors we have to explore. it - // contains Now/Next variables and atomic propositions. Each - // satisfaction of succ_set_ represents a transition, and we want - // to compute as few transitions as possible. However one - // important constraint is that all Next variables must appear in - // the satisfaction. - // - // The full satisfactions of succ_set_ maybe something - // like this (ignoring Now variables): - // a & b & Next[a] & Next[b] - // !a & b & Next[a] & Next[b] - // a & !b & Next[a] & Next[b] - // a & b & Next[a] & !Next[b] - // This denotes four transitions, three of which going to - // the same node. Obviously (a&b | !a&b | a&!b) - // == (a | b), so it's tempting to replace these four - // transitions by - // (a + b) & Next[a] & Next[b] - // a & b & Next[a] & !Next[b] - // Is this always correct? No! It depends on the - // acceptance conditions associated to each transition. - // We cannot merge transitions which have different - // acceptance conditions. - // Let's label transitions with hypothetic acceptance sets: - // a & b & Next[a] & Next[b] ; Acc[1] - // !a & b & Next[a] & Next[b] ; Acc[1] - // a & !b & Next[a] & Next[b] ; Acc[2] - // a & b & Next[a] & !Next[b] ; Acc[1] - // Now it's pretty clear only the first two transitions - // may be merged: - // b & Next[a] & Next[b] ; Acc[1] - // a & !b & Next[a] & Next[b] ; Acc[2] - // a & b & Next[a] & !Next[b] ; Acc[1] - - do - { - // FIXME: Iterating on the successors this way (calling - // bdd_satone{,set} and NANDing out (-=) the result from a - // set) requires several descents of the BDD. Maybe it would - // be faster to compute all satisfying formulae in one - // operation. - - succ_set_left_ -= current_; - if (succ_set_left_ == bddfalse) // No more successors? - return false; - - // Pick one transition, and extract its destination. - bdd trans = bdd_satoneset(succ_set_left_, data_.next_set, - bddfalse); - bdd dest = bdd_exist(trans, data_.notnext_set); - - // Gather all transitions going to this destination... - current_ = succ_set_left_ & dest; - // ... and compute their acceptance sets. - bdd as = data_.acceptance_conditions & current_; - - // AS is false when no satisfaction of the current transition - // belongs to an acceptance set: current_ can be used as-is. - if (as != bddfalse) - { - // Otherwise, we have acceptance sets, and we should - // restrict current_ to a subset sharing the same - // acceptance conditions. - // same acceptance set. - - as = bdd_exist(as, data_.nownext_set); - // as = (a | (!a)&b) & (Acc[a] | Acc[b]) + (!a & Acc[b]) - bdd cube = bdd_satone(as); - // cube = (!ab & Acc[a]) - bdd prop = bdd_exist(cube, data_.acc_set); - // prop = (!a)&b - current_acc_ = bdd_forall(bdd_restrict(as, prop), data_.var_set); - // current_acc_ = (Acc[a] | Acc[b]) - assert(current_acc_ != bddfalse); - // Find other transitions included exactly in each of these - // acceptance sets and are not included in other sets. - // Consider - // !p.!Acc[g].Acc[f] + p.!Acc[g].Acc[f] + p.Acc[g].!Acc[f] - // if current_acc_ = !Acc[g].Acc[f] we - // want to compute !p, not (!p + p), because p really - // belongs to !Acc[g].Acc[f] + Acc[g].!Acc[f], not - // only !Acc[g].Acc[f]. - // So, first, filter out all transitions like p, which - // are also in other acceptance sets. - bdd fout = bdd_relprod(as, !current_acc_, data_.acc_set); - bdd as_fout = as - fout; - // Then, pick the remaining term that are exactly in all - // required acceptance sets. - bdd all = bddtrue; - bdd acc = current_acc_; - do - { - bdd one_acc = bdd_satone(acc); - acc -= one_acc; - all &= bdd_relprod(as_fout, one_acc, data_.acc_set); - } - while (acc != bddfalse); - // all = (a | (!a)&b) & (Acc[a] | Acc[b]) - current_ = all & dest; - // current_ = (a | (!a)&b) & (Next...) - } - else - { - current_acc_ = bddfalse; - } - - assert(current_ != bddfalse); - // The destination state, computed here, should be compatible - // with the transition relation. Otherwise it won't have any - // successor (a dead node) and we can skip it. We need to - // compute current_state_ anyway, so this test costs us nothing. - assert(dest == bdd_exist(current_, data_.notnext_set)); - current_state_ = bdd_replace(dest, data_.dict->next_to_now); - } - while ((current_state_ & data_.relation) == bddfalse); - - return succ_set_left_ != bddfalse; - } - - bool - tgba_succ_iterator_concrete::done() const - { - return succ_set_left_ == bddfalse; - } - - state_bdd* - tgba_succ_iterator_concrete::current_state() const - { - assert(!done()); - return new state_bdd(current_state_); - } - - bdd - tgba_succ_iterator_concrete::current_condition() const - { - assert(!done()); - return bdd_exist(current_, data_.notvar_set); - } - - bdd - tgba_succ_iterator_concrete::current_acceptance_conditions() const - { - assert(!done()); - return current_acc_; - } - -} diff --git a/src/tgba/succiterconcrete.hh b/src/tgba/succiterconcrete.hh deleted file mode 100644 index b9eebbc75..000000000 --- a/src/tgba/succiterconcrete.hh +++ /dev/null @@ -1,86 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// 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_TGBA_SUCCITERCONCRETE_HH -# define SPOT_TGBA_SUCCITERCONCRETE_HH - -#include "statebdd.hh" -#include "succiter.hh" -#include "tgbabddcoredata.hh" - -namespace spot -{ - /// A concrete iterator over successors of a TGBA state. - /// \ingroup tgba_representation - class SPOT_API tgba_succ_iterator_concrete: - public tgba_succ_iterator - { - public: - /// \brief Build a spot::tgba_succ_iterator_concrete. - /// - /// \param successors The set of successors with ingoing - /// conditions and acceptance conditions, represented as a BDD. - /// The job of this iterator will be to enumerate the - /// satisfactions of that BDD and split them into destination - /// states and conditions, and compute acceptance conditions. - /// \param d The core data of the automata. - /// These contains sets of variables useful to split a BDD, and - /// compute acceptance conditions. - tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors) - : data_(d) - { - recycle(successors); - } - - void recycle(bdd successors) - { - succ_set_ = successors; - succ_set_left_ = successors; - current_ = bddfalse; - } - - virtual ~tgba_succ_iterator_concrete(); - - // iteration - bool first(); - bool next(); - bool done() const; - - // inspection - state_bdd* current_state() const; - bdd current_condition() const; - bdd current_acceptance_conditions() const; - - private: - const tgba_bdd_core_data& data_; ///< Core data of the automaton. - bdd succ_set_; ///< The set of successors. - bdd succ_set_left_; ///< Unexplored successors (including current_). - bdd current_; ///< \brief Current successor, as a conjunction of - /// atomic proposition and Next variables. - bdd current_state_; ///< \brief Current successor, as a - /// conjunction of Now variables. - bdd current_acc_; ///< \brief Acceptance conditions for the current - /// transition. - }; -} - -#endif // SPOT_TGBA_SUCCITERCONCRETE_HH diff --git a/src/tgba/tgbabddconcrete.cc b/src/tgba/tgbabddconcrete.cc deleted file mode 100644 index bf0c70146..000000000 --- a/src/tgba/tgbabddconcrete.cc +++ /dev/null @@ -1,160 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2014 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003 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 "tgbabddconcrete.hh" -#include "bddprint.hh" -#include - -namespace spot -{ - tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact) - : data_(fact.get_core_data()) - { - get_dict()->register_all_variables_of(&fact, this); - } - - tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init) - : data_(fact.get_core_data()) - { - get_dict()->register_all_variables_of(&fact, this); - set_init_state(init); - } - - tgba_bdd_concrete::~tgba_bdd_concrete() - { - get_dict()->unregister_all_my_variables(this); - } - - void - tgba_bdd_concrete::set_init_state(bdd s) - { - // Usually, the ltl2tgba translator will return an - // initial state which does not include all true Now variables, - // even though the truth of some Now variables is garanteed. - // - // For instance, when building the automata for the formula GFa, - // the translator will define the following two equivalences - // Now[Fa] <=> a | (Prom[a] & Next[Fa]) - // Now[GFa] <=> Now[Fa] & Next[GFa] - // and return Now[GFa] as initial state. - // - // Starting for state Now[GFa], we could then build - // the following automaton: - // In state Now[GFa]: - // if `a', go to state Now[GFa] & Now[Fa] - // if `!a', go to state Now[GFa] & Now[Fa] with Prom[a] - // In state Now[GFa] & Now[Fa]: - // if `a', go to state Now[GFa] & Now[Fa] - // if `!a', go to state Now[GFa] & Now[Fa] with Prom[a] - // - // As we can see, states Now[GFa] and Now[GFa] & Now[Fa] share - // the same actions. This is no surprise, because - // Now[GFa] <=> Now[GFa] & Now[Fa] according to the equivalences - // defined by the translator. - // - // This happens because we haven't completed the initial - // state with the value of other Now variables. We can - // complete this state with the other equivalant Now variables - // here, but we can't do anything about the remaining unknown - // variables. - s &= bdd_relprod(s, data_.relation, data_.notnow_set); - init_ = s; - } - - state_bdd* - tgba_bdd_concrete::get_init_state() const - { - return new state_bdd(init_); - } - - bdd - tgba_bdd_concrete::get_init_bdd() const - { - return init_; - } - - tgba_succ_iterator_concrete* - tgba_bdd_concrete::succ_iter(const state* state) const - { - const state_bdd* s = down_cast(state); - assert(s); - bdd succ_set = data_.relation & s->as_bdd(); - // Do not allocate an iterator if we can reuse one. - if (iter_cache_) - { - tgba_succ_iterator_concrete* res = - down_cast(iter_cache_); - iter_cache_ = nullptr; - res->recycle(succ_set); - return res; - } - return new tgba_succ_iterator_concrete(data_, succ_set); - } - - bdd - tgba_bdd_concrete::compute_support_conditions(const state* st) const - { - const state_bdd* s = down_cast(st); - assert(s); - return bdd_relprod(s->as_bdd(), data_.relation, data_.notvar_set); - } - - std::string - tgba_bdd_concrete::format_state(const state* state) const - { - const state_bdd* s = down_cast(state); - assert(s); - return bdd_format_set(get_dict(), s->as_bdd()); - } - - bdd_dict* - tgba_bdd_concrete::get_dict() const - { - return data_.dict; - } - - bdd - tgba_bdd_concrete::all_acceptance_conditions() const - { - return data_.all_acceptance_conditions; - } - - bdd - tgba_bdd_concrete::neg_acceptance_conditions() const - { - return data_.negacc_set; - } - - const tgba_bdd_core_data& - tgba_bdd_concrete::get_core_data() const - { - return data_; - } - - void - tgba_bdd_concrete::delete_unaccepting_scc() - { - data_.delete_unaccepting_scc(init_); - set_init_state(init_); - } - -} diff --git a/src/tgba/tgbabddconcrete.hh b/src/tgba/tgbabddconcrete.hh deleted file mode 100644 index 69dc1f8ec..000000000 --- a/src/tgba/tgbabddconcrete.hh +++ /dev/null @@ -1,97 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014 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 . - -#ifndef SPOT_TGBA_TGBABDDCONCRETE_HH -# define SPOT_TGBA_TGBABDDCONCRETE_HH - -#include "tgba.hh" -#include "statebdd.hh" -#include "tgbabddfactory.hh" -#include "succiterconcrete.hh" - -namespace spot -{ - /// \ingroup tgba_representation - /// \brief A concrete spot::tgba implemented using BDDs. - class SPOT_API tgba_bdd_concrete: public tgba - { - public: - /// \brief Construct a tgba_bdd_concrete with unknown initial state. - /// - /// set_init_state() should be called later. - tgba_bdd_concrete(const tgba_bdd_factory& fact); - - /// \brief Construct a tgba_bdd_concrete with known initial state. - tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init); - - virtual ~tgba_bdd_concrete(); - - /// \brief Set the initial state. - virtual void set_init_state(bdd s); - - virtual state_bdd* get_init_state() const; - - /// \brief Get the initial state directly as a BDD. - /// - /// The sole point of this method is to prevent writing - /// horrors such as - /// \code - /// state_bdd* s = automata.get_init_state(); - /// some_class some_instance(s->as_bdd()); - /// s->destroy(); - /// \endcode - bdd get_init_bdd() const; - - virtual tgba_succ_iterator_concrete* - succ_iter(const state* local_state) const; - - virtual std::string format_state(const state* state) const; - - virtual bdd_dict* get_dict() const; - - /// \brief Get the core data associated to this automaton. - /// - /// These data includes the various BDD used to represent - /// the relation, encode variable sets, Next-to-Now rewrite - /// rules, etc. - const tgba_bdd_core_data& get_core_data() const; - - virtual bdd all_acceptance_conditions() const; - virtual bdd neg_acceptance_conditions() const; - - /// \brief Delete SCCs (Strongly Connected Components) from the - /// TGBA which cannot be accepting. - void delete_unaccepting_scc(); - - protected: - virtual bdd compute_support_conditions(const state* state) const; - - tgba_bdd_core_data data_; ///< Core data associated to the automaton. - bdd init_; ///< Initial state. - private: - // Disallow copy. - tgba_bdd_concrete(const tgba_bdd_concrete&) SPOT_DELETED; - tgba_bdd_concrete& operator=(const tgba_bdd_concrete&) SPOT_DELETED; - }; -} - -#endif // SPOT_TGBA_TGBABDDCONCRETE_HH diff --git a/src/tgba/tgbabddconcretefactory.cc b/src/tgba/tgbabddconcretefactory.cc deleted file mode 100644 index 3d109e3bd..000000000 --- a/src/tgba/tgbabddconcretefactory.cc +++ /dev/null @@ -1,149 +0,0 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003 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 "tgbabddconcretefactory.hh" - -namespace spot -{ - tgba_bdd_concrete_factory::tgba_bdd_concrete_factory(bdd_dict* dict) - : data_(dict) - { - } - - tgba_bdd_concrete_factory::~tgba_bdd_concrete_factory() - { - acc_map_::iterator ai; - for (ai = acc_.begin(); ai != acc_.end(); ++ai) - ai->first->destroy(); - get_dict()->unregister_all_my_variables(this); - } - - int - tgba_bdd_concrete_factory::create_state(const ltl::formula* f) - { - int num = get_dict()->register_state(f, this); - // Keep track of all "Now" variables for easy - // existential quantification. - data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1)); - return num; - } - - int - tgba_bdd_concrete_factory::create_anonymous_state() - { - int num = get_dict()->register_anonymous_variables(2, this); - bdd_setpair(get_dict()->next_to_now, num + 1, num); - bdd_setpair(get_dict()->now_to_next, num, num + 1); - // Keep track of all "Now" variables for easy - // existential quantification. - data_.declare_now_next (bdd_ithvar(num), bdd_ithvar(num + 1)); - return num; - } - - int - tgba_bdd_concrete_factory::create_atomic_prop(const ltl::formula* f) - { - int num = get_dict()->register_proposition(f, this); - // Keep track of all atomic proposition for easy - // existential quantification. - data_.declare_atomic_prop(bdd_ithvar(num)); - return num; - } - - void - tgba_bdd_concrete_factory::declare_acceptance_condition(bdd b, - const ltl::formula* a) - { - // Maintain a conjunction of BDDs associated to A. We will latter - // (in tgba_bdd_concrete_factory::finish()) associate this - // conjunction to A. - acc_map_::iterator ai = acc_.find(a); - if (ai == acc_.end()) - { - a = a->clone(); - acc_[a] = b; - } - else - { - ai->second &= b; - } - } - - void - tgba_bdd_concrete_factory::finish() - { - acc_map_::iterator ai; - for (ai = acc_.begin(); ai != acc_.end(); ++ai) - { - // Register a BDD variable for this acceptance condition. - int num = get_dict()->register_acceptance_variable(ai->first, this); - // Keep track of all acceptance conditions for easy - // existential quantification. - data_.declare_acceptance_condition(bdd_ithvar(num)); - } - for (ai = acc_.begin(); ai != acc_.end(); ++ai) - { - bdd acc = bdd_ithvar(get_dict()->acc_map[ai->first]); - - // Complete acc with all the other acceptance conditions negated. - acc &= bdd_exist(data_.negacc_set, acc); - - // Any state matching the BDD formulae registered is part - // of this acceptance set. - data_.acceptance_conditions |= ai->second & acc; - - // Keep track of all acceptance conditions, so that we can - // easily check whether a transition satisfies all acceptance - // conditions. - data_.all_acceptance_conditions |= acc; - } - - data_.acceptance_conditions_support = - bdd_support(data_.acceptance_conditions); - - // Any constraint between Now variables also exist between Next - // variables. Doing this limits the quantity of useless - // successors we will have to explore. (By "useless successors" - // I mean a combination of Next variables that represent a cul de sac - // state: the combination exists but won't allow further exploration - // because it fails the constraints.) - data_.relation &= bdd_replace(bdd_exist(data_.relation, data_.notnow_set), - get_dict()->now_to_next); - } - - const tgba_bdd_core_data& - tgba_bdd_concrete_factory::get_core_data() const - { - return data_; - } - - bdd_dict* - tgba_bdd_concrete_factory::get_dict() const - { - return data_.dict; - } - - void - tgba_bdd_concrete_factory::constrain_relation(bdd new_rel) - { - data_.relation &= new_rel; - } -} diff --git a/src/tgba/tgbabddconcretefactory.hh b/src/tgba/tgbabddconcretefactory.hh deleted file mode 100644 index ca83de4a3..000000000 --- a/src/tgba/tgbabddconcretefactory.hh +++ /dev/null @@ -1,102 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). -// Copyright (C) 2003, 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_TGBA_TGBABDDCONCRETEFACTORY_HH -# define SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH - -#include "misc/hash.hh" -#include "ltlast/formula.hh" -#include "tgbabddfactory.hh" - -namespace spot -{ - /// Helper class to build a spot::tgba_bdd_concrete object. - class SPOT_API tgba_bdd_concrete_factory: public tgba_bdd_factory - { - public: - tgba_bdd_concrete_factory(bdd_dict* dict); - - virtual ~tgba_bdd_concrete_factory(); - - /// Create a Now/Next variables for formula \a f. - /// - /// \param f The formula to create a state for. - /// \return The BDD variable number v for the Now state. The - /// Next BDD corresponds to v+1. - /// - /// The state variables are not created if they already exist. - /// Instead their existing variable numbers are returned. - /// Variable numbers can be turned into BDD using ithvar(). - int create_state(const ltl::formula* f); - - /// Create a anonymous Now/Next variables. - /// - /// \return The BDD variable number v for the Now state. The - /// Next BDD corresponds to v+1. - int create_anonymous_state(); - - /// Create an atomic proposition variable for formula \a f. - /// - /// \param f The formula to create an aotmic proposition for. - /// \return The variable number for this state. - /// - /// The atomic proposition is not created if it already exists. - /// Instead its existing variable number is returned. Variable numbers - /// can be turned into BDD using ithvar(). - int create_atomic_prop(const ltl::formula* f); - - /// Declare an acceptance condition. - /// - /// Formula such as 'f U g' or 'F g' make the promise - /// that 'g' will be fulfilled eventually. So once - /// one of this formula has been translated into a BDD, - /// we use declare_acceptance_condition() to associate - /// all other states to the acceptance set of 'g'. - /// - /// \param b a BDD indicating which variables are in the - /// acceptance set - /// \param a the formula associated - void declare_acceptance_condition(bdd b, const ltl::formula* a); - - const tgba_bdd_core_data& get_core_data() const; - bdd_dict* get_dict() const; - - /// Add a new constraint to the relation. - void constrain_relation(bdd new_rel); - - /// \brief Perfom final computations before the relation can be used. - /// - /// This function should be called after all propositions, state, - /// acceptance conditions, and constraints have been declared, and - /// before calling get_code_data() or get_dict(). - void finish(); - - private: - tgba_bdd_core_data data_; ///< Core data for the new automata. - - typedef std::unordered_map acc_map_; - acc_map_ acc_; ///< BDD associated to each acceptance condition - }; - -} -#endif // SPOT_TGBA_TGBABDDCONCRETEFACTORY_HH diff --git a/src/tgba/tgbabddconcreteproduct.cc b/src/tgba/tgbabddconcreteproduct.cc deleted file mode 100644 index 68ee1381d..000000000 --- a/src/tgba/tgbabddconcreteproduct.cc +++ /dev/null @@ -1,78 +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 . - -#include -#include "tgbabddconcreteproduct.hh" - -namespace spot -{ - namespace - { - /// \brief Helper class for product(). - /// - /// As both automata are encoded using BDD, we just have - /// to homogenize the variable numbers before ANDing the - /// relations and initial states. - class tgba_bdd_product_factory: public tgba_bdd_factory - { - public: - tgba_bdd_product_factory(const tgba_bdd_concrete* left, - const tgba_bdd_concrete* right) - : dict_(left->get_dict()), - left_(left), - right_(right), - data_(left_->get_core_data(), right_->get_core_data()), - init_(left_->get_init_bdd() & right_->get_init_bdd()) - { - assert(dict_ == right->get_dict()); - } - - virtual - ~tgba_bdd_product_factory() - { - } - - const tgba_bdd_core_data& - get_core_data() const - { - return data_; - } - - bdd - get_init_state() const - { - return init_; - } - - private: - bdd_dict* dict_; - const tgba_bdd_concrete* left_; - const tgba_bdd_concrete* right_; - tgba_bdd_core_data data_; - bdd init_; - }; - } - - tgba_bdd_concrete* - product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right) - { - tgba_bdd_product_factory p(left, right); - return new tgba_bdd_concrete(p, p.get_init_state()); - } -} diff --git a/src/tgba/tgbabddconcreteproduct.hh b/src/tgba/tgbabddconcreteproduct.hh deleted file mode 100644 index 837baedd3..000000000 --- a/src/tgba/tgbabddconcreteproduct.hh +++ /dev/null @@ -1,36 +0,0 @@ -// Copyright (C) 2003, 2004, 2013 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_TGBA_TGBABDDCONCRETEPRODUCT_HH -# define SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH - -#include "tgbabddconcrete.hh" - -namespace spot -{ - /// \ingroup tgba_algorithms - /// \brief Multiplies two spot::tgba_bdd_concrete automata. - /// - /// This function builds the resulting product as another - /// spot::tgba_bdd_concrete automaton. - SPOT_API tgba_bdd_concrete* - product(const tgba_bdd_concrete* left, const tgba_bdd_concrete* right); -} - -#endif // SPOT_TGBA_TGBABDDCONCRETEPRODUCT_HH diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc deleted file mode 100644 index cc5c78165..000000000 --- a/src/tgba/tgbabddcoredata.cc +++ /dev/null @@ -1,200 +0,0 @@ -// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003 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 "tgbabddcoredata.hh" - -namespace spot -{ - tgba_bdd_core_data::tgba_bdd_core_data(bdd_dict* dict) - : relation(bddtrue), - acceptance_conditions(bddfalse), - acceptance_conditions_support(bddtrue), - all_acceptance_conditions(bddfalse), - now_set(bddtrue), - next_set(bddtrue), - nownext_set(bddtrue), - notnow_set(bddtrue), - notnext_set(bddtrue), - var_set(bddtrue), - notvar_set(bddtrue), - varandnext_set(bddtrue), - acc_set(bddtrue), - notacc_set(bddtrue), - negacc_set(bddtrue), - dict(dict) - { - } - - tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& copy) - : relation(copy.relation), - acceptance_conditions(copy.acceptance_conditions), - acceptance_conditions_support(copy.acceptance_conditions_support), - all_acceptance_conditions(copy.all_acceptance_conditions), - now_set(copy.now_set), - next_set(copy.next_set), - nownext_set(copy.nownext_set), - notnow_set(copy.notnow_set), - notnext_set(copy.notnext_set), - var_set(copy.var_set), - notvar_set(copy.notvar_set), - varandnext_set(copy.varandnext_set), - acc_set(copy.acc_set), - notacc_set(copy.notacc_set), - negacc_set(copy.negacc_set), - dict(copy.dict) - { - } - - // Merge two core_data. - tgba_bdd_core_data::tgba_bdd_core_data(const tgba_bdd_core_data& left, - const tgba_bdd_core_data& right) - : relation(left.relation & right.relation), - acceptance_conditions(left.acceptance_conditions - | right.acceptance_conditions), - acceptance_conditions_support(left.acceptance_conditions_support - & right.acceptance_conditions_support), - all_acceptance_conditions(left.all_acceptance_conditions - | right.all_acceptance_conditions), - now_set(left.now_set & right.now_set), - next_set(left.next_set & right.next_set), - nownext_set(left.nownext_set & right.nownext_set), - notnow_set(left.notnow_set & right.notnow_set), - notnext_set(left.notnext_set & right.notnext_set), - var_set(left.var_set & right.var_set), - notvar_set(left.notvar_set & right.notvar_set), - varandnext_set(left.varandnext_set & right.varandnext_set), - acc_set(left.acc_set & right.acc_set), - notacc_set(left.notacc_set & right.notacc_set), - negacc_set(left.negacc_set & right.negacc_set), - dict(left.dict) - { - assert(dict == right.dict); - } - - tgba_bdd_core_data& - tgba_bdd_core_data::operator=(const tgba_bdd_core_data& copy) - { - if (this != ©) - { - this->~tgba_bdd_core_data(); - new (this) tgba_bdd_core_data(copy); - } - return *this; - } - - void - tgba_bdd_core_data::declare_now_next(bdd now, bdd next) - { - now_set &= now; - next_set &= next; - notnext_set &= now; - notnow_set &= next; - bdd both = now & next; - nownext_set &= both; - notvar_set &= both; - notacc_set &= both; - varandnext_set &= next; - } - - void - tgba_bdd_core_data::declare_atomic_prop(bdd var) - { - notnow_set &= var; - notnext_set &= var; - notacc_set &= var; - var_set &= var; - varandnext_set &= var; - } - - void - tgba_bdd_core_data::declare_acceptance_condition(bdd acc) - { - notnow_set &= acc; - notnext_set &= acc; - notvar_set &= acc; - acc_set &= acc; - negacc_set &= !acc; - } - - void - tgba_bdd_core_data::delete_unaccepting_scc(bdd init) - { - bdd er = bdd_exist(relation, var_set); /// existsRelation - bdd s0 = bddfalse; - bdd s1 = bdd_exist(bdd_exist(init & relation, var_set), now_set); - s1 = bdd_replace(s1, dict->next_to_now); - - /// Find all reachable states - while (s0 != s1) - { - s0 = s1; - /// Compute s1 = succ(s0) | s - s1 = bdd_replace(bdd_exist(s0 & er, now_set), dict->next_to_now) | s0; - } - - /// Find states which can be visited infinitely often while seeing - /// all acceptance conditions - s0 = bddfalse; - while (s0 != s1) - { - s0 = s1; - bdd all = all_acceptance_conditions; - while (all != bddfalse) - { - bdd next = bdd_satone(all); - all -= next; - s1 = infinitely_often(s1, next, er); - } - } - - relation = (relation & bdd_replace(s0, dict->now_to_next)); - } - - bdd - tgba_bdd_core_data::infinitely_often(bdd s, bdd acc, bdd er) - { - bdd ar = acc & (relation & acceptance_conditions); /// accRelation - bdd s0 = bddfalse; - bdd s1 = s; - - while (s0 != s1) - { - s0 = s1; - bdd as = bdd_replace(s0, dict->now_to_next) & ar; - as = bdd_exist(bdd_exist(as, next_set), var_set) & s0; - - /// Do predStar - bdd s0_ = bddfalse; - bdd s1_ = bdd_exist(as, acc_set); - while (s0_ != s1_) - { - s0_ = s1_; - /// Compute s1_ = pred(s0_) | s0_ - s1_ = bdd_exist(er & bdd_replace(s0_, dict->now_to_next), next_set); - s1_ = (s1_ & s0) | s0_; - } - s1 = s0_; - } - - return s0; - } -} diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh deleted file mode 100644 index c2776a891..000000000 --- a/src/tgba/tgbabddcoredata.hh +++ /dev/null @@ -1,159 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// Copyright (C) 2003, 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_TGBA_TGBABDDCOREDATA_HH -# define SPOT_TGBA_TGBABDDCOREDATA_HH - -#include -#include "bdddict.hh" - -namespace spot -{ - /// Core data for a TGBA encoded using BDDs. - struct SPOT_API tgba_bdd_core_data - { - /// \brief encodes the transition relation of the TGBA. - /// - /// \c relation uses three kinds of variables: - /// \li "Now" variables, that encode the current state - /// \li "Next" variables, that encode the destination state - /// \li atomic propositions, which are things to verify before going on - /// to the next state - bdd relation; - - /// \brief encodes the acceptance conditions - /// - /// a U b, or F b, both imply that \c b should - /// be verified eventually. We encode this with generalized Büchi - /// acceptating conditions. An acceptance set, called - /// Acc[b], hold all the state that do not promise to - /// verify \c b eventually. (I.e., all the states that contain \c - /// b, or do not contain a U b, or F b.) - /// - /// The spot::succ_iter::current_acceptance_conditions() method - /// will return the \c Acc[x] variables of the acceptance sets - /// in which a transition is. Actually we never return \c Acc[x] - /// alone, but \c Acc[x] and all other acceptance variables negated. - /// - /// So if there is three acceptance set \c a, \c b, and \c c, and a - /// transition is in set \c a, we'll return - /// Acc[a]&!Acc[b]&!Acc[c]. If the transition is in both \c - /// a and \c b, we'll return (Acc[a]\&!Acc[b]\&!Acc[c]) \c | \c - /// (!Acc[a]\&Acc[b]\&!Acc[c]). - /// - /// Acceptance conditions are attributed to transitions and are - /// only concerned by atomic propositions (which label the - /// transitions) and Next variables (the destination). Typically, - /// a transition should bear the variable \c Acc[b] if it doesn't - /// check for `b' and have a destination of the form a U b, - /// or F b. - /// - /// To summarize, \c acceptance_conditions contains three kinds of - /// variables: - /// \li "Next" variables, that encode the destination state, - /// \li atomic propositions, which are things to verify before going on - /// to the next state, - /// \li "Acc" variables. - bdd acceptance_conditions; - - /// The value of \c bdd_support(acceptance_conditions) - bdd acceptance_conditions_support; - - /// \brief The set of all acceptance conditions used by the 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. - bdd all_acceptance_conditions; - - /// The conjunction of all Now variables, in their positive form. - bdd now_set; - /// The conjunction of all Next variables, in their positive form. - bdd next_set; - /// The conjunction of all Now and Next variables, in their positive form. - bdd nownext_set; - /// \brief The (positive) conjunction of all variables which are - /// not Now variables. - bdd notnow_set; - /// \brief The (positive) conjunction of all variables which are - /// not Next variables. - bdd notnext_set; - /// \brief The (positive) conjunction of all variables which are - /// atomic propositions. - bdd var_set; - /// \brief The (positive) conjunction of all variables which are - /// not atomic propositions. - bdd notvar_set; - /// \brief The (positive) conjunction of all Next variables - /// and atomic propositions. - bdd varandnext_set; - /// \brief The (positive) conjunction of all variables which are - /// acceptance conditions. - bdd acc_set; - /// \brief The (positive) conjunction of all variables which are not - /// acceptance conditions. - bdd notacc_set; - /// \brief The negative conjunction of all variables which are acceptance - /// conditions. - bdd negacc_set; - - /// The dictionary used by the automata. - bdd_dict* dict; - - /// \brief Default constructor. - /// - /// Initially all variable set are empty and the \c relation is true. - tgba_bdd_core_data(bdd_dict* dict); - - /// Copy constructor. - tgba_bdd_core_data(const tgba_bdd_core_data& copy); - - /// \brief Merge two tgba_bdd_core_data. - /// - /// This is used when building a product of two automata. - tgba_bdd_core_data(const tgba_bdd_core_data& left, - const tgba_bdd_core_data& right); - - tgba_bdd_core_data& operator=(const tgba_bdd_core_data& copy); - - /// \brief Update the variable sets to take a new pair of variables into - /// account. - void declare_now_next(bdd now, bdd next); - /// \brief Update the variable sets to take a new automic proposition into - /// account. - void declare_atomic_prop(bdd var); - /// \brief Update the variable sets to take a new acceptance condition - /// into account. - void declare_acceptance_condition(bdd prom); - - /// \brief Delete SCCs (Strongly Connected Components) from the - /// relation which cannot be accepting. - void delete_unaccepting_scc(bdd init); - - private: - bdd infinitely_often(bdd s, bdd acc, bdd er); - }; -} - -#endif // SPOT_TGBA_TGBABDDCOREDATA_HH diff --git a/src/tgba/tgbabddfactory.hh b/src/tgba/tgbabddfactory.hh deleted file mode 100644 index 5799d9c25..000000000 --- a/src/tgba/tgbabddfactory.hh +++ /dev/null @@ -1,43 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// Copyright (C) 2003, 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_TGBA_TGBABDDFACTORY_HH -# define SPOT_TGBA_TGBABDDFACTORY_HH - -#include "tgbabddcoredata.hh" - -namespace spot -{ - /// \brief Abstract class for spot::tgba_bdd_concrete factories. - /// - /// A spot::tgba_bdd_concrete can be constructed from anything that - /// supplies core data and their associated dictionary. - class SPOT_API tgba_bdd_factory - { - public: - virtual ~tgba_bdd_factory() {} - /// Get the core data for the new automata. - virtual const tgba_bdd_core_data& get_core_data() const = 0; - }; -} - -#endif // SPOT_TGBA_TGBABDDFACTORY_HH diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh index e21071c4a..d5ed9fb0e 100644 --- a/src/tgba/tgbaexplicit.hh +++ b/src/tgba/tgbaexplicit.hh @@ -172,7 +172,11 @@ namespace spot /// States labeled by a formula /// \ingroup tgba_representation class SPOT_API state_explicit_formula: +#ifndef SWIG public state_explicit +#else + public state +#endif { public: state_explicit_formula(): diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 3673b006c..7aa6f6da0 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -48,7 +48,6 @@ tgbaalgos_HEADERS = \ lbtt.hh \ ltl2taa.hh \ ltl2tgba_fm.hh \ - ltl2tgba_lacim.hh \ magic.hh \ minimize.hh \ neverclaim.hh \ @@ -96,7 +95,6 @@ libtgbaalgos_la_SOURCES = \ lbtt.cc \ ltl2taa.cc \ ltl2tgba_fm.cc \ - ltl2tgba_lacim.cc \ magic.cc \ minimize.cc \ ndfs_result.hxx \ diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc deleted file mode 100644 index 356feddfa..000000000 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ /dev/null @@ -1,307 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2014 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 . - -#include "ltlast/visitor.hh" -#include "ltlast/allnodes.hh" -#include "ltlvisit/lunabbrev.hh" -#include "ltlvisit/nenoform.hh" -#include "tgba/tgbabddconcretefactory.hh" -#include - -#include "ltl2tgba_lacim.hh" - -namespace spot -{ - namespace - { - using namespace ltl; - - /// \brief Recursively translate a formula into a BDD. - /// - /// The algorithm used here is adapted from Jean-Michel Couvreur's - /// Probataf tool. - class ltl_trad_visitor: public visitor - { - public: - ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) - : fact_(fact), root_(root) - { - } - - virtual - ~ltl_trad_visitor() - { - } - - bdd - result() - { - return res_; - } - - void - visit(const atomic_prop* node) - { - res_ = bdd_ithvar(fact_.create_atomic_prop(node)); - } - - void - visit(const constant* node) - { - switch (node->val()) - { - case constant::True: - res_ = bddtrue; - return; - case constant::False: - res_ = bddfalse; - return; - case constant::EmptyWord: - SPOT_UNIMPLEMENTED(); - } - SPOT_UNREACHABLE(); - } - - void - visit(const unop* node) - { - switch (node->op()) - { - case unop::F: - { - /* - Fx <=> x | XFx - In other words: - now <=> x | next - */ - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - bdd x = recurse(node->child()); - fact_.constrain_relation(bdd_apply(now, x | next, bddop_biimp)); - /* - `x | next', doesn't actually encode the fact that x - should be fulfilled eventually. We ensure this by - creating a new generalized Büchi acceptance set, Acc[x], - and leave out of this set any transition going off NOW - without checking X. Such acceptance conditions are - checked for during the emptiness check. - */ - fact_.declare_acceptance_condition(x | !now, node->child()); - res_ = now; - return; - } - case unop::G: - { - bdd child = recurse(node->child()); - // If G occurs at the top of the formula we don't - // need Now/Next variables. We just constrain - // the relation so that the child always happens. - // This saves 2 BDD variables. - if (root_) - { - fact_.constrain_relation(child); - res_ = child; - return; - } - // Gx <=> x && XGx - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, child & next, - bddop_biimp)); - res_ = now; - return; - } - case unop::Not: - { - res_ = bdd_not(recurse(node->child())); - return; - } - case unop::X: - { - int v = fact_.create_state(node->child()); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, recurse(node->child()), - bddop_biimp)); - res_ = next; - return; - } - case unop::Finish: - case unop::Closure: - case unop::NegClosure: - case unop::NegClosureMarked: - SPOT_UNIMPLEMENTED(); - } - SPOT_UNREACHABLE(); - } - - void - visit(const bunop*) - { - SPOT_UNIMPLEMENTED(); - } - - void - visit(const binop* node) - { - bdd f1 = recurse(node->first()); - bdd f2 = recurse(node->second()); - - binop::type op = node->op(); - switch (op) - { - case binop::Xor: - res_ = bdd_apply(f1, f2, bddop_xor); - return; - case binop::Implies: - res_ = bdd_apply(f1, f2, bddop_imp); - return; - case binop::Equiv: - res_ = bdd_apply(f1, f2, bddop_biimp); - return; - case binop::U: - case binop::W: - { - // f1 U f2 <=> f2 | (f1 & X(f1 U f2)) - // In other words: - // now <=> f2 | (f1 & next) - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, f2 | (f1 & next), - bddop_biimp)); - if (op == binop::U) - { - // The rightmost conjunction, f1 & next, doesn't - // actually encode the fact that f2 should be - // fulfilled eventually. We declare an acceptance - // condition for this purpose (see the comment in - // the unop::F case). - fact_.declare_acceptance_condition(f2 | !now, node->second()); - } - res_ = now; - return; - } - case binop::R: - case binop::M: - { - // f1 R f2 <=> f2 & (f1 | X(f1 R f2)) - // In other words: - // now <=> f2 & (f1 | next) - int v = fact_.create_state(node); - bdd now = bdd_ithvar(v); - bdd next = bdd_ithvar(v + 1); - fact_.constrain_relation(bdd_apply(now, f2 & (f1 | next), - bddop_biimp)); - if (op == binop::M) - { - // f2 & next, doesn't actually encode the fact that - // f1 should be fulfilled eventually. We declare an - // acceptance condition for this purpose (see the - // comment in the unop::F case). - fact_.declare_acceptance_condition(f1 | !now, node->second()); - } - res_ = now; - return; - } - case binop::UConcat: - case binop::EConcat: - case binop::EConcatMarked: - SPOT_UNIMPLEMENTED(); - } - SPOT_UNREACHABLE(); - } - - void - visit(const multop* node) - { - int op = -1; - bool root = false; - switch (node->op()) - { - case multop::And: - op = bddop_and; - res_ = bddtrue; - // When the root formula is a conjunction it's ok to - // consider all children as root formulae. This allows the - // root-G trick to save many more variable. (See the - // translation of G.) - root = root_; - break; - case multop::Or: - op = bddop_or; - res_ = bddfalse; - break; - case multop::Concat: - case multop::Fusion: - case multop::AndNLM: - case multop::AndRat: - case multop::OrRat: - SPOT_UNIMPLEMENTED(); - } - assert(op != -1); - unsigned s = node->size(); - for (unsigned n = 0; n < s; ++n) - { - res_ = bdd_apply(res_, recurse(node->nth(n), root), op); - } - } - - bdd - recurse(const formula* f, bool root = false) - { - ltl_trad_visitor v(fact_, root); - f->accept(v); - return v.result(); - } - - private: - bdd res_; - tgba_bdd_concrete_factory& fact_; - bool root_; - }; - } // anonymous - - tgba_bdd_concrete* - ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict) - { - // Normalize the formula. We want all the negations on - // the atomic propositions. We also suppress logic - // abbreviations such as <=>, =>, or XOR, since they - // would involve negations at the BDD level. - const ltl::formula* f1 = ltl::unabbreviate_logic(f); - const ltl::formula* f2 = ltl::negative_normal_form(f1); - f1->destroy(); - - // Traverse the formula and draft the automaton in a factory. - tgba_bdd_concrete_factory fact(dict); - ltl_trad_visitor v(fact, true); - f2->accept(v); - f2->destroy(); - fact.finish(); - - // Finally setup the resulting automaton. - return new tgba_bdd_concrete(fact, v.result()); - } -} diff --git a/src/tgbaalgos/ltl2tgba_lacim.hh b/src/tgbaalgos/ltl2tgba_lacim.hh deleted file mode 100644 index d3316cbf5..000000000 --- a/src/tgbaalgos/ltl2tgba_lacim.hh +++ /dev/null @@ -1,57 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). -// 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_TGBAALGOS_LTL2TGBA_LACIM_HH -# define SPOT_TGBAALGOS_LTL2TGBA_LACIM_HH - -#include "ltlast/formula.hh" -#include "tgba/tgbabddconcrete.hh" - -namespace spot -{ - /// \ingroup tgba_ltl - /// \brief Build a spot::tgba_bdd_concrete from an LTL formula. - /// - /// This is based on the following paper. - /** \verbatim - @InProceedings{ couvreur.00.lacim, - author = {Jean-Michel Couvreur}, - title = {Un point de vue symbolique sur la logique temporelle - lin{\'e}aire}, - booktitle = {Actes du Colloque LaCIM 2000}, - month = {August}, - year = {2000}, - pages = {131--140}, - volume = {27}, - series = {Publications du LaCIM}, - publisher = {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al}, - editor = {Pierre Leroux} - } - \endverbatim */ - /// \param f The formula to translate into an automaton. - /// \param dict The spot::bdd_dict the constructed automata should use. - /// \return A spot::tgba_bdd_concrete that recognizes the language of \a f. - SPOT_API tgba_bdd_concrete* - ltl_to_tgba_lacim(const ltl::formula* f, bdd_dict* dict); -} - -#endif // SPOT_TGBAALGOS_LTL2TGBA_LACIM_HH diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index 988c58820..ceb195e8b 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -31,7 +31,6 @@ noinst_PROGRAMS = ltl2tgba randtgba check_SCRIPTS = defs # Keep this sorted alphabetically. check_PROGRAMS = \ - bddprod \ bitvect \ complement \ explicit \ @@ -43,7 +42,6 @@ check_PROGRAMS = \ intvcmp2 \ ltlprod \ maskacc \ - mixprod \ powerset \ readsat \ taatgba \ @@ -51,8 +49,6 @@ check_PROGRAMS = \ tripprod # Keep this sorted alphabetically. -bddprod_SOURCES = ltlprod.cc -bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT bitvect_SOURCES = bitvect.cc complement_SOURCES = complementation.cc explicit_SOURCES = explicit.cc @@ -66,7 +62,6 @@ intvcmp2_SOURCES = intvcmp2.cc ltl2tgba_SOURCES = ltl2tgba.cc ltlprod_SOURCES = ltlprod.cc maskacc_SOURCES = maskacc.cc -mixprod_SOURCES = mixprod.cc powerset_SOURCES = powerset.cc randtgba_SOURCES = randtgba.cc readsat_SOURCES = readsat.cc @@ -100,13 +95,11 @@ TESTS = \ ltl2ta.test \ ltl2ta2.test \ ltlprod.test \ - bddprod.test \ explprod.test \ explpro2.test \ explpro3.test \ explpro4.test \ tripprod.test \ - mixprod.test \ dupexp.test \ degendet.test \ degenid.test \ diff --git a/src/tgbatest/bddprod.test b/src/tgbatest/bddprod.test deleted file mode 100755 index c01a7da74..000000000 --- a/src/tgbatest/bddprod.test +++ /dev/null @@ -1,38 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 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 - -# We don't check the output, but just running these might be enough to -# trigger assertions. - -run 0 ../bddprod a b -run 0 ../bddprod a a -run 0 ../bddprod 'a U b' 'X f' -run 0 ../bddprod 'X a' 'X a' -run 0 ../bddprod 'X a' 'a U b' -run 0 ../bddprod 'a & b & c' 'b & d & c' -run 0 ../bddprod 'a | b | (c U (d & (g U (h ^ i))))' 'h ^ i' -run 0 ../bddprod 'Xa & (b U !a) & (b U !a)' '(b U !a) & f' diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test index 745add0a7..d14655695 100755 --- a/src/tgbatest/cycles.test +++ b/src/tgbatest/cycles.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -82,7 +82,3 @@ test `wc -l < out` -eq 10 run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out test `grep 'is weak' out | wc -l` -eq 4 test `grep 'is not weak' out | wc -l` -eq 1 - -run 0 ../ltl2tgba -l -KW 'F(Fa R (Gb & !a))' > out -test `grep 'is weak' out | wc -l` -eq 7 -test `grep 'is not weak' out | wc -l` -eq 1 diff --git a/src/tgbatest/dupexp.test b/src/tgbatest/dupexp.test index c4c9321b8..f2a4a9f87 100755 --- a/src/tgbatest/dupexp.test +++ b/src/tgbatest/dupexp.test @@ -1,5 +1,5 @@ #!/bin/sh -# Copyright (C) 2009 Laboratoire de Recherche et Développement +# Copyright (C) 2009, 2014 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 @@ -30,10 +30,6 @@ dorun() run 0 ../ltl2tgba -f -s "$1" >output1 run 0 ../ltl2tgba -f -S "$1" >output2 test `wc -l output1 - run 0 ../ltl2tgba -l -S "$1" >output2 - test `wc -l (F x))' 3 -expect_no 'Xa && (!a U b) && !b && X!b' 4 -expect_no '(a U !b) && Gb' 3 +expect_no 'Xa && (!a U b) && !b && X!b' 2 +expect_no '(a U !b) && Gb' 2 diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 85bf6f755..e1ddcd8ac 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -30,7 +30,6 @@ #include "ltlvisit/apcollect.hh" #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2taa.hh" #include "tgba/bddprint.hh" @@ -142,8 +141,6 @@ syntax(char* prog) << "Translation algorithm:" << std::endl << " -f use Couvreur's FM algorithm for LTL" << " (default)" << std::endl - << " -l use Couvreur's LaCIM algorithm for LTL " - << std::endl << " -taa use Tauriainen's TAA-based algorithm for LTL" << std::endl << " -u use Compositional translation" @@ -165,19 +162,6 @@ syntax(char* prog) << "(implies -f)" << std::endl << std::endl - << "Options for Couvreur's LaCIM algorithm (-l):" - << std::endl - << " -a display the acceptance_conditions BDD, not the " - << "reachability graph" - << std::endl - << " -A same as -a, but as a set" << std::endl - << " -r display the relation BDD, not the reachability graph" - << std::endl - << " -R same as -r, but as a set" << std::endl - << " -R3b symbolically prune unaccepting SCC from BDD relation" - << std::endl - << std::endl - << "Options for Tauriainen's TAA-based algorithm (-taa):" << std::endl << " -c enable language containment checks (implies -taa)" @@ -351,7 +335,7 @@ main(int argc, char** argv) bool utf8_opt = false; enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen; enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled; - enum { TransFM, TransLaCIM, TransTAA, TransCompo } translation = TransFM; + enum { TransFM, TransTAA, TransCompo } translation = TransFM; bool fm_red = false; bool fm_exprop_opt = false; bool fm_symb_merge_opt = true; @@ -377,7 +361,6 @@ main(int argc, char** argv) false, false, false); bool simpcache_stats = false; bool scc_filter_all = false; - bool symbolic_scc_pruning = false; bool display_reduced_form = false; bool post_branching = false; bool fair_loop_approx = false; @@ -443,14 +426,7 @@ main(int argc, char** argv) utf8_opt = true; spot::enable_utf8(); } - else if (!strcmp(argv[formula_index], "-a")) - { - output = 2; - } - else if (!strcmp(argv[formula_index], "-A")) - { - output = 4; - } + else if (!strcmp(argv[formula_index], "-b")) { output = 7; @@ -613,10 +589,6 @@ main(int argc, char** argv) { output = 16; } - else if (!strcmp(argv[formula_index], "-l")) - { - translation = TransLaCIM; - } else if (!strcmp(argv[formula_index], "-L")) { fair_loop_approx = true; @@ -668,10 +640,6 @@ main(int argc, char** argv) tm.stop("reading -P's argument"); system_aut = s; } - else if (!strcmp(argv[formula_index], "-r")) - { - output = 1; - } else if (!strcmp(argv[formula_index], "-r1")) { simpltl = true; @@ -714,10 +682,6 @@ main(int argc, char** argv) redopt.containment_checks = true; redopt.containment_checks_stronger = true; } - else if (!strcmp(argv[formula_index], "-R")) - { - output = 3; - } else if (!strcmp(argv[formula_index], "-R1q") || !strcmp(argv[formula_index], "-R1t") || !strcmp(argv[formula_index], "-R2q") @@ -740,10 +704,6 @@ main(int argc, char** argv) scc_filter = true; scc_filter_all = true; } - else if (!strcmp(argv[formula_index], "-R3b")) - { - symbolic_scc_pruning = true; - } else if (!strcmp(argv[formula_index], "-rd")) { display_reduced_form = true; @@ -1021,7 +981,6 @@ main(int argc, char** argv) switch (translation) { case TransFM: - case TransLaCIM: case TransTAA: case TransCompo: { @@ -1037,7 +996,6 @@ main(int argc, char** argv) if (f || from_file) { - spot::tgba_bdd_concrete* concrete = 0; const spot::tgba* to_free = 0; const spot::tgba* to_free2 = 0; spot::tgba* a = 0; @@ -1212,9 +1170,6 @@ main(int argc, char** argv) case TransTAA: a = spot::ltl_to_taa(f, dict, containment); break; - case TransLaCIM: - a = concrete = spot::ltl_to_tgba_lacim(f, dict); - break; } tm.stop("translating formula"); to_free = a; @@ -1240,35 +1195,7 @@ main(int argc, char** argv) } if (opt_monitor && !scc_filter) - { - if (dynamic_cast(a)) - symbolic_scc_pruning = true; - else - scc_filter = true; - } - - if (symbolic_scc_pruning) - { - const spot::tgba_bdd_concrete* bc = - dynamic_cast(a); - if (!bc) - { - std::cerr << ("Error: Automaton is not symbolic: cannot " - "prune SCCs symbolically.\n" - " Try -R3 instead of -R3b, or use " - "another translation.") - << std::endl; - exit(2); - } - else - { - tm.start("reducing A_f w/ symbolic SCC pruning"); - if (bc) - const_cast(bc) - ->delete_unaccepting_scc(); - tm.stop("reducing A_f w/ symbolic SCC pruning"); - } - } + scc_filter = true; // Remove dead SCCs and useless acceptance conditions before // degeneralization. @@ -1701,28 +1628,6 @@ main(int argc, char** argv) case 0: spot::dotty_reachable(std::cout, a, assume_sba); break; - case 1: - if (concrete) - spot::bdd_print_dot(std::cout, concrete->get_dict(), - concrete->get_core_data().relation); - break; - case 2: - if (concrete) - spot::bdd_print_dot(std::cout, concrete->get_dict(), - concrete-> - get_core_data().acceptance_conditions); - break; - case 3: - if (concrete) - spot::bdd_print_set(std::cout, concrete->get_dict(), - concrete->get_core_data().relation); - break; - case 4: - if (concrete) - spot::bdd_print_set(std::cout, concrete->get_dict(), - concrete-> - get_core_data().acceptance_conditions); - break; case 5: a->get_dict()->dump(std::cout); break; diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test index f72716bd5..880bf6f13 100755 --- a/src/tgbatest/ltl2tgba.test +++ b/src/tgbatest/ltl2tgba.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et +# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 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 @@ -41,9 +41,9 @@ check_psl () check_ltl () { check_psl "$@" - # Make cross products with LaCIM - run 0 ../ltl2tgba -l -R3b -b "$1" > out.tgba - run 0 ../ltl2tgba -l -R3b -Pout.tgba -E "!($1)" + # Make cross products with TAA + run 0 ../ltl2tgba -taa -R3 -b "$1" > out.tgba + run 0 ../ltl2tgba -taa -R3 -Pout.tgba -E "!($1)" } check_ltl a diff --git a/src/tgbatest/ltlcross.test b/src/tgbatest/ltlcross.test index 5b2a609f9..7af064457 100755 --- a/src/tgbatest/ltlcross.test +++ b/src/tgbatest/ltlcross.test @@ -25,15 +25,12 @@ ltl2tgba=../ltl2tgba ../../bin/randltl -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 | ../../bin/ltlcross --products=2 \ - "$ltl2tgba -t -l %f > %T" \ - "$ltl2tgba -t -l -R3b -r4 %f > %T" \ "$ltl2tgba -t -f %f > %T" \ "$ltl2tgba -t -f -y %f > %T" \ "$ltl2tgba -t -f -r4 %f > %T" \ "$ltl2tgba -t -f -R3 %f > %T" \ "$ltl2tgba -t -f -R3 -Rm %f > %T" \ "$ltl2tgba -t -f -R3 -RM %f > %T" \ - "$ltl2tgba -t -l -R3b -Rm %f > %T" \ "$ltl2tgba -t -f -D %f > %T" \ "$ltl2tgba -t -f -D %f > %T" \ "$ltl2tgba -t -f -r4 -R3 -RDS %f > %T" \ diff --git a/src/tgbatest/ltlprod.cc b/src/tgbatest/ltlprod.cc index 690a045e9..0b6331008 100644 --- a/src/tgbatest/ltlprod.cc +++ b/src/tgbatest/ltlprod.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et +// Copyright (C) 2008, 2009, 2012, 2014 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), @@ -25,9 +25,8 @@ #include #include "ltlast/allnodes.hh" #include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgba/tgbaproduct.hh" -#include "tgba/tgbabddconcreteproduct.hh" +#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/dotty.hh" void @@ -61,16 +60,11 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); { - spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); - spot::tgba_bdd_concrete* a2 = spot::ltl_to_tgba_lacim(f2, dict); + auto a1 = spot::ltl_to_tgba_fm(f1, dict); + auto a2 = spot::ltl_to_tgba_fm(f2, dict); f1->destroy(); f2->destroy(); - -#ifdef BDD_CONCRETE_PRODUCT - spot::tgba_bdd_concrete* p = spot::product(a1, a2); -#else - spot::tgba_product* p = new spot::tgba_product(a1, a2); -#endif + auto p = new spot::tgba_product(a1, a2); spot::dotty_reachable(std::cout, p); delete p; delete a1; diff --git a/src/tgbatest/mixprod.cc b/src/tgbatest/mixprod.cc deleted file mode 100644 index bf4635da1..000000000 --- a/src/tgbatest/mixprod.cc +++ /dev/null @@ -1,78 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2008, 2009, 2012, 2014 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 . - -#include -#include -#include -#include "ltlast/allnodes.hh" -#include "ltlparse/public.hh" -#include "tgbaalgos/ltl2tgba_lacim.hh" -#include "tgba/tgbaproduct.hh" -#include "tgba/tgbabddconcreteproduct.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/save.hh" - -void -syntax(char* prog) -{ - std::cerr << prog << " formula file" << std::endl; - exit(2); -} - -int -main(int argc, char** argv) -{ - int exit_code = 0; - - if (argc != 3) - syntax(argv[0]); - - spot::bdd_dict* dict = new spot::bdd_dict(); - - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - - spot::ltl::parse_error_list pel1; - const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); - if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) - return 2; - - spot::tgba_parse_error_list pel2; - spot::tgba* a2 = spot::tgba_parse(argv[2], pel2, dict, env); - if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel2)) - return 2; - - { - spot::tgba_bdd_concrete* a1 = spot::ltl_to_tgba_lacim(f1, dict); - f1->destroy(); - spot::tgba_product p(a1, a2); - spot::tgba_save_reachable(std::cout, &p); - delete a1; - } - - assert(spot::ltl::unop::instance_count() == 0); - assert(spot::ltl::binop::instance_count() == 0); - assert(spot::ltl::multop::instance_count() == 0); - delete a2; - assert(spot::ltl::atomic_prop::instance_count() == 0); - delete dict; - return exit_code; -} diff --git a/src/tgbatest/mixprod.test b/src/tgbatest/mixprod.test deleted file mode 100755 index 23e1edc1b..000000000 --- a/src/tgbatest/mixprod.test +++ /dev/null @@ -1,46 +0,0 @@ -#!/bin/sh -# Copyright (C) 2009 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 - -# We don't check the output, but just running this might be enough to -# trigger assertions or I/O errors. - -cat >input1 <stdout -cat stdout - -# Make sure we can read the produced output - -run 0 ../mixprod 'G!a' stdout - -rm input1 stdout diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index cb0ea9b85..27b80da4e 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -32,30 +32,6 @@ need_lbtt set -e cat > config </dev/null + run 0 ../ltl2tgba -taa -DS -Rm "!($f)" >/dev/null i=`expr $i + 1` fi diff --git a/src/tgbatest/wdba2.test b/src/tgbatest/wdba2.test index 969c8cfe2..01e3dca41 100755 --- a/src/tgbatest/wdba2.test +++ b/src/tgbatest/wdba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012 Laboratoire de Recherche et Développement +# Copyright (C) 2012, 2014 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -37,11 +37,3 @@ run 0 ../ltl2tgba -Rm -kt 'Fa | XGd' > out2 cmp out expected cmp out2 expected - -# This non-obligation formula used to be minimized by mistake when -# translated with lacim. -x=`../ltl2tgba -l -Rm 'F(Fa R (Gb & !a))' | - grep -v -- '->' | - sed -n 's/.*label="\(..*\)".*/\1/p' | - tr -d '0-9\n'` -test -n "$x" diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 211f768e8..0ba0f5a62 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -565,7 +565,6 @@ an identifier: aUb is an atomic proposition, unlike
  • Translator Algorithm:
  • Couvreur/FM
    • -
  • Couvreur/LaCIM
  • Tauriainen/TAA
  • LTL3BA
  • Comp.Susp.
    • @@ -591,12 +590,6 @@ an identifier: aUb is an atomic proposition, unlike fair-loop approximations
    -
    -
    -