graph: let transitions() iterate only on valid transitions
This fixes #6. * src/graph/graph.hh: Rename the old transitions() as transition_vector(), and implement a new transitions() that iterates only on non-dead transitions. * src/tgba/tgbagraph.hh, src/tgba/tgbagraph.cc, src/graph/ngraph.hh: Adjust wrappers. * src/hoaparse/hoaparse.yy, src/tgbaalgos/complete.cc, src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc, src/tgbaalgos/randomize.cc, src/tgbaalgos/safety.cc: Adjust calls.
This commit is contained in:
parent
8014833ae3
commit
fbbf584bbb
10 changed files with 147 additions and 17 deletions
|
|
@ -373,8 +373,121 @@ namespace spot
|
||||||
transition t_;
|
transition t_;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
//////////////////////////////////////////////////
|
||||||
|
// all_trans
|
||||||
|
//////////////////////////////////////////////////
|
||||||
|
|
||||||
|
template <typename Graph>
|
||||||
|
class SPOT_API all_trans_iterator:
|
||||||
|
std::iterator<std::forward_iterator_tag,
|
||||||
|
typename
|
||||||
|
std::conditional<std::is_const<Graph>::value,
|
||||||
|
const typename Graph::trans_storage_t,
|
||||||
|
typename Graph::trans_storage_t>::type>
|
||||||
|
{
|
||||||
|
typedef
|
||||||
|
std::iterator<std::forward_iterator_tag,
|
||||||
|
typename
|
||||||
|
std::conditional<std::is_const<Graph>::value,
|
||||||
|
const typename Graph::trans_storage_t,
|
||||||
|
typename Graph::trans_storage_t>::type>
|
||||||
|
super;
|
||||||
|
|
||||||
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||||
|
const typename Graph::trans_vector,
|
||||||
|
typename Graph::trans_vector>::type
|
||||||
|
tv_t;
|
||||||
|
|
||||||
|
unsigned t_;
|
||||||
|
tv_t& tv_;
|
||||||
|
|
||||||
|
void skip_()
|
||||||
|
{
|
||||||
|
unsigned s = tv_.size();
|
||||||
|
do
|
||||||
|
++t_;
|
||||||
|
while (t_ < s && tv_[t_].next_succ == t_);
|
||||||
|
}
|
||||||
|
|
||||||
|
public:
|
||||||
|
all_trans_iterator(unsigned pos, tv_t& tv)
|
||||||
|
: t_(pos), tv_(tv)
|
||||||
|
{
|
||||||
|
skip_();
|
||||||
|
}
|
||||||
|
|
||||||
|
all_trans_iterator(tv_t& tv)
|
||||||
|
: t_(tv.size()), tv_(tv)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
all_trans_iterator& operator++()
|
||||||
|
{
|
||||||
|
skip_();
|
||||||
|
return *this;
|
||||||
|
}
|
||||||
|
|
||||||
|
all_trans_iterator operator++(int)
|
||||||
|
{
|
||||||
|
all_trans_iterator old = *this;
|
||||||
|
++*this;
|
||||||
|
return old;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator==(all_trans_iterator o) const
|
||||||
|
{
|
||||||
|
return t_ == o.t_;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool operator!=(all_trans_iterator o) const
|
||||||
|
{
|
||||||
|
return t_ != o.t_;
|
||||||
|
}
|
||||||
|
|
||||||
|
typename super::reference
|
||||||
|
operator*()
|
||||||
|
{
|
||||||
|
return tv_[t_];
|
||||||
|
}
|
||||||
|
|
||||||
|
typename super::pointer
|
||||||
|
operator->()
|
||||||
|
{
|
||||||
|
return &tv_[t_];
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
template <typename Graph>
|
||||||
|
class SPOT_API all_trans
|
||||||
|
{
|
||||||
|
typedef typename std::conditional<std::is_const<Graph>::value,
|
||||||
|
const typename Graph::trans_vector,
|
||||||
|
typename Graph::trans_vector>::type
|
||||||
|
tv_t;
|
||||||
|
typedef all_trans_iterator<Graph> iter_t;
|
||||||
|
tv_t& tv_;
|
||||||
|
public:
|
||||||
|
|
||||||
|
all_trans(tv_t& tv)
|
||||||
|
: tv_(tv)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
iter_t begin()
|
||||||
|
{
|
||||||
|
return {0, tv_};
|
||||||
|
}
|
||||||
|
|
||||||
|
iter_t end()
|
||||||
|
{
|
||||||
|
return {tv_};
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// The actual graph implementation
|
// The actual graph implementation
|
||||||
|
|
||||||
template <typename State_Data, typename Trans_Data, bool Alternating>
|
template <typename State_Data, typename Trans_Data, bool Alternating>
|
||||||
|
|
@ -614,12 +727,27 @@ namespace spot
|
||||||
return states_;
|
return states_;
|
||||||
}
|
}
|
||||||
|
|
||||||
const trans_vector& transitions() const
|
internal::all_trans<const digraph> transitions() const
|
||||||
{
|
{
|
||||||
return transitions_;
|
return transitions_;
|
||||||
}
|
}
|
||||||
|
|
||||||
trans_vector& transitions()
|
internal::all_trans<digraph> transitions()
|
||||||
|
{
|
||||||
|
return transitions_;
|
||||||
|
}
|
||||||
|
|
||||||
|
// When using this method, beware that the first entry (transition
|
||||||
|
// #0) is not a real transition, and that any transition with
|
||||||
|
// next_succ pointing to itself is an erased transition.
|
||||||
|
//
|
||||||
|
// You should probably use transitions() instead.
|
||||||
|
const trans_vector& transition_vector() const
|
||||||
|
{
|
||||||
|
return transitions_;
|
||||||
|
}
|
||||||
|
|
||||||
|
trans_vector& transition_vector()
|
||||||
{
|
{
|
||||||
return transitions_;
|
return transitions_;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -91,7 +91,7 @@ namespace spot
|
||||||
auto old = p.first->second;
|
auto old = p.first->second;
|
||||||
p.first->second = s;
|
p.first->second = s;
|
||||||
// Add the successor of OLD to those of S.
|
// Add the successor of OLD to those of S.
|
||||||
auto& trans = g_.transitions();
|
auto& trans = g_.transition_vector();
|
||||||
auto& states = g_.states();
|
auto& states = g_.states();
|
||||||
trans[states[s].succ_tail].next_succ = states[old].succ;
|
trans[states[s].succ_tail].next_succ = states[old].succ;
|
||||||
states[s].succ_tail = states[old].succ_tail;
|
states[s].succ_tail = states[old].succ_tail;
|
||||||
|
|
|
||||||
|
|
@ -953,7 +953,7 @@ static void fix_acceptance(result_& r)
|
||||||
// If a set x appears only as Inf(!x), we can complement it so that
|
// If a set x appears only as Inf(!x), we can complement it so that
|
||||||
// we work with Inf(x) instead.
|
// we work with Inf(x) instead.
|
||||||
auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
|
auto onlyneg = r.neg_acc_sets - r.pos_acc_sets;
|
||||||
for (auto& t: r.h->aut->transitions())
|
for (auto& t: r.h->aut->transition_vector())
|
||||||
t.acc ^= onlyneg;
|
t.acc ^= onlyneg;
|
||||||
|
|
||||||
// However if set x is used elsewhere, for instance in
|
// However if set x is used elsewhere, for instance in
|
||||||
|
|
@ -968,7 +968,7 @@ static void fix_acceptance(result_& r)
|
||||||
auto v = acc.sets(both);
|
auto v = acc.sets(both);
|
||||||
auto vs = v.size();
|
auto vs = v.size();
|
||||||
unsigned base = acc.add_sets(vs);
|
unsigned base = acc.add_sets(vs);
|
||||||
for (auto& t: r.h->aut->transitions())
|
for (auto& t: r.h->aut->transition_vector())
|
||||||
if ((t.acc & both) != both)
|
if ((t.acc & both) != both)
|
||||||
for (unsigned i = 0; i < vs; ++i)
|
for (unsigned i = 0; i < vs; ++i)
|
||||||
if (!t.acc.has(i))
|
if (!t.acc.has(i))
|
||||||
|
|
|
||||||
|
|
@ -43,7 +43,7 @@ namespace spot
|
||||||
// them.
|
// them.
|
||||||
});
|
});
|
||||||
|
|
||||||
auto& trans = this->transitions();
|
auto& trans = this->transition_vector();
|
||||||
unsigned tend = trans.size();
|
unsigned tend = trans.size();
|
||||||
unsigned out = 0;
|
unsigned out = 0;
|
||||||
unsigned in = 1;
|
unsigned in = 1;
|
||||||
|
|
|
||||||
|
|
@ -405,6 +405,11 @@ namespace spot
|
||||||
auto transitions()
|
auto transitions()
|
||||||
SPOT_RETURN(g_.transitions());
|
SPOT_RETURN(g_.transitions());
|
||||||
|
|
||||||
|
auto transition_vector() const
|
||||||
|
SPOT_RETURN(g_.transition_vector());
|
||||||
|
auto transition_vector()
|
||||||
|
SPOT_RETURN(g_.transition_vector());
|
||||||
|
|
||||||
auto is_dead_transition(const graph_t::trans_storage_t& t) const
|
auto is_dead_transition(const graph_t::trans_storage_t& t) const
|
||||||
SPOT_RETURN(g_.is_dead_transition(t));
|
SPOT_RETURN(g_.is_dead_transition(t));
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -32,7 +32,7 @@ namespace spot
|
||||||
// acceptance set as the added sink would become accepting.
|
// acceptance set as the added sink would become accepting.
|
||||||
// In this case, add an acceptance set to all transitions.
|
// In this case, add an acceptance set to all transitions.
|
||||||
allacc = aut->set_single_acceptance_set();
|
allacc = aut->set_single_acceptance_set();
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->transition_vector())
|
||||||
t.acc = allacc;
|
t.acc = allacc;
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
|
|
|
||||||
|
|
@ -303,8 +303,7 @@ namespace spot
|
||||||
// Compute the AP used in the hard way.
|
// Compute the AP used in the hard way.
|
||||||
bdd ap = bddtrue;
|
bdd ap = bddtrue;
|
||||||
for (auto& t: ref->transitions())
|
for (auto& t: ref->transitions())
|
||||||
if (!ref->is_dead_transition(t))
|
ap &= bdd_support(t.cond);
|
||||||
ap &= bdd_support(t.cond);
|
|
||||||
|
|
||||||
// Count the number of atomic propositions
|
// Count the number of atomic propositions
|
||||||
int nap = 0;
|
int nap = 0;
|
||||||
|
|
|
||||||
|
|
@ -432,8 +432,7 @@ namespace spot
|
||||||
// Compute the AP used in the hard way.
|
// Compute the AP used in the hard way.
|
||||||
bdd ap = bddtrue;
|
bdd ap = bddtrue;
|
||||||
for (auto& t: ref->transitions())
|
for (auto& t: ref->transitions())
|
||||||
if (!ref->is_dead_transition(t))
|
ap &= bdd_support(t.cond);
|
||||||
ap &= bdd_support(t.cond);
|
|
||||||
|
|
||||||
// Count the number of atomic propositions
|
// Count the number of atomic propositions
|
||||||
int nap = 0;
|
int nap = 0;
|
||||||
|
|
|
||||||
|
|
@ -42,9 +42,9 @@ namespace spot
|
||||||
}
|
}
|
||||||
if (randomize_transitions)
|
if (randomize_transitions)
|
||||||
{
|
{
|
||||||
auto begin = g.transitions().begin() + 1;
|
g.remove_dead_transitions_();
|
||||||
auto end = g.transitions().end();
|
auto& v = g.transition_vector();
|
||||||
std::random_shuffle(begin, end, spot::mrand);
|
std::random_shuffle(v.begin() + 1, v.end(), spot::mrand);
|
||||||
}
|
}
|
||||||
|
|
||||||
typedef tgba_digraph::graph_t::trans_storage_t tr_t;
|
typedef tgba_digraph::graph_t::trans_storage_t tr_t;
|
||||||
|
|
|
||||||
|
|
@ -66,9 +66,8 @@ namespace spot
|
||||||
bool is_safety_mwdba(const const_tgba_digraph_ptr& aut)
|
bool is_safety_mwdba(const const_tgba_digraph_ptr& aut)
|
||||||
{
|
{
|
||||||
for (auto& t: aut->transitions())
|
for (auto& t: aut->transitions())
|
||||||
if (!aut->is_dead_transition(t))
|
if (!aut->acc().accepting(t.acc))
|
||||||
if (!aut->acc().accepting(t.acc))
|
return false;
|
||||||
return false;
|
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue