From 116fe8654f65350092197b84b6e9c5264c4a7e15 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 8 Jul 2014 16:22:43 +0200 Subject: [PATCH] Remove ltl2tgba_lacim and all supporting classes. This translator algorithm is seldom used in practice because we work with explicit automata everywhere, and this is only useful to build symbolic automata. Furthermore, the symbolic automata produced by this algorithm are larger (when looked at explicitly) than those produced by ltl2tgba_fm or other explicit translators. The nice side effect of this removal is that we can also remove a lot of supporting classes, that were relying a lot on BDDs. * src/tgba/public.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh, src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.cc, src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh, src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbatest/bddprod.test, src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test: Delete all these files. * bench/ltlcounter/Makefile.am, bench/ltlcounter/README, bench/ltlcounter/plot.gnu, bench/ltlcounter/run, src/tgba/Makefile.am, src/tgbaalgos/Makefile.am, src/tgbatest/Makefile.am, src/tgbatest/cycles.test, src/tgbatest/dupexp.test, src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcross.test, src/tgbatest/ltlprod.cc, src/tgbatest/spotlbtt.test, src/tgbatest/wdba.test, src/tgbatest/wdba2.test, src/tgba/tgbaexplicit.hh, wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in, wrap/python/spot.i, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test: Adjust. --- bench/ltlcounter/Makefile.am | 6 +- bench/ltlcounter/README | 2 +- bench/ltlcounter/plot.gnu | 8 +- bench/ltlcounter/run | 12 +- src/tgba/Makefile.am | 14 -- src/tgba/public.hh | 38 ---- src/tgba/statebdd.cc | 53 ----- src/tgba/statebdd.hh | 57 ------ src/tgba/succiterconcrete.cc | 193 ------------------ src/tgba/succiterconcrete.hh | 86 -------- src/tgba/tgbabddconcrete.cc | 160 --------------- src/tgba/tgbabddconcrete.hh | 97 --------- src/tgba/tgbabddconcretefactory.cc | 149 -------------- src/tgba/tgbabddconcretefactory.hh | 102 ---------- src/tgba/tgbabddconcreteproduct.cc | 78 -------- src/tgba/tgbabddconcreteproduct.hh | 36 ---- src/tgba/tgbabddcoredata.cc | 200 ------------------- src/tgba/tgbabddcoredata.hh | 159 --------------- src/tgba/tgbabddfactory.hh | 43 ---- src/tgba/tgbaexplicit.hh | 4 + src/tgbaalgos/Makefile.am | 2 - src/tgbaalgos/ltl2tgba_lacim.cc | 307 ----------------------------- src/tgbaalgos/ltl2tgba_lacim.hh | 57 ------ src/tgbatest/Makefile.am | 7 - src/tgbatest/bddprod.test | 38 ---- src/tgbatest/cycles.test | 6 +- src/tgbatest/dupexp.test | 6 +- src/tgbatest/emptchk.test | 46 ++--- src/tgbatest/ltl2tgba.cc | 101 +--------- src/tgbatest/ltl2tgba.test | 8 +- src/tgbatest/ltlcross.test | 3 - src/tgbatest/ltlprod.cc | 16 +- src/tgbatest/mixprod.cc | 78 -------- src/tgbatest/mixprod.test | 46 ----- src/tgbatest/spotlbtt.test | 41 ---- src/tgbatest/wdba.test | 4 +- src/tgbatest/wdba2.test | 10 +- wrap/python/ajax/ltl2tgba.html | 7 - wrap/python/ajax/spot.in | 9 +- wrap/python/spot.i | 24 ++- wrap/python/tests/interdep.py | 27 ++- wrap/python/tests/ltl2tgba.py | 42 +--- wrap/python/tests/ltl2tgba.test | 20 +- 43 files changed, 111 insertions(+), 2291 deletions(-) delete mode 100644 src/tgba/public.hh delete mode 100644 src/tgba/statebdd.cc delete mode 100644 src/tgba/statebdd.hh delete mode 100644 src/tgba/succiterconcrete.cc delete mode 100644 src/tgba/succiterconcrete.hh delete mode 100644 src/tgba/tgbabddconcrete.cc delete mode 100644 src/tgba/tgbabddconcrete.hh delete mode 100644 src/tgba/tgbabddconcretefactory.cc delete mode 100644 src/tgba/tgbabddconcretefactory.hh delete mode 100644 src/tgba/tgbabddconcreteproduct.cc delete mode 100644 src/tgba/tgbabddconcreteproduct.hh delete mode 100644 src/tgba/tgbabddcoredata.cc delete mode 100644 src/tgba/tgbabddcoredata.hh delete mode 100644 src/tgba/tgbabddfactory.hh delete mode 100644 src/tgbaalgos/ltl2tgba_lacim.cc delete mode 100644 src/tgbaalgos/ltl2tgba_lacim.hh delete mode 100755 src/tgbatest/bddprod.test delete mode 100644 src/tgbatest/mixprod.cc delete mode 100755 src/tgbatest/mixprod.test 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
    -
    -
    -