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

cycles: rewrite using the tgba_digraph interface

Browse source 
Fixes #50.

* src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh: Rewrite using
unsigned instead of state*, and std::vector instead of std::map.
* src/tgbaalgos/isweakscc.cc, src/tgbaalgos/powerset.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-18 14:03:16 +01:00
parent 8fd594f5d0
commit 1411fa6063
4 changed files with 76 additions and 122 deletions
Download patch file Download diff file Expand all files Collapse all files

118
src/tgbaalgos/cycles.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@ -23,23 +23,25 @@
namespace spot
{
enumerate_cycles::enumerate_cycles(const scc_info& map)
: aut_(map.get_aut()), sm_(map)
: aut_(map.get_aut()),
info_(aut_->num_states(), aut_->num_states()),
sm_(map)
{
}
void
enumerate_cycles::nocycle(tagged_state x, tagged_state y)
enumerate_cycles::nocycle(unsigned x, unsigned y)
{
// insert x in B(y)
y->second.b.insert(x->first);
info_[y].b.push_back(x);
// remove y from A(x)
x->second.del.insert(y->first);
info_[x].del[y] = true;
}
void
enumerate_cycles::unmark(tagged_state y)
enumerate_cycles::unmark(unsigned y)
{
std::deque<tagged_state> q;
std::vector<unsigned> q;
q.push_back(y);
while (!q.empty())
@ -47,102 +49,82 @@ namespace spot
y = q.back();
q.pop_back();
y->second.mark = false;
for (auto s: y->second.b)
info_[y].mark = false;
for (auto x: info_[y].b)
{
tagged_state x = tags_.find(s);
assert(x != tags_.end());
assert(info_[x].seen);
// insert y in A(x)
x->second.del.erase(y->first);
info_[x].del[y] = false;
// unmark x recursively if marked
if (x->second.mark)
if (info_[x].mark)
q.push_back(x);
}
// empty B(y)
y->second.b.clear();
info_[y].b.clear();
}
}
enumerate_cycles::tagged_state
enumerate_cycles::tag_state(const state* s)
{
auto p = tags_.emplace(s, state_info());
if (!p.second)
s->destroy();
return p.first;
}
void
enumerate_cycles::push_state(tagged_state ts)
enumerate_cycles::push_state(unsigned s)
{
ts->second.mark = true;
dfs_entry e;
e.ts = ts;
e.succ = 0;
e.f = false;
dfs_.push_back(e);
info_[s].mark = true;
dfs_.emplace_back(s);
}
// FIXME: Recode this algorithm using unsigned states.
void
enumerate_cycles::run(unsigned scc)
{
bool keep_going = true;
push_state(tag_state(aut_->state_from_number(sm_.one_state_of(scc))));
{
unsigned s = sm_.one_state_of(scc);
info_[s].seen = true;
push_state(s);
}
while (keep_going && !dfs_.empty())
{
dfs_entry& cur = dfs_.back();
bool cont;
if (cur.succ == 0)
{
cur.succ = aut_->succ_iter(cur.ts->first);
cont = cur.succ->first();
}
cur.succ = aut_->get_graph().state_storage(cur.s).succ;
else
cont = cur.succ->next();
if (cont)
cur.succ = aut_->trans_storage(cur.succ).next_succ;
if (cur.succ)
{
// Explore one successor.
// Ignore those that are not on the SCC, or destination
// that have been "virtually" deleted from A(v).
state* s = cur.succ->current_state();
if ((sm_.scc_of(aut_->state_number(s)) != scc)
|| (cur.ts->second.del.find(s) != cur.ts->second.del.end()))
{
s->destroy();
continue;
}
unsigned s = aut_->trans_storage(cur.succ).dst;
tagged_state w = tag_state(s);
if (!w->second.mark)
if ((sm_.scc_of(s) != scc) || (info_[cur.s].del[s]))
continue;
info_[s].seen = true;
if (!info_[s].mark)
{
push_state(w);
push_state(s);
}
else if (!w->second.reach)
else if (!info_[s].reach)
{
keep_going = cycle_found(w->first);
keep_going = cycle_found(s);
cur.f = true;
}
else
{
nocycle(cur.ts, w);
nocycle(cur.s, s);
}
}
else
{
// No more successors.
bool f = cur.f;
tagged_state v = cur.ts;
aut_->release_iter(cur.succ);
unsigned v = cur.s;
dfs_.pop_back();
if (f)
unmark(v);
v->second.reach = true;
info_[v].reach = true;
// Update the predecessor in the stack if there is one.
if (!dfs_.empty())
@ -150,39 +132,25 @@ namespace spot
if (f)
dfs_.back().f = true;
else
nocycle(dfs_.back().ts, v);
nocycle(dfs_.back().s, v);
}
}
}
// Purge the dfs_ stack, in case we aborted because cycle_found()
// returned false.
while (!dfs_.empty())
{
aut_->release_iter(dfs_.back().succ);
dfs_.pop_back();
}
hash_type::iterator i = tags_.begin();
while (i != tags_.end())
{
hash_type::iterator old = i;
++i;
old->first->destroy();
}
tags_.clear();
dfs_.clear();
}
bool
enumerate_cycles::cycle_found(const state* start)
enumerate_cycles::cycle_found(unsigned start)
{
dfs_stack::const_iterator i = dfs_.begin();
while (i->ts->first != start)
while (i->s != start)
++i;
do
{
std::cout << aut_->format_state(i->ts->first) << ' ';
std::cout << i->s << ' ';
++i;
}
while (i != dfs_.end());

52
src/tgbaalgos/cycles.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -80,10 +80,11 @@ namespace spot
// Extra information required for the algorithm for each state.
struct state_info
{
state_info()
: reach(false), mark(false)
state_info(unsigned num)
: seen(false), reach(false), mark(false), del(num)
{
}
bool seen;
// Whether the state has already left the stack at least once.
bool reach;
// set to true when the state current state w is stacked, and
@ -93,39 +94,34 @@ namespace spot
// that a contributed to a contributed to a cycle.
bool mark;
// Deleted successors (in the paper, states deleted from A(x))
state_set del;
std::vector<bool> del;
// Predecessors of the current states, that could not yet
// contribute to a cycle.
state_set b;
std::vector<unsigned> b;
};
// Store the state_info for all visited states.
typedef std::unordered_map<const state*, state_info,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type tags_;
// A tagged_state s is a state* (s->first) associated to its
// state_info (s->second). We usually handle tagged_state in the
// algorithm to avoid repeated lookup of the state_info data.
typedef hash_type::iterator tagged_state;
// The automaton we are working on.
const_tgba_digraph_ptr aut_;
// Store the state_info for all visited states.
std::vector<state_info> info_;
// The SCC map built for aut_.
const scc_info& sm_;
// The DFS stack. Each entry contains a tagged state, an iterator
// on the transitions leaving that state, and a Boolean f
// indicating whether this state as already contributed to a cycle
// (f is updated when backtracking, so it should not be used by
// The DFS stack. Each entry contains a state, an iterator on the
// transitions leaving that state, and a Boolean f indicating
// whether this state as already contributed to a cycle (f is
// updated when backtracking, so it should not be used by
// cycle_found()).
struct dfs_entry
{
tagged_state ts;
tgba_succ_iterator* succ;
bool f;
unsigned s;
unsigned succ = 0U;
bool f = false;
dfs_entry(unsigned s): s(s)
{
}
};
typedef std::deque<dfs_entry> dfs_stack;
typedef std::vector<dfs_entry> dfs_stack;
dfs_stack dfs_;
public:
@ -155,18 +151,16 @@ namespace spot
///
/// This method method should return false iff no more cycles need
/// should be enumerated by run().
virtual bool cycle_found(const state* start);
virtual bool cycle_found(unsigned start);
private:
// introduce a new state to the tags map.
tagged_state tag_state(const state* s);
// add a new state to the dfs_ stack
void push_state(tagged_state ts);
void push_state(unsigned s);
// block the edge (x,y) because it cannot contribute to a new
// cycle currently (sub-procedure from the paper)
void nocycle(tagged_state x, tagged_state y);
void nocycle(unsigned x, unsigned y);
// unmark the state y (sub-procedure from the paper)
void unmark(tagged_state y);
void unmark(unsigned y);
};
}

