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

* src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result):

Browse source 
Add the TGBA considered as a protected attribute, and provide an
automaton() accessor.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow
this new interface.
This commit is contained in:
Alexandre Duret-Lutz 2004-11-25 12:51:04 +00:00
parent 16e54b2fc4
commit f47f955a34
9 changed files with 97 additions and 77 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2004-11-25 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness.hh (emptiness_check, emptiness_check_result):
Add the TGBA considered as a protected attribute, and provide an
automaton() accessor.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/gtec.cc: Adjust to follow
this new interface.
2004-11-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Revert

28
src/tgbaalgos/emptiness.hh
View file

@ -73,6 +73,11 @@ namespace spot
class emptiness_check_result
{
public:
emptiness_check_result(const tgba* a)
: a_(a)
{
}
/// \brief Return a run accepted by the automata passed to
/// the emptiness check.
///
@ -86,14 +91,34 @@ namespace spot
/// is no counter-example; the mere existence of an instance of
/// this class asserts the existence of a counter-example).
virtual tgba_run* accepting_run();
/// The automaton on which an accepting_run() was found.
const tgba*
automaton() const
{
return a_;
}
protected:
const tgba* a_; ///< The automaton.
};
/// Common interface to emptiness check algorithms.
class emptiness_check
{
public:
emptiness_check(const tgba* a)
: a_(a)
{
}
virtual ~emptiness_check();
/// The automaton that this emptiness-check inspects.
const tgba*
automaton() const
{
return a_;
}
/// \brief Check whether the automaton contain an accepting run.
///
/// Return 0 if the automaton accept no run. Return an instance
@ -108,6 +133,9 @@ namespace spot
/// Print statistics, if any.
virtual std::ostream& print_stats(std::ostream& os) const;
protected:
const tgba* a_; ///< The automaton.
};
/// @}

2
src/tgbaalgos/gtec/ce.cc
View file

@ -27,7 +27,7 @@ namespace spot
couvreur99_check_result::couvreur99_check_result
(const couvreur99_check_status* ecs,
const explicit_connected_component_factory* eccf)
: ecs_(ecs), eccf_(eccf)
: emptiness_check_result(ecs->aut), ecs_(ecs), eccf_(eccf)
{
}

1
src/tgbaalgos/gtec/gtec.cc
View file

@ -31,6 +31,7 @@ namespace spot
couvreur99_check::couvreur99_check(const tgba* a,
const numbered_state_heap_factory* nshf)
: emptiness_check(a)
{
ecs_ = new couvreur99_check_status(a, nshf);
}

21
src/tgbaalgos/gv04.cc
View file

