Commit 121d5824 authored by Denis Poitrenaud's avatar Denis Poitrenaud
Browse files

* src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo.

* src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now
the original one.
* src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files
implementing most of all the optimisations of tau03.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public.
* src/tgbatest/tba_samples_from_spin.test: Test them.
parent 32117733
2004-11-17 Poitrenaud Denis <denis@src.lip6.fr>
* src/tgbaalgos/se05.hh, src/tgbaalgos/tau03.hh: Typo.
* src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now
the original one.
* src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files
implementing most of all the optimisations of tau03.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public.
* src/tgbatest/tba_samples_from_spin.test: Test them.
2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh, * src/tgba/tgba.hh, src/tgbaalgos/ltl2tgba_fm.hh,
......
...@@ -46,6 +46,7 @@ tgbaalgos_HEADERS = \ ...@@ -46,6 +46,7 @@ tgbaalgos_HEADERS = \
se05.hh \ se05.hh \
stats.hh \ stats.hh \
tau03.hh \ tau03.hh \
tau03opt.hh \
reductgba_sim.hh reductgba_sim.hh
noinst_LTLIBRARIES = libtgbaalgos.la noinst_LTLIBRARIES = libtgbaalgos.la
...@@ -69,6 +70,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -69,6 +70,7 @@ libtgbaalgos_la_SOURCES = \
se05.cc \ se05.cc \
stats.cc \ stats.cc \
tau03.cc \ tau03.cc \
tau03opt.cc \
reductgba_sim.cc \ reductgba_sim.cc \
reductgba_sim_del.cc reductgba_sim_del.cc
......
...@@ -145,4 +145,4 @@ namespace spot ...@@ -145,4 +145,4 @@ namespace spot
/// @} /// @}
} }
#endif // SPOT_TGBAALGOS_MAGIC_HH #endif // SPOT_TGBAALGOS_SE05_HH
...@@ -19,6 +19,10 @@ ...@@ -19,6 +19,10 @@
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA. // 02111-1307, USA.
/// FIXME: Add
/// - the computation of a counter example if detected.
/// - a bit-state hashing version.
//#define TRACE //#define TRACE
#ifdef TRACE #ifdef TRACE
...@@ -39,7 +43,7 @@ namespace spot ...@@ -39,7 +43,7 @@ namespace spot
{ {
namespace namespace
{ {
enum color {WHITE, CYAN, BLUE}; enum color {WHITE, BLUE};
/// \brief Emptiness checker on spot::tgba automata having at most one /// \brief Emptiness checker on spot::tgba automata having at most one
/// accepting condition (i.e. a TBA). /// accepting condition (i.e. a TBA).
...@@ -77,17 +81,16 @@ namespace spot ...@@ -77,17 +81,16 @@ namespace spot
/// accepting path. /// accepting path.
virtual emptiness_check_result* check() virtual emptiness_check_result* check()
{ {
if (!st_red.empty()) if (!st_blue.empty())
{ {
assert(!st_blue.empty());
return 0; return 0;
} }
assert(st_blue.empty()); assert(st_red.empty());
nbn = nbt = 0; nbn = nbt = 0;
sts = mdp = 0; sts = mdp = 0;
const state* s0 = a->get_init_state(); const state* s0 = a->get_init_state();
++nbn; ++nbn;
h.add_new_state(s0, CYAN); h.add_new_state(s0, BLUE);
push(st_blue, s0, bddfalse, bddfalse); push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue()) if (dfs_blue())
return new emptiness_check_result; return new emptiness_check_result;
...@@ -146,9 +149,6 @@ namespace spot ...@@ -146,9 +149,6 @@ namespace spot
/// by the last dfs visiting it. /// by the last dfs visiting it.
heap h; heap h;
/// State targeted by the red dfs.
const state* target;
/// The automata to check. /// The automata to check.
const tgba* a; const tgba* a;
...@@ -175,24 +175,23 @@ namespace spot ...@@ -175,24 +175,23 @@ namespace spot
<< a->format_state(s_prime) << std::endl; << a->format_state(s_prime) << std::endl;
#endif #endif
f.it->next(); f.it->next();
typename heap::color_ref c = h.get_color_ref(s_prime); typename heap::color_ref c_prime = h.get_color_ref(s_prime);
if (c.is_white()) if (c_prime.is_white())
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
{ {
++nbn; ++nbn;
#ifdef TRACE #ifdef TRACE
std::cout << " It is white, go down" << std::endl; std::cout << " It is white, go down" << std::endl;
#endif #endif
h.add_new_state(s_prime, CYAN); h.add_new_state(s_prime, BLUE);
push(st_blue, s_prime, label, acc); push(st_blue, s_prime, label, acc);
} }
else // Backtrack the edge (f.s, <label, acc>, s_prime) else // Backtrack the edge (f.s, <label, acc>, s_prime)
{ {
#ifdef TRACE #ifdef TRACE
std::cout << " It is cyan or blue, pop it" std::cout << " It is blue, pop it" << std::endl;
<< std::endl;
#endif #endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
else else
...@@ -217,44 +216,35 @@ namespace spot ...@@ -217,44 +216,35 @@ namespace spot
assert(!c_prime.is_white()); assert(!c_prime.is_white());
bdd acu = acc | c.get_acc(); bdd acu = acc | c.get_acc();
#ifdef TRACE #ifdef TRACE
std::cout << "DFS_BLUE rescanning from: " std::cout << "DFS_BLUE rescanning the arc from "
<< a->format_state(f.s) << std::endl; << a->format_state(f.s) << " to "
std::cout << " tests "
<< a->format_state(s_prime) << std::endl; << a->format_state(s_prime) << std::endl;
std::cout << " if ";
bdd_print_acc(std::cout, a->get_dict(), acu);
std::cout << std::endl;
std::cout << " is not included in ";
bdd_print_acc(std::cout, a->get_dict(), c_prime.get_acc());
std::cout << std::endl;
#endif #endif
if ((c_prime.get_acc() & acu) != acu) if ((c_prime.get_acc() & acu) != acu)
{ {
#ifdef TRACE #ifdef TRACE
std::cout << " that is true, starts a red dfs with " std::cout << " ";
bdd_print_acc(std::cout, a->get_dict(), acu);
std::cout << " is not included in ";
bdd_print_acc(std::cout, a->get_dict(),
c_prime.get_acc());
std::cout << std::endl;
std::cout << " Start a red dfs from "
<< a->format_state(s_prime) << a->format_state(s_prime)
<< " propagating: "; << " propagating: ";
bdd_print_acc(std::cout, a->get_dict(), acu); bdd_print_acc(std::cout, a->get_dict(), acu);
std::cout << std::endl; std::cout << std::endl;
#endif #endif
target = f.s;
c_prime.cumulate_acc(acu); c_prime.cumulate_acc(acu);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (target->compare(s_prime) == 0 && dfs_red(acu);
c_prime.get_acc() == all_cond)
{
delete i;
return true;
}
if (dfs_red(acu) || c.get_acc() == all_cond)
{
delete i;
return true;
}
} }
} }
delete i; delete i;
c.set_color(BLUE); if (c.get_acc() == all_cond)
{
return true;
}
delete f.it; delete f.it;
--sts; --sts;
h.pop_notify(f.s); h.pop_notify(f.s);
...@@ -264,7 +254,7 @@ namespace spot ...@@ -264,7 +254,7 @@ namespace spot
return false; return false;
} }
bool dfs_red(const bdd& acu) void dfs_red(const bdd& acu)
{ {
assert(!st_red.empty()); assert(!st_red.empty());
...@@ -287,31 +277,33 @@ namespace spot ...@@ -287,31 +277,33 @@ namespace spot
#endif #endif
f.it->next(); f.it->next();
typename heap::color_ref c_prime = h.get_color_ref(s_prime); typename heap::color_ref c_prime = h.get_color_ref(s_prime);
if (!c_prime.is_white() && if (!c_prime.is_white())
(c_prime.get_acc() & acu) != acu)
{ {
if ((c_prime.get_acc() & acu) != acu)
{
#ifdef TRACE #ifdef TRACE
std::cout << " It is cyan or blue and propagation " std::cout << " It is blue and propagation "
<< "is nedded, go down" << "is needed, go down" << std::endl;
<< std::endl;
#endif #endif
c_prime.cumulate_acc(acu); c_prime.cumulate_acc(acu);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (target->compare(s_prime) == 0 && }
c_prime.get_acc() == all_cond) else
return true; {
#ifdef TRACE
std::cout << " It is blue and no propagation "
<< "is needed, pop it" << std::endl;
#endif
h.pop_notify(s_prime);
}
} }
else else
{ {
#ifdef TRACE #ifdef TRACE
std::cout << " It is white or no propagation is needed " std::cout << " It is white, pop it" << std::endl;
<< ", pop it"
<< std::endl;
#endif #endif
if (c_prime.is_white()) delete s_prime;
delete s_prime; }
h.pop_notify(s_prime);
}
} }
else // Backtrack else // Backtrack
{ {
...@@ -325,7 +317,6 @@ namespace spot ...@@ -325,7 +317,6 @@ namespace spot
st_red.pop_front(); st_red.pop_front();
} }
} }
return false;
} }
}; };
......
...@@ -45,7 +45,7 @@ namespace spot ...@@ -45,7 +45,7 @@ namespace spot
/// ///
/// procedure dfs_blue (s) /// procedure dfs_blue (s)
/// begin /// begin
/// s.color = cyan; /// s.color = blue;
/// s.acc = emptyset; /// s.acc = emptyset;
/// for all t in post(s) do /// for all t in post(s) do
/// if t.color == white then /// if t.color == white then
...@@ -54,28 +54,19 @@ namespace spot ...@@ -54,28 +54,19 @@ namespace spot
/// end for; /// end for;
/// for all t in post(s) do /// for all t in post(s) do
/// let (s, l, a, t) be the edge from s to t; /// let (s, l, a, t) be the edge from s to t;
/// if a U s.acc not included in t.acc then /// if s.acc U a not included in t.acc then
/// target = s;
/// call dfs_red(t, a U s.acc); /// call dfs_red(t, a U s.acc);
/// end if; /// end if;
/// end for; /// end for;
/// if s.acc == all_acc then /// if s.acc == all_acc then
/// report a cycle; /// report a cycle;
/// end if; /// end if;
/// s.color = blue;
/// end; /// end;
/// ///
/// procedure dfs_red(s, A) /// procedure dfs_red(s, A)
/// begin /// begin
/// s.acc = s.acc U A; /// s.acc = s.acc U A;
/// // The following test has been added to the origiginal algorithm to
/// // report a cycle as soon as possible (and to mimic the classic magic
/// // search.
/// if s == target and s.acc == all_acc then
/// report a cycle;
/// end if;
/// for all t in post(s) do /// for all t in post(s) do
/// let (s, l, a, t) be the edge from s to t;
/// if t.color != white and A not included in t.acc then /// if t.color != white and A not included in t.acc then
/// call dfs_red(t, A); /// call dfs_red(t, A);
/// end if; /// end if;
...@@ -107,4 +98,4 @@ namespace spot ...@@ -107,4 +98,4 @@ namespace spot
/// @} /// @}
} }
#endif // SPOT_TGBAALGOS_MAGIC_HH #endif // SPOT_TGBAALGOS_TAU03_HH
// 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 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
/// FIXME: Add
/// - the optimisation based on weights (a weight by accepting conditions),
/// - the computation of a counter example if detected.
/// - a bit-state hashing version.
//#define TRACE
#ifdef TRACE
#include <iostream>
#include "tgba/bddprint.hh"
#endif
#include <cassert>
#include <list>
#include <iterator>
#include "misc/hash.hh"
#include "tgba/tgba.hh"
#include "emptiness.hh"
#include "magic.hh"
#include "tau03opt.hh"
namespace spot
{
namespace
{
enum color {WHITE, CYAN, BLUE};
/// \brief Emptiness checker on spot::tgba automata having at most one
/// accepting condition (i.e. a TBA).
template <typename heap>
class tau03_opt_search : public emptiness_check
{
public:
/// \brief Initialize the search algorithm on the automaton \a a
tau03_opt_search(const tgba *a, size_t size)
: h(size), a(a), all_acc(a->all_acceptance_conditions())
{
assert(a->number_of_acceptance_conditions() > 0);
}
virtual ~tau03_opt_search()
{
// Release all iterators on the stacks.
while (!st_blue.empty())
{
h.pop_notify(st_blue.front().s);
delete st_blue.front().it;
st_blue.pop_front();
}
while (!st_red.empty())
{
h.pop_notify(st_red.front().s);
delete st_red.front().it;
st_red.pop_front();
}
}
/// \brief Perform a Magic Search.
///
/// \return non null pointer iff the algorithm has found an
/// accepting path.
virtual emptiness_check_result* check()
{
if (!st_red.empty())
{
assert(!st_blue.empty());
return 0;
}
assert(st_blue.empty());
nbn = nbt = 0;
sts = mdp = 0;
const state* s0 = a->get_init_state();
++nbn;
h.add_new_state(s0, CYAN);
push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue())
return new emptiness_check_result;
return 0;
}
virtual std::ostream& print_stats(std::ostream &os) const
{
os << nbn << " distinct nodes visited" << std::endl;
os << nbt << " transitions explored" << std::endl;
os << mdp << " nodes for the maximal stack depth" << std::endl;
return os;
}
private:
/// \brief counters for statistics (number of distinct nodes, of
/// transitions and maximal stacks size.
int nbn, nbt, mdp, sts;
struct stack_item
{
stack_item(const state* n, tgba_succ_iterator* i, bdd l, bdd a)
: s(n), it(i), label(l), acc(a) {};
/// The visited state.
const state* s;
/// Design the next successor of \a s which has to be visited.
tgba_succ_iterator* it;
/// The label of the transition traversed to reach \a s
/// (false for the first one).
bdd label;
/// The acceptance set of the transition traversed to reach \a s
/// (false for the first one).
bdd acc;
};
typedef std::list<stack_item> stack_type;
void push(stack_type& st, const state* s,
const bdd& label, const bdd& acc)
{
++sts;
if (sts>mdp)
mdp = sts;
tgba_succ_iterator* i = a->succ_iter(s);
i->first();
st.push_front(stack_item(s, i, label, acc));
}
/// \brief Stack of the blue dfs.
stack_type st_blue;
/// \brief Stack of the red dfs.
stack_type st_red;
/// \brief Map where each visited state is colored
/// by the last dfs visiting it.
heap h;
/// The automata to check.
const tgba* a;
/// The unique accepting condition of the automaton \a a.
bdd all_acc;
bool dfs_blue()
{
while (!st_blue.empty())
{
stack_item& f = st_blue.front();
#ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
#endif
if (!f.it->done())
{
++nbt;
const state *s_prime = f.it->current_state();
bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions();
#ifdef TRACE
std::cout << " Visit the successor: "
<< a->format_state(s_prime) << std::endl;
#endif
f.it->next();
typename heap::color_ref c_prime = h.get_color_ref(s_prime);
if (c_prime.is_white())
// Go down the edge (f.s, <label, acc>, s_prime)
{
++nbn;
#ifdef TRACE
std::cout << " It is white, go down" << std::endl;
#endif
h.add_new_state(s_prime, CYAN);
push(st_blue, s_prime, label, acc);
}
else
{
typename heap::color_ref c = h.get_color_ref(f.s);
assert(!c.is_white());
if (c_prime.get_color() == CYAN &&
(c.get_acc() | acc | c_prime.get_acc()) == all_acc)
{
#ifdef TRACE
std::cout << " It is cyan and acceptance condition "
<< "is reached, report cycle" << std::endl;
#endif
c_prime.cumulate_acc(c.get_acc() | acc);
push(st_red, s_prime, label, acc);
return true;
}
else // Backtrack the edge (f.s, <label, acc>, s_prime)
{
#ifdef TRACE
std::cout << " It is cyan or blue, pop it"
<< std::endl;
#endif
h.pop_notify(s_prime);
}
}
}
else
// Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{
#ifdef TRACE
std::cout << " All the successors have been visited"
<< ", rescan this successors"
<< std::endl;
#endif
typename heap::color_ref c = h.get_color_ref(f.s);
assert(!c.is_white());
tgba_succ_iterator* i = a->succ_iter(f.s);
for (i->first(); !i->done(); i->next())
{
++nbt;
const state *s_prime = i->current_state();
bdd label = i->current_condition();
bdd acc = i->current_acceptance_conditions();
typename heap::color_ref c_prime = h.get_color_ref(s_prime);