10
src/tgbaalgos/isweakscc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -26,7 +26,7 @@ namespace spot
namespace
{
// Look for a non-accepting cycle.
class weak_checker: public enumerate_cycles
class weak_checker final : public enumerate_cycles
{
public:
bool result;
@ -37,14 +37,14 @@ namespace spot
}
virtual bool
cycle_found(const state* start)
cycle_found(unsigned start) override
{
dfs_stack::const_reverse_iterator i = dfs_.rbegin();
acc_cond::mark_t acc = 0U;
for (;;)
{
acc |= i->succ->current_acceptance_conditions();
if (i->ts->first == start)
acc |= aut_->trans_storage(i->succ).acc;
if (i->s == start)
break;
++i;
// The const cast is here to please old g++ versions.

18
src/tgbaalgos/powerset.cc
View file

@ -228,7 +228,7 @@ namespace spot
namespace
{
class fix_scc_acceptance: protected enumerate_cycles
class fix_scc_acceptance final: protected enumerate_cycles
{
public:
typedef dfs_stack::const_iterator cycle_iter;
@ -304,9 +304,7 @@ namespace spot
// Iterate on each original state corresponding to the
// start of the loop in the determinized automaton.
const power_map::power_state& ps =
refmap_.states_of(a->state_number(begin->ts->first));
for (auto s: ps)
for (auto s: refmap_.states_of(begin->s))
{
// Check the product between LOOP_A, and ORIG_A starting
// in S.
@ -330,22 +328,16 @@ namespace spot
}
virtual bool
cycle_found(const state* start)
cycle_found(unsigned start) override
{
cycle_iter i = dfs_.begin();
while (i->ts->first != start)
while (i->s != start)
++i;
trans_set ts;
bool is_acc = is_cycle_accepting(i, ts);
do
{
// std::cerr << aut_->format_state(i->ts->first) << ' ';
++i;
}
++i;
while (i != dfs_.end());
// std::cerr << " acc=" << is_acc << " (";
// bdd_print_accset(std::cerr, aut_->get_dict(), s) << ") ";
// print_set(std::cerr, ts) << '\n';
if (is_acc)
{
accept_.push_back(ts);