@ -52,9 +52,6 @@ namespace spot
struct gv04: public emptiness_check, public ec_statistics
{
// The automata to check.
const tgba* a;
// The unique accepting condition of the automaton \a a,
// or bddfalse if there is no.
bdd accepting;
@ -73,7 +70,7 @@ namespace spot
bool violation; // Whether an accepting run was found.
gv04(const tgba *a)
: a(a), accepting(a->all_acceptance_conditions())
: emptiness_check(a), accepting(a->all_acceptance_conditions())
{
assert(a->number_of_acceptance_conditions() <= 1);
}
@ -97,19 +94,19 @@ namespace spot
{
top = dftop = -1;
violation = false;
push(a->get_init_state(), false);
push(a_->get_init_state(), false);
while (!violation && dftop >= 0)
{
trace << "Main iteration (top = " << top
<< ", dftop = " << dftop
<< ", s = " << a->format_state(stack[dftop].s)
<< ", s = " << a_->format_state(stack[dftop].s)
<< ")" << std::endl;
tgba_succ_iterator* iter = stack[dftop].lasttr;
if (!iter)
{
iter = stack[dftop].lasttr = a->succ_iter(stack[dftop].s);
iter = stack[dftop].lasttr = a_->succ_iter(stack[dftop].s);
iter->first();
}
else
@ -129,7 +126,7 @@ namespace spot
inc_transitions();
trace << " Next successor: s_prime = "
<< a->format_state(s_prime)
<< a_->format_state(s_prime)
<< (acc ? " (with accepting link)" : "");
hash_type::const_iterator i = h.find(s_prime);
@ -169,7 +166,7 @@ namespace spot
void
push(const state* s, bool accepting)
{
trace << " push(s = " << a->format_state(s)
trace << " push(s = " << a_->format_state(s)
<< ", accepting = " << accepting << ")" << std::endl;
h[s] = ++top;
@ -244,7 +241,7 @@ namespace spot
gv04& data;
result(gv04& data)
: data(data)
: emptiness_check_result(data.automaton()), data(data)
{
}
@ -269,7 +266,7 @@ namespace spot
for (int i = 0; i <= data.top; ++i)
{
trace << "state " << i << " ("
<< data.a->format_state(data.stack[i].s)
<< data.a_->format_state(data.stack[i].s)
<< ") has lowlink = " << data.stack[i].lowlink << std::endl;
}
#endif
@ -306,7 +303,7 @@ namespace spot
int scc_root;
first_bfs(const gv04& data, int scc_root)
: bfs_steps(data.a), data(data), scc_root(scc_root)
: bfs_steps(data.automaton()), data(data), scc_root(scc_root)
{
}

22
src/tgbaalgos/magic.cc
View file

@ -50,9 +50,8 @@ namespace spot
/// \pre The automaton \a a must have at most one accepting
/// condition (i.e. it is a TBA).
magic_search(const tgba *a, size_t size)
: ec_statistics(),
: emptiness_check(a),
h(size),
a(a),
all_cond(a->all_acceptance_conditions())
{
assert(a->number_of_acceptance_conditions() <= 1);
@ -88,7 +87,7 @@ namespace spot
if (st_red.empty())
{
assert(st_blue.empty());
const state* s0 = a->get_init_state();
const state* s0 = a_->get_init_state();
inc_states();
h.add_new_state(s0, BLUE);
push(st_blue, s0, bddfalse, bddfalse);
@ -146,7 +145,7 @@ namespace spot
const bdd& label, const bdd& acc)
{
inc_depth();
tgba_succ_iterator* i = a->succ_iter(s);
tgba_succ_iterator* i = a_->succ_iter(s);
i->first();
st.push_front(stack_item(s, i, label, acc));
}
@ -171,9 +170,6 @@ namespace spot
/// State targeted by the red dfs.
const state* target;
/// The automata to check.
const tgba* a;
/// The unique accepting condition of the automaton \a a.
bdd all_cond;
@ -184,14 +180,14 @@ namespace spot
stack_item& f = st_blue.front();
# ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -256,7 +252,7 @@ namespace spot
// functionnality, the test can be ommited.
# ifdef TRACE
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"
<< std::endl;
# endif
@ -290,14 +286,14 @@ namespace spot
stack_item& f = st_red.front();
# ifdef TRACE
std::cout << "DFS_RED treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -354,7 +350,7 @@ namespace spot
{
public:
result(magic_search& ms)
: ms_(ms)
: emptiness_check_result(ms.automaton()), ms_(ms)
{
}
virtual tgba_run* accepting_run()

22
src/tgbaalgos/se05.cc
View file

@ -52,10 +52,9 @@ namespace spot
/// \pre The automaton \a a must have at most one accepting
/// condition (i.e. it is a TBA).
se05_search(const tgba *a, size_t size)
: ec_statistics(),
: emptiness_check(a),
current_weight(0),
h(size),
a(a),
all_cond(a->all_acceptance_conditions())
{
assert(a->number_of_acceptance_conditions() <= 1);
@ -91,7 +90,7 @@ namespace spot
if (st_red.empty())
{
assert(st_blue.empty());
const state* s0 = a->get_init_state();
const state* s0 = a_->get_init_state();
inc_states();
h.add_new_state(s0, CYAN, current_weight);
push(st_blue, s0, bddfalse, bddfalse);
@ -149,7 +148,7 @@ namespace spot
const bdd& label, const bdd& acc)
{
inc_depth();
tgba_succ_iterator* i = a->succ_iter(s);
tgba_succ_iterator* i = a_->succ_iter(s);
i->first();
st.push_front(stack_item(s, i, label, acc));
}
@ -175,9 +174,6 @@ namespace spot
/// 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_cond;
@ -188,14 +184,14 @@ namespace spot
stack_item& f = st_blue.front();
# ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -275,7 +271,7 @@ namespace spot
// functionnality, the test can be ommited.
# ifdef TRACE
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 "
<< "red dfs" << std::endl;
# endif
@ -306,14 +302,14 @@ namespace spot
stack_item& f = st_red.front();
# ifdef TRACE
std::cout << "DFS_RED treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -379,7 +375,7 @@ namespace spot
{
public:
result(se05_search& ms)
: ms_(ms)
: emptiness_check_result(ms.automaton()), ms_(ms)
{
}
virtual tgba_run* accepting_run()

36
src/tgbaalgos/tau03.cc
View file

@ -52,9 +52,8 @@ namespace spot
public:
/// \brief Initialize the search algorithm on the automaton \a a
tau03_search(const tgba *a, size_t size)
: ec_statistics(),
: emptiness_check(a),
h(size),
a(a),
all_cond(a->all_acceptance_conditions())
{
assert(a->number_of_acceptance_conditions() > 0);
@ -86,12 +85,12 @@ namespace spot
if (!st_blue.empty())
return 0;
assert(st_red.empty());
const state* s0 = a->get_init_state();
const state* s0 = a_->get_init_state();
inc_states();
h.add_new_state(s0, BLUE);
push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue())
return new emptiness_check_result;
return new emptiness_check_result(a_);
return 0;
}
@ -126,7 +125,7 @@ namespace spot
const bdd& label, const bdd& acc)
{
inc_depth();
tgba_succ_iterator* i = a->succ_iter(s);
tgba_succ_iterator* i = a_->succ_iter(s);
i->first();
st.push_front(stack_item(s, i, label, acc));
}
@ -148,9 +147,6 @@ namespace spot
/// 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_cond;
@ -161,14 +157,14 @@ namespace spot
stack_item& f = st_blue.front();
# ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -204,15 +200,15 @@ namespace spot
# 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);
tgba_succ_iterator* i = a_->succ_iter(f.s);
for (i->first(); !i->done(); i->next())
{
inc_transitions();
const state *s_prime = i->current_state();
#ifdef TRACE
std::cout << "DFS_BLUE rescanning the arc from "
<< a->format_state(f.s) << " to "
<< a->format_state(s_prime) << std::endl;
<< a_->format_state(f.s) << " to "
<< a_->format_state(s_prime) << std::endl;
# endif
bdd label = i->current_condition();
bdd acc = i->current_acceptance_conditions();
@ -223,15 +219,15 @@ namespace spot
{
# ifdef TRACE
std::cout << " ";
bdd_print_acc(std::cout, a->get_dict(), acu);
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());
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: ";
bdd_print_acc(std::cout, a->get_dict(), acu);
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# endif
c_prime.cumulate_acc(acu);
@ -271,14 +267,14 @@ namespace spot
stack_item& f = st_red.front();
#ifdef TRACE
std::cout << "DFS_RED treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
#ifdef TRACE
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 acc = f.it->current_acceptance_conditions();

32
src/tgbaalgos/tau03opt.cc
View file

@ -67,10 +67,9 @@ namespace spot
public:
/// \brief Initialize the search algorithm on the automaton \a a
tau03_opt_search(const tgba *a, size_t size)
: ec_statistics(),
: emptiness_check(a),
current_weight(a->neg_acceptance_conditions()),
h(size),
a(a),
all_acc(a->all_acceptance_conditions())
{
}
@ -101,12 +100,12 @@ namespace spot
if (!st_blue.empty())
return 0;
assert(st_red.empty());
const state* s0 = a->get_init_state();
const state* s0 = a_->get_init_state();
inc_states();
h.add_new_state(s0, CYAN, current_weight);
push(st_blue, s0, bddfalse, bddfalse);
if (dfs_blue())
return new emptiness_check_result;
return new emptiness_check_result(a_);
return 0;
}
@ -141,7 +140,7 @@ namespace spot
const bdd& label, const bdd& acc)
{
inc_depth();
tgba_succ_iterator* i = a->succ_iter(s);
tgba_succ_iterator* i = a_->succ_iter(s);
i->first();
st.push_front(stack_item(s, i, label, acc));
}
@ -166,9 +165,6 @@ namespace spot
/// 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;
@ -179,14 +175,14 @@ namespace spot
stack_item& f = st_blue.front();
# ifdef TRACE
std::cout << "DFS_BLUE treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();
@ -229,12 +225,12 @@ namespace spot
if ((c_prime.get_acc() & acu) != acu)
{
# ifdef TRACE
bdd_print_acc(std::cout, a->get_dict(), acu);
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());
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);
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# endif
c_prime.cumulate_acc(acu);
@ -277,10 +273,10 @@ namespace spot
{
# ifdef TRACE
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 "
<< " start a red dfs propagating ";
bdd_print_acc(std::cout, a->get_dict(), acu);
bdd_print_acc(std::cout, a_->get_dict(), acu);
std::cout << std::endl;
# endif
c_prime.cumulate_acc(acu);
@ -317,14 +313,14 @@ namespace spot
stack_item& f = st_red.front();
# ifdef TRACE
std::cout << "DFS_RED treats: "
<< a->format_state(f.s) << std::endl;
<< a_->format_state(f.s) << std::endl;
# endif
if (!f.it->done())
{
const state *s_prime = f.it->current_state();
# ifdef TRACE
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 acc = f.it->current_acceptance_conditions();