alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,

Browse source 
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/tau03opt.cc: Fix comments and debug traces

* src/tgbatest/randtgba.cc: Adjust names of algorithms.
This commit is contained in:
Denis Poitrenaud 2004-11-25 14:40:17 +00:00
parent 2143d6c4b6
commit 15329c5618
9 changed files with 252 additions and 364 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2004-11-25 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/tau03opt.cc: Fix comments and debug traces
* src/tgbatest/randtgba.cc: Adjust names of algorithms.
2004-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbatest/randtgba.cc: Add option -D. * src/tgbatest/randtgba.cc: Add option -D.

79
src/tgbaalgos/magic.cc
View file

@ -21,8 +21,11 @@
//#define TRACE //#define TRACE
#ifdef TRACE
#include <iostream> #include <iostream>
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif #endif
#include <cassert> #include <cassert>
@ -178,17 +181,12 @@ namespace spot
while (!st_blue.empty()) while (!st_blue.empty())
{ {
stack_item& f = st_blue.front(); stack_item& f = st_blue.front();
# ifdef TRACE trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_BLUE treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -197,9 +195,7 @@ namespace spot
typename heap::color_ref c = h.get_color_ref(s_prime); typename heap::color_ref c = h.get_color_ref(s_prime);
if (c.is_white()) if (c.is_white())
{ {
# ifdef TRACE trace << " It is white, go down" << std::endl;
std::cout << " It is white, go down" << std::endl;
# endif
inc_states(); inc_states();
h.add_new_state(s_prime, BLUE); h.add_new_state(s_prime, BLUE);
push(st_blue, s_prime, label, acc); push(st_blue, s_prime, label, acc);
@ -212,10 +208,8 @@ namespace spot
// the number of runs reported by successive // the number of runs reported by successive
// calls to the check method. Without this // calls to the check method. Without this
// functionnality, the test can be ommited. // functionnality, the test can be ommited.
# ifdef TRACE trace << " It is blue and the arc is "
std::cout << " It is blue and the arc is " << "accepting, start a red dfs" << std::endl;
<< "accepting, start a red dfs" << std::endl;
# endif
target = f.s; target = f.s;
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
@ -224,9 +218,7 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " It is blue or red, pop it" << std::endl;
std::cout << " It is blue or red, pop it" << std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
@ -235,10 +227,7 @@ namespace spot
// Backtrack the edge // Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s) // (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{ {
# ifdef TRACE trace << " All the successors have been visited" << std::endl;
std::cout << " All the successors have been visited"
<< std::endl;
# endif
stack_item f_dest(f); stack_item f_dest(f);
pop(st_blue); pop(st_blue);
typename heap::color_ref c = h.get_color_ref(f_dest.s); typename heap::color_ref c = h.get_color_ref(f_dest.s);
@ -250,12 +239,10 @@ namespace spot
// the number of runs reported by successive // the number of runs reported by successive
// calls to the check method. Without this // calls to the check method. Without this
// functionnality, the test can be ommited. // functionnality, the test can be ommited.
# ifdef TRACE trace << " It is blue and the arc from "
std::cout << " It is blue and the arc from " << a_->format_state(st_blue.front().s)
<< a_->format_state(st_blue.front().s) << " to it is accepting, start a red dfs"
<< " to it is accepting, start a red dfs" << std::endl;
<< std::endl;
# endif
target = st_blue.front().s; target = st_blue.front().s;
c.set_color(RED); c.set_color(RED);
push(st_red, f_dest.s, f_dest.label, f_dest.acc); push(st_red, f_dest.s, f_dest.label, f_dest.acc);
@ -264,10 +251,7 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " Pop it" << std::endl;
std::cout << " Pop it"
<< std::endl;
# endif
h.pop_notify(f_dest.s); h.pop_notify(f_dest.s);
} }
} }
@ -284,17 +268,12 @@ namespace spot
while (!st_red.empty()) while (!st_red.empty())
{ {
stack_item& f = st_red.front(); stack_item& f = st_red.front();
# ifdef TRACE trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_RED treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -310,16 +289,12 @@ namespace spot
// to the visit of white state. Anyway, it is not necessary // to the visit of white state. Anyway, it is not necessary
// to visit white states either if a cycle can be missed // to visit white states either if a cycle can be missed
// with bit-state hashing search. // with bit-state hashing search.
# ifdef TRACE trace << " It is white, pop it" << std::endl;
std::cout << " It is white, pop it" << std::endl;
# endif
delete s_prime; delete s_prime;
} }
else if (c.get_color() == BLUE) else if (c.get_color() == BLUE)
{ {
# ifdef TRACE trace << " It is blue, go down" << std::endl;
std::cout << " It is blue, go down" << std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (target->compare(s_prime) == 0) if (target->compare(s_prime) == 0)
@ -327,18 +302,14 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " It is red, pop it" << std::endl;
std::cout << " It is red, pop it" << std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
else // Backtrack else // Backtrack
{ {
# ifdef TRACE trace << " All the successors have been visited, pop it"
std::cout << " All the successors have been visited, pop it" << std::endl;
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
pop(st_red); pop(st_red);
} }

5
src/tgbaalgos/magic.hh
View file

@ -55,8 +55,7 @@ namespace spot
/// for all t in post(s) do /// for all t in post(s) do
/// if t.color == white then /// if t.color == white then
/// call dfs_blue(t); /// call dfs_blue(t);
/// end if; /// else if (the edge (s,t) is accepting) then
/// if (the edge (s,t) is accepting) then
/// target = s; /// target = s;
/// call dfs_red(t); /// call dfs_red(t);
/// end if; /// end if;
@ -70,7 +69,7 @@ namespace spot
/// report cycle /// report cycle
/// end if; /// end if;
/// for all t in post(s) do /// for all t in post(s) do
/// if t.color != red then /// if t.color == blue then
/// call dfs_red(t); /// call dfs_red(t);
/// end if; /// end if;
/// end for; /// end for;

160
src/tgbaalgos/se05.cc
View file

@ -21,8 +21,11 @@
//#define TRACE //#define TRACE
#ifdef TRACE
#include <iostream> #include <iostream>
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif #endif
#include <cassert> #include <cassert>
@ -53,7 +56,7 @@ namespace spot
/// condition (i.e. it is a TBA). /// condition (i.e. it is a TBA).
se05_search(const tgba *a, size_t size) se05_search(const tgba *a, size_t size)
: emptiness_check(a), : emptiness_check(a),
current_weight(0), ec_statistics(),
h(size), h(size),
all_cond(a->all_acceptance_conditions()) all_cond(a->all_acceptance_conditions())
{ {
@ -92,7 +95,7 @@ namespace spot
assert(st_blue.empty()); assert(st_blue.empty());
const state* s0 = a_->get_init_state(); const state* s0 = a_->get_init_state();
inc_states(); inc_states();
h.add_new_state(s0, CYAN, current_weight); h.add_new_state(s0, CYAN);
push(st_blue, s0, bddfalse, bddfalse); push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue()) if (dfs_blue())
return new result(*this); return new result(*this);
@ -160,10 +163,6 @@ namespace spot
st.pop_front(); st.pop_front();
} }
/// \brief number of visited accepting arcs
/// in the blue stack.
int current_weight;
/// \brief Stack of the blue dfs. /// \brief Stack of the blue dfs.
stack_type st_blue; stack_type st_blue;
@ -182,17 +181,12 @@ namespace spot
while (!st_blue.empty()) while (!st_blue.empty())
{ {
stack_item& f = st_blue.front(); stack_item& f = st_blue.front();
# ifdef TRACE trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_BLUE treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -201,25 +195,16 @@ namespace spot
typename heap::color_ref c = h.get_color_ref(s_prime); typename heap::color_ref c = h.get_color_ref(s_prime);
if (c.is_white()) if (c.is_white())
{ {
# ifdef TRACE trace << " It is white, go down" << std::endl;
std::cout << " It is white, go down" << std::endl;
# endif
if (acc == all_cond)
++current_weight;
inc_states(); inc_states();
h.add_new_state(s_prime, CYAN, current_weight); h.add_new_state(s_prime, CYAN);
push(st_blue, s_prime, label, acc); push(st_blue, s_prime, label, acc);
} }
else if (c.get_color() == CYAN && (acc == all_cond || else if (c.get_color() == CYAN && (acc == all_cond ||
(f.s->compare(s_prime) != 0 && f.acc == all_cond) // option SE05 (f.s->compare(s_prime) != 0 && f.acc == all_cond)))
// current_weight > c.get_weight() // option WEIGHT
/**/))
// For Alexandre: combat style.test! ----------^
{ {
# ifdef TRACE trace << " It is cyan and acceptance condition "
std::cout << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl;
<< "is reached, report cycle" << std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
return true; return true;
@ -230,10 +215,8 @@ namespace spot
// the number of runs reported by successive // the number of runs reported by successive
// calls to the check method. Without this // calls to the check method. Without this
// functionnality, the test can be ommited. // functionnality, the test can be ommited.
# ifdef TRACE trace << " It is cyan or blue and the arc is "
std::cout << " It is cyan or blue and the arc is " << "accepting, start a red dfs" << std::endl;
<< "accepting, start a red dfs" << std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
if (dfs_red()) if (dfs_red())
@ -241,10 +224,7 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " It is cyan, blue or red, pop it" << std::endl;
std::cout << " It is cyan, blue or red, pop it"
<< std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
@ -252,14 +232,9 @@ namespace spot
// Backtrack the edge // Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s) // (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{ {
# ifdef TRACE trace << " All the successors have been visited" << std::endl;
std::cout << " All the successors have been visited"
<< std::endl;
# endif
stack_item f_dest(f); stack_item f_dest(f);
pop(st_blue); pop(st_blue);
if (f_dest.acc == all_cond)
--current_weight;
typename heap::color_ref c = h.get_color_ref(f_dest.s); typename heap::color_ref c = h.get_color_ref(f_dest.s);
assert(!c.is_white()); assert(!c.is_white());
if (!st_blue.empty() && if (!st_blue.empty() &&
@ -269,12 +244,10 @@ namespace spot
// the number of runs reported by successive // the number of runs reported by successive
// calls to the check method. Without this // calls to the check method. Without this
// functionnality, the test can be ommited. // functionnality, the test can be ommited.
# ifdef TRACE trace << " The arc from "
std::cout << " The arc from " << a_->format_state(st_blue.front().s)
<< a_->format_state(st_blue.front().s) << " to the current state is accepting, start a "
<< " to the current state is accepting, start a " << "red dfs" << std::endl;
<< "red dfs" << std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, f_dest.s, f_dest.label, f_dest.acc); push(st_red, f_dest.s, f_dest.label, f_dest.acc);
if (dfs_red()) if (dfs_red())
@ -282,9 +255,7 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " Pop it" << std::endl;
std::cout << " Pop it" << std::endl;
# endif
c.set_color(BLUE); c.set_color(BLUE);
h.pop_notify(f_dest.s); h.pop_notify(f_dest.s);
} }
@ -300,17 +271,12 @@ namespace spot
while (!st_red.empty()) while (!st_red.empty())
{ {
stack_item& f = st_red.front(); stack_item& f = st_red.front();
# ifdef TRACE trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_RED treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -325,45 +291,33 @@ namespace spot
// implying the report of a cycle. // implying the report of a cycle.
// However, with a bit-state hashing search and due to // However, with a bit-state hashing search and due to
// collision, this property does not hold. // collision, this property does not hold.
# ifdef TRACE trace << " It is white (due to collision), pop it"
std::cout << " It is white (due to collision), pop it" << std::endl;
<< std::endl;
# endif
delete s_prime; delete s_prime;
} }
else if (c.get_color() == RED) else if (c.get_color() == RED)
{ {
# ifdef TRACE trace << " It is red, pop it" << std::endl;
std::cout << " It is red, pop it"
<< std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
else if (c.get_color() == CYAN) else if (c.get_color() == CYAN)
{ {
# ifdef TRACE trace << " It is cyan, report a cycle" << std::endl;
std::cout << " It is cyan, report a cycle"
<< std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
return true; return true;
} }
else else
{ {
# ifdef TRACE trace << " It is blue, go down" << std::endl;
std::cout << " It is blue, go down" << std::endl;
# endif
c.set_color(RED); c.set_color(RED);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
} }
} }
else // Backtrack else // Backtrack
{ {
# ifdef TRACE trace << " All the successors have been visited, pop it"
std::cout << " All the successors have been visited, pop it" << std::endl;
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
pop(st_red); pop(st_red);
} }
@ -429,7 +383,7 @@ namespace spot
class explicit_se05_search_heap class explicit_se05_search_heap
{ {
typedef Sgi::hash_map<const state*, int, typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> hcyan_type; state_ptr_hash, state_ptr_equal> hcyan_type;
typedef Sgi::hash_map<const state*, color, typedef Sgi::hash_map<const state*, color,
state_ptr_hash, state_ptr_equal> hash_type; state_ptr_hash, state_ptr_equal> hash_type;
@ -437,12 +391,12 @@ namespace spot
class color_ref class color_ref
{ {
public: public:
color_ref(hash_type* h, hcyan_type* hc, const state* s, int w) color_ref(hash_type* h, hcyan_type* hc, const state* s)
: is_cyan(true), weight(w), ph(h), phc(hc), ps(s), pc(0) : is_cyan(true), ph(h), phc(hc), ps(s), pc(0)
{ {
} }
color_ref(color* c) color_ref(color* c)
: is_cyan(false), weight(0), ph(0), phc(0), ps(0), pc(c) : is_cyan(false), ph(0), phc(0), ps(0), pc(c)
{ {
} }
color get_color() const color get_color() const
@ -451,11 +405,6 @@ namespace spot
return CYAN; return CYAN;
return *pc; return *pc;
} }
int get_weight() const
{
assert(is_cyan);
return weight;
}
void set_color(color c) void set_color(color c)
{ {
assert(!is_white()); assert(!is_white());
@ -478,7 +427,6 @@ namespace spot
} }
private: private:
bool is_cyan; bool is_cyan;
int weight; // weight of a cyan node
hash_type* ph; //point to the main hash table hash_type* ph; //point to the main hash table
hcyan_type* phc; // point to the hash table hcyan hcyan_type* phc; // point to the hash table hcyan
const state* ps; // point to the state in hcyan const state* ps; // point to the state in hcyan
@ -494,7 +442,7 @@ namespace spot
hcyan_type::const_iterator sc = hc.begin(); hcyan_type::const_iterator sc = hc.begin();
while (sc != hc.end()) while (sc != hc.end())
{ {
const state* ptr = sc->first; const state* ptr = *sc;
++sc; ++sc;
delete ptr; delete ptr;
} }
@ -522,20 +470,19 @@ namespace spot
} }
return color_ref(&(it->second)); // blue or red state return color_ref(&(it->second)); // blue or red state
} }
if (s!=ic->first) if (s!=*ic)
{ {
delete s; delete s;
s = ic->first; s = *ic;
} }
return color_ref(&h, &hc, ic->first, ic->second); // cyan state return color_ref(&h, &hc, *ic); // cyan state
} }
void add_new_state(const state* s, color c, int w=-1) void add_new_state(const state* s, color c)
{ {
assert(hc.find(s)==hc.end() && h.find(s)==h.end()); assert(hc.find(s)==hc.end() && h.find(s)==h.end());
assert(c!=CYAN || w>=0);
if (c == CYAN) if (c == CYAN)
hc.insert(std::make_pair(s, w)); hc.insert(s);
else else
h.insert(std::make_pair(s, c)); h.insert(std::make_pair(s, c));
} }
@ -553,19 +500,19 @@ namespace spot
class bsh_se05_search_heap class bsh_se05_search_heap
{ {
private: private:
typedef Sgi::hash_map<const state*, int, typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> hcyan_type; state_ptr_hash, state_ptr_equal> hcyan_type;
public: public:
class color_ref class color_ref
{ {
public: public:
color_ref(hcyan_type* h, const state* st, int w, color_ref(hcyan_type* h, const state* st,
unsigned char *base, unsigned char offset) unsigned char *base, unsigned char offset)
: is_cyan(true), weight(w), phc(h), ps(st), b(base), o(offset*2) : is_cyan(true), phc(h), ps(st), b(base), o(offset*2)
{ {
} }
color_ref(unsigned char *base, unsigned char offset) color_ref(unsigned char *base, unsigned char offset)
: is_cyan(false), weight(0), phc(0), ps(0), b(base), o(offset*2) : is_cyan(false), phc(0), ps(0), b(base), o(offset*2)
{ {
} }
color get_color() const color get_color() const
@ -574,11 +521,6 @@ namespace spot
return CYAN; return CYAN;
return color(((*b) >> o) & 3U); return color(((*b) >> o) & 3U);
} }
int get_weight() const
{
assert(is_cyan);
return weight;
}
void set_color(color c) void set_color(color c)
{ {
if (is_cyan && c!=CYAN) if (is_cyan && c!=CYAN)
@ -595,7 +537,6 @@ namespace spot
} }
private: private:
bool is_cyan; bool is_cyan;
int weight;
hcyan_type* phc; hcyan_type* phc;
const state* ps; const state* ps;
unsigned char *b; unsigned char *b;
@ -618,16 +559,15 @@ namespace spot
size_t ha = s->hash(); size_t ha = s->hash();
hcyan_type::iterator ic = hc.find(s); hcyan_type::iterator ic = hc.find(s);
if (ic!=hc.end()) if (ic!=hc.end())
return color_ref(&hc, ic->first, ic->second, &h[ha%size], ha%4); return color_ref(&hc, *ic, &h[ha%size], ha%4);
return color_ref(&h[ha%size], ha%4); return color_ref(&h[ha%size], ha%4);
} }
void add_new_state(const state* s, color c, int w=-1) void add_new_state(const state* s, color c)
{ {
assert(c!=CYAN || w>=0);
assert(get_color_ref(s).is_white()); assert(get_color_ref(s).is_white());
if (c==CYAN) if (c==CYAN)
hc.insert(std::make_pair(s, w)); hc.insert(s);
else else
{ {
color_ref cr(get_color_ref(s)); color_ref cr(get_color_ref(s));

27
src/tgbaalgos/se05.hh
View file

@ -47,29 +47,21 @@ namespace spot
/// \verbatim /// \verbatim
/// procedure check () /// procedure check ()
/// begin /// begin
/// weight = 0;
/// call dfs_blue(s0); /// call dfs_blue(s0);
/// end; /// end;
/// ///
/// procedure dfs_blue (s) /// procedure dfs_blue (s)
/// begin /// begin
/// s.color = cyan; /// s.color = cyan;
/// s.weight = weight;
/// for all t in post(s) do /// for all t in post(s) do
/// if t.color == white then /// if t.color == white then
/// if the edge (s,t) is accepting then
/// weight = weight + 1;
/// end if;
/// call dfs_blue(t); /// call dfs_blue(t);
/// if the edge (s,t) is accepting then
/// weight = weight - 1;
/// end if;
/// else if t.color == cyan and /// else if t.color == cyan and
/// (the edge (s,t) is accepting or /// (the edge (s,t) is accepting or
/// weight > t.weight) then /// (it exists a predecessor p of s in st_blue and s != t and
/// the arc between p and s is accepting)) then
/// report cycle; /// report cycle;
/// end if; /// else if the edge (s,t) is accepting then
/// if the edge (s,t) is accepting then
/// call dfs_red(t); /// call dfs_red(t);
/// end if; /// end if;
/// end for; /// end for;
@ -83,15 +75,14 @@ namespace spot
/// end if; /// end if;
/// s.color = red; /// s.color = red;
/// for all t in post(s) do /// for all t in post(s) do
/// if t.color != red then /// if t.color == blue then
/// call dfs_red(t); /// call dfs_red(t);
/// end if; /// end if;
/// end for; /// end for;
/// end; /// end;
/// \endverbatim /// \endverbatim
/// ///
/// It is an adaptation to TBA (and a slight extension) of the one /// It is an adaptation to TBA of the one presented in
/// presented in
/// \verbatim /// \verbatim
/// @techreport{SE04, /// @techreport{SE04,
/// author = {Stefan Schwoon and Javier Esparza}, /// author = {Stefan Schwoon and Javier Esparza},
@ -106,12 +97,6 @@ namespace spot
/// } /// }
/// \endverbatim /// \endverbatim
/// ///
/// The extention consists in the introduction of a weight associated
/// to each state in the blue stack (the cyan states). The weight of a
/// cyan state corresponds to the number of accepting arcs traversed to reach
/// it from the initial state. Weights are used to detect accepting cycle in
/// the blue dfs.
///
/// \sa spot::explicit_magic_search /// \sa spot::explicit_magic_search
/// ///
emptiness_check* explicit_se05_search(const tgba *a); emptiness_check* explicit_se05_search(const tgba *a);
@ -122,7 +107,7 @@ namespace spot
/// it is a TBA). /// it is a TBA).
/// ///
/// During the visit of \a a, the returned checker does not store explicitely /// During the visit of \a a, the returned checker does not store explicitely
/// the traversed states but uses the bit-state hashing technicpresented in: /// the traversed states but uses the bit-state hashing technic presented in:
/// ///
/// \verbatim /// \verbatim
/// @book{Holzmann91, /// @book{Holzmann91,

101
src/tgbaalgos/tau03.cc
View file

@ -25,9 +25,11 @@
//#define TRACE //#define TRACE
#ifdef TRACE
#include <iostream> #include <iostream>
#include "tgba/bddprint.hh" #ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif #endif
#include <cassert> #include <cassert>
@ -155,17 +157,12 @@ namespace spot
while (!st_blue.empty()) while (!st_blue.empty())
{ {
stack_item& f = st_blue.front(); stack_item& f = st_blue.front();
# ifdef TRACE trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_BLUE treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -174,18 +171,14 @@ namespace spot
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())
{ {
# ifdef TRACE trace << " It is white, go down" << std::endl;
std::cout << " It is white, go down" << std::endl;
# endif
inc_states(); inc_states();
h.add_new_state(s_prime, BLUE); h.add_new_state(s_prime, BLUE);
push(st_blue, s_prime, label, acc); push(st_blue, s_prime, label, acc);
} }
else else
{ {
# ifdef TRACE trace << " It is blue, pop it" << std::endl;
std::cout << " It is blue, pop it" << std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
@ -193,11 +186,9 @@ namespace spot
// Backtrack the edge // Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s) // (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{ {
# ifdef TRACE trace << " All the successors have been visited"
std::cout << " All the successors have been visited" << ", rescan this successors"
<< ", rescan this successors" << std::endl;
<< std::endl;
# endif
typename heap::color_ref c = h.get_color_ref(f.s); typename heap::color_ref c = h.get_color_ref(f.s);
assert(!c.is_white()); assert(!c.is_white());
tgba_succ_iterator* i = a_->succ_iter(f.s); tgba_succ_iterator* i = a_->succ_iter(f.s);
@ -205,11 +196,9 @@ namespace spot
{ {
inc_transitions(); inc_transitions();
const state *s_prime = i->current_state(); const state *s_prime = i->current_state();
#ifdef TRACE trace << "DFS_BLUE rescanning the arc from "
std::cout << "DFS_BLUE rescanning the arc from " << a_->format_state(f.s) << " to "
<< a_->format_state(f.s) << " to " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = i->current_condition(); bdd label = i->current_condition();
bdd acc = i->current_acceptance_conditions(); bdd acc = i->current_acceptance_conditions();
typename heap::color_ref c_prime = h.get_color_ref(s_prime); typename heap::color_ref c_prime = h.get_color_ref(s_prime);
@ -217,19 +206,8 @@ namespace spot
bdd acu = acc | c.get_acc(); bdd acu = acc | c.get_acc();
if ((c_prime.get_acc() & acu) != acu) if ((c_prime.get_acc() & acu) != acu)
{ {
# ifdef TRACE trace << " a propagation is needed, go down"
std::cout << " "; << std::endl;
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)
<< " propagating: ";
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# 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);
dfs_red(acu); dfs_red(acu);
@ -238,18 +216,14 @@ namespace spot
delete i; delete i;
if (c.get_acc() == all_cond) if (c.get_acc() == all_cond)
{ {
#ifdef TRACE trace << "DFS_BLUE propagation is successful, report a"
std::cout << "DFS_BLUE propagation is successful, report a" << " cycle" << std::endl;
<< " cycle" << std::endl;
# endif
return true; return true;
} }
else else
{ {
#ifdef TRACE trace << "DFS_BLUE propagation is unsuccessful, pop it"
std::cout << "DFS_BLUE propagation is unsuccessful, pop it"; << std::endl;
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
pop(st_blue); pop(st_blue);
} }
@ -265,17 +239,12 @@ namespace spot
while (!st_red.empty()) while (!st_red.empty())
{ {
stack_item& f = st_red.front(); stack_item& f = st_red.front();
#ifdef TRACE trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_RED treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
#ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -284,35 +253,27 @@ namespace spot
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())
{ {
# ifdef TRACE trace << " It is white, pop it" << std::endl;
std::cout << " It is white, pop it" << std::endl;
# endif
delete s_prime; delete s_prime;
} }
else if ((c_prime.get_acc() & acu) != acu) else if ((c_prime.get_acc() & acu) != acu)
{ {
# ifdef TRACE trace << " It is blue and propagation "
std::cout << " It is blue and propagation " << "is needed, go down" << std::endl;
<< "is needed, go down" << std::endl;
# 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);
} }
else else
{ {
# ifdef TRACE trace << " It is blue and no propagation "
std::cout << " It is blue and no propagation " << "is needed, pop it" << std::endl;
<< "is needed, pop it" << std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
else // Backtrack else // Backtrack
{ {
# ifdef TRACE trace << " All the successors have been visited, pop it"
std::cout << " All the successors have been visited, pop it" << std::endl;
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
pop(st_red); pop(st_red);
} }

177
src/tgbaalgos/tau03opt.cc
View file

@ -33,15 +33,14 @@
/// after the visit of previous successors). /// after the visit of previous successors).
/// ///
/// * Add a bit-state hashing version. /// * Add a bit-state hashing version.
///
/// * Is it possible to reduce the tgba on-the-fly during the product: only the
/// acceptance conditions are pertinent...
//#define TRACE //#define TRACE
#ifdef TRACE
#include <iostream> #include <iostream>
#include "tgba/bddprint.hh" #ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif #endif
#include <cassert> #include <cassert>
@ -105,7 +104,10 @@ namespace spot
h.add_new_state(s0, CYAN, current_weight); h.add_new_state(s0, CYAN, current_weight);
push(st_blue, s0, bddfalse, bddfalse); push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue()) if (dfs_blue())
return new emptiness_check_result(a_); if (a_->number_of_acceptance_conditions() <=1)
return new result(*this);
else
return new emptiness_check_result(a_);
return 0; return 0;
} }
@ -173,17 +175,12 @@ namespace spot
while (!st_blue.empty()) while (!st_blue.empty())
{ {
stack_item& f = st_blue.front(); stack_item& f = st_blue.front();
# ifdef TRACE trace << "DFS_BLUE treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_BLUE treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -192,9 +189,7 @@ namespace spot
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())
{ {
# ifdef TRACE trace << " It is white, go down" << std::endl;
std::cout << " It is white, go down" << std::endl;
# endif
current_weight += acc; current_weight += acc;
inc_states(); inc_states();
h.add_new_state(s_prime, CYAN, current_weight); h.add_new_state(s_prime, CYAN, current_weight);
@ -208,31 +203,20 @@ namespace spot
((current_weight - c_prime.get_weight()) | ((current_weight - c_prime.get_weight()) |
c.get_acc() | acc | c_prime.get_acc()) == all_acc) c.get_acc() | acc | c_prime.get_acc()) == all_acc)
{ {
# ifdef TRACE trace << " It is cyan and acceptance condition "
std::cout << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl;
<< "is reached, report cycle" << std::endl;
# endif
c_prime.cumulate_acc(c.get_acc() | acc); c_prime.cumulate_acc(c.get_acc() | acc);
push(st_red, s_prime, label, acc); push(st_red, s_prime, label, acc);
return true; return true;
} }
else else
{ {
# ifdef TRACE trace << " It is cyan or blue and";
std::cout << " It is cyan or blue and";
# endif
bdd acu = acc | c.get_acc(); bdd acu = acc | c.get_acc();
if ((c_prime.get_acc() & acu) != acu) if ((c_prime.get_acc() & acu) != acu)
{ {
# ifdef TRACE trace << " a propagation is needed, "
bdd_print_acc(std::cout, a_->get_dict(), acu); << "start a red dfs" << std::endl;
std::cout << " is not included in ";
bdd_print_acc(std::cout, a_->get_dict(),
c_prime.get_acc());
std::cout << ", start a red dfs propagating: ";
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# 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 (dfs_red(acu)) if (dfs_red(acu))
@ -240,10 +224,8 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " no propagation is needed, pop it."
std::cout << " no propagation is needed, pop it." << std::endl;
<< std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
@ -253,10 +235,7 @@ namespace spot
// Backtrack the edge // Backtrack the edge
// (predecessor of f.s in st_blue, <f.label, f.acc>, f.s) // (predecessor of f.s in st_blue, <f.label, f.acc>, f.s)
{ {
# ifdef TRACE trace << " All the successors have been visited" << std::endl;
std::cout << " All the successors have been visited"
<< std::endl;
# endif
stack_item f_dest(f); stack_item f_dest(f);
pop(st_blue); pop(st_blue);
current_weight -= f_dest.acc; current_weight -= f_dest.acc;
@ -271,14 +250,10 @@ namespace spot
bdd acu = f_dest.acc | c.get_acc(); bdd acu = f_dest.acc | c.get_acc();
if ((c_prime.get_acc() & acu) != acu) if ((c_prime.get_acc() & acu) != acu)
{ {
# ifdef TRACE trace << " The arc from "
std::cout << " The arc from " << a_->format_state(st_blue.front().s)
<< a_->format_state(st_blue.front().s) << " to the current state implies to "
<< " to the current state implies to " << " start a red dfs" << std::endl;
<< " start a red dfs propagating ";
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# endif
c_prime.cumulate_acc(acu); c_prime.cumulate_acc(acu);
push(st_red, f_dest.s, f_dest.label, f_dest.acc); push(st_red, f_dest.s, f_dest.label, f_dest.acc);
if (dfs_red(acu)) if (dfs_red(acu))
@ -286,17 +261,13 @@ namespace spot
} }
else else
{ {
# ifdef TRACE trace << " Pop it" << std::endl;
std::cout << " Pop it" << std::endl;
# endif
h.pop_notify(f_dest.s); h.pop_notify(f_dest.s);
} }
} }
else else
{ {
# ifdef TRACE trace << " Pop it" << std::endl;
std::cout << " Pop it" << std::endl;
# endif
h.pop_notify(f_dest.s); h.pop_notify(f_dest.s);
} }
} }
@ -311,17 +282,12 @@ namespace spot
while (!st_red.empty()) while (!st_red.empty())
{ {
stack_item& f = st_red.front(); stack_item& f = st_red.front();
# ifdef TRACE trace << "DFS_RED treats: " << a_->format_state(f.s) << std::endl;
std::cout << "DFS_RED treats: "
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done()) if (!f.it->done())
{ {
const state *s_prime = f.it->current_state(); const state *s_prime = f.it->current_state();
# ifdef TRACE trace << " Visit the successor: "
std::cout << " Visit the successor: " << a_->format_state(s_prime) << std::endl;
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = f.it->current_condition(); bdd label = f.it->current_condition();
bdd acc = f.it->current_acceptance_conditions(); bdd acc = f.it->current_acceptance_conditions();
// Go down the edge (f.s, <label, acc>, s_prime) // Go down the edge (f.s, <label, acc>, s_prime)
@ -330,48 +296,38 @@ namespace spot
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())
{ {
# ifdef TRACE trace << " It is white, pop it" << std::endl;
std::cout << " It is white, pop it" << std::endl;
# endif
delete s_prime; delete s_prime;
} }
else if (c_prime.get_color() == CYAN && else if (c_prime.get_color() == CYAN &&
((current_weight - c_prime.get_weight()) | ((current_weight - c_prime.get_weight()) |
c_prime.get_acc() | acu) == all_acc) c_prime.get_acc() | acu) == all_acc)
{ {
# ifdef TRACE trace << " It is cyan and acceptance condition "
std::cout << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl;
<< "is reached, report cycle" << std::endl;
# 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);
return true; return true;
} }
else if ((c_prime.get_acc() & acu) != acu) else if ((c_prime.get_acc() & acu) != acu)
{ {
# ifdef TRACE trace << " It is cyan or blue and propagation "
std::cout << " It is cyan or blue and propagation " << "is needed, go down"
<< "is needed, go down" << std::endl;
<< std::endl;
# 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);
} }
else else
{ {
# ifdef TRACE trace << " It is cyan or blue and no propagation "
std::cout << " It is cyan or blue and no propagation " << "is needed , pop it" << std::endl;
<< "is needed , pop it" << std::endl;
# endif
h.pop_notify(s_prime); h.pop_notify(s_prime);
} }
} }
else // Backtrack else // Backtrack
{ {
# ifdef TRACE trace << " All the successors have been visited, pop it"
std::cout << " All the successors have been visited, pop it" << std::endl;
<< std::endl;
# endif
h.pop_notify(f.s); h.pop_notify(f.s);
pop(st_red); pop(st_red);
} }
@ -379,6 +335,61 @@ namespace spot
return false; return false;
} }
class result: public emptiness_check_result
{
public:
result(tau03_opt_search& ms)
: emptiness_check_result(ms.a_),
ms_(ms)
{
}
virtual tgba_run* accepting_run()
{
assert(!ms_.st_blue.empty());
assert(!ms_.st_red.empty());
tgba_run* run = new tgba_run;
typename stack_type::const_reverse_iterator i, j, end;
tgba_run::steps* l;
const state* target = ms_.st_red.front().s;
l = &run->prefix;
i = ms_.st_blue.rbegin();
end = ms_.st_blue.rend(); --end;
j = i; ++j;
for (; i != end; ++i, ++j)
{
if (l == &run->prefix && i->s->compare(target) == 0)
l = &run->cycle;
tgba_run::step s = { i->s->clone(), j->label, j->acc };
l->push_back(s);
}
if (l == &run->prefix && i->s->compare(target) == 0)
l = &run->cycle;
assert(l == &run->cycle);
j = ms_.st_red.rbegin();
tgba_run::step s = { i->s->clone(), j->label, j->acc };
l->push_back(s);
i = j; ++j;
end = ms_.st_red.rend(); --end;
for (; i != end; ++i, ++j)
{
tgba_run::step s = { i->s->clone(), j->label, j->acc };
l->push_back(s);
}
return run;
}
private:
tau03_opt_search& ms_;
};
}; };
class explicit_tau03_opt_search_heap class explicit_tau03_opt_search_heap

48
src/tgbaalgos/tau03opt.hh
View file

@ -40,6 +40,7 @@ namespace spot
/// \verbatim /// \verbatim
/// procedure check () /// procedure check ()
/// begin /// begin
/// weight = 0; // the null vector
/// call dfs_blue(s0); /// call dfs_blue(s0);
/// end; /// end;
/// ///
@ -47,41 +48,52 @@ namespace spot
/// begin /// begin
/// s.color = cyan; /// s.color = cyan;
/// s.acc = emptyset; /// s.acc = emptyset;
/// s.weight = weight;
/// 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 t.color == white then /// if t.color == white then
/// for all b in a do
/// weight[b] = weight[b] + 1;
/// end for;
/// call dfs_blue(t); /// call dfs_blue(t);
/// else if t.color == cyan && s.acc U a U t.acc == all_acc then /// for all b in a do
/// report a cycle; /// weight[b] = weight[b] - 1;
/// end if; /// end for;
/// end for; /// else
/// 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; /// Acc = s.acc U a;
/// if s.acc U a not included in t.acc then /// if t.color == cyan &&
/// call dfs_red(t, a U s.acc); /// (Acc U support(weight -s.weight) U t.acc) == all_acc then
/// report a cycle;
/// else if Acc not included in t.acc then
/// call dfs_red(t, Acc);
/// end if;
/// end if; /// end if;
/// end for; /// end for;
/// s.color = blue; /// s.color = blue;
/// end; /// end;
/// ///
/// procedure dfs_red(s, A) /// procedure dfs_red(s, Acc)
/// begin /// begin
/// s.acc = s.acc U A;
/// 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 t.color != white then /// if t.color == cyan &&
/// if t.color == cyan && A U t.acc == all_acc then /// (Acc U support(weight -t.weight) U t.acc) == all_acc then
/// report a cycle; /// report a cycle;
/// else if A not included in t.acc then /// else if t.color != white and Acc not included in t.acc then
/// call dfs_red(t, A); /// call dfs_red(t, Acc);
/// end if;
/// end if; /// end if;
/// end for; /// end for;
/// end; /// end;
/// \endverbatim /// \endverbatim
/// ///
/// This algorithm is an optimisation of the one implemented in /// This algorithm is a generalisation to TGBA of the one implemented in
/// spot::explicit_tau03_search. /// spot::explicit_se05_search. It is based on the acceptance set labelling
/// of states used in spot::explicit_tau03_search. Moreover, it introduce
/// a slight optimisation based on vectors of integers counting for each
/// acceptance condition how many time the condition has been visited in
/// the path stored in the blue stack. Such a vector is associated to each
/// state of this stack.
/// ///
emptiness_check* explicit_tau03_opt_search(const tgba *a); emptiness_check* explicit_tau03_opt_search(const tgba *a);

10
src/tgbatest/randtgba.cc
View file

@ -340,11 +340,11 @@ main(int argc, char** argv)
spot::tgba* d = opt_n_acc > 1 ? degen : a; spot::tgba* d = opt_n_acc > 1 ? degen : a;
ec_obj.push_back(spot::explicit_magic_search(d)); ec_obj.push_back(spot::explicit_magic_search(d));
ec_name.push_back("explicit_magic_search"); ec_name.push_back("explicit_magic");
ec_safe.push_back(true); ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096)); ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096));
ec_name.push_back("bit_state_hashing_magic_search"); ec_name.push_back("bit_state_hashing_magic");
ec_safe.push_back(false); ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_se05_search(d)); ec_obj.push_back(spot::explicit_se05_search(d));
@ -352,7 +352,7 @@ main(int argc, char** argv)
ec_safe.push_back(true); ec_safe.push_back(true);
ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096)); ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096));
ec_name.push_back("bit_state_hashing_se05_search"); ec_name.push_back("bit_state_hashing_se05");
ec_safe.push_back(false); ec_safe.push_back(false);
ec_obj.push_back(spot::explicit_gv04_check(d)); ec_obj.push_back(spot::explicit_gv04_check(d));
@ -365,12 +365,12 @@ main(int argc, char** argv)
spot::tgba* d = opt_n_acc == 0 ? degen : a; spot::tgba* d = opt_n_acc == 0 ? degen : a;
ec_obj.push_back(spot::explicit_tau03_search(d)); ec_obj.push_back(spot::explicit_tau03_search(d));
ec_name.push_back("explicit_tau03_search"); ec_name.push_back("explicit_tau03");
ec_safe.push_back(true); ec_safe.push_back(true);
} }
ec_obj.push_back(spot::explicit_tau03_opt_search(a)); ec_obj.push_back(spot::explicit_tau03_opt_search(a));
ec_name.push_back("explicit_tau03_opt_search"); ec_name.push_back("explicit_tau03_opt");
ec_safe.push_back(true); ec_safe.push_back(true);
int n_ec = ec_obj.size(); int n_ec = ec_obj.size();