Commit 116fe865 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 26b93282
# 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
......@@ -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.
......@@ -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"
#!/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'"
......@@ -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 \
......
// -*- 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 <http://www.gnu.org/licenses/>.
#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
// 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 <http://www.gnu.org/licenses/>.
#include "statebdd.hh"
#include <bdd.h>
#include <cassert>
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<const state_bdd*>(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);
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBA_STATEBDD_HH
# define SPOT_TGBA_STATEBDD_HH
#include <bdd.h>
#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
// -*- 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 <http://www.gnu.org/licenses/>.
#include "succiterconcrete.hh"
#include <cassert>
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_;
}
}
// -*- 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 <http://www.gnu.org/licenses/>.
#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
// -*- 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 <http://www.gnu.org/licenses/>.
#include "tgbabddconcrete.hh"
#include "bddprint.hh"
#include <cassert>
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_;
}