sccinfo: make it easier to iterate over all SCCs
* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: add scc_info::begin() and scc_info::end() methods to iterate over the node_ vector. Tidy the scc_node structure that that its member are accessed via methods. * src/tgbaalgos/safety.cc, src/bin/ltlcross.cc: Simplify using this interface.
This commit is contained in:
Alexandre Duret-Lutz
parent
579e8fc0a9
commit
e01ab2b236
4 changed files with 114 additions and 67 deletions
|
|
@ -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.
|
||||
|
|
@ -1186,9 +1186,8 @@ namespace
|
|||
{
|
||||
// r == true iff the automaton i is accepting.
|
||||
bool r = false;
|
||||
unsigned c = m->scc_count();
|
||||
for (unsigned j = 0; j < c; ++j)
|
||||
if (m->is_accepting_scc(j))
|
||||
for (auto& scc: *m)
|
||||
if (scc.is_accepting())
|
||||
{
|
||||
r = true;
|
||||
break;
|
||||
|
|
@ -1240,15 +1239,13 @@ namespace
|
|||
// Collect all the states of SSPACE that appear in the accepting SCCs
|
||||
// of PROD. (Trivial SCCs are considered accepting.)
|
||||
static void
|
||||
states_in_acc(const spot::scc_info* m,
|
||||
state_set& s)
|
||||
states_in_acc(const spot::scc_info* m, state_set& s)
|
||||
{
|
||||
auto aut = m->get_aut();
|
||||
auto ps = aut->get_named_prop<const spot::product_states>("product-states");
|
||||
unsigned c = m->scc_count();
|
||||
for (unsigned n = 0; n < c; ++n)
|
||||
if (m->is_accepting_scc(n) || m->is_trivial(n))
|
||||
for (auto i: m->states_of(n))
|
||||
for (auto& scc: *m)
|
||||
if (scc.is_accepting() || scc.is_trivial())
|
||||
for (auto i: scc.states())
|
||||
// Get the projection on sspace.
|
||||
s.insert((*ps)[i].second);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2010, 2011, 2013, 2014 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE)
|
||||
// Copyright (C) 2010, 2011, 2013, 2014, 2015 Laboratoire de Recherche
|
||||
// et Développement de l'Epita (LRDE)
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -25,22 +25,21 @@ namespace spot
|
|||
{
|
||||
bool
|
||||
is_guarantee_automaton(const const_tgba_digraph_ptr& aut,
|
||||
const scc_info* sm)
|
||||
const scc_info* si)
|
||||
{
|
||||
// Create an scc_info if the user did not give one to us.
|
||||
bool need_sm = !sm;
|
||||
if (need_sm)
|
||||
sm = new scc_info(aut);
|
||||
bool need_si = !si;
|
||||
if (need_si)
|
||||
si = new scc_info(aut);
|
||||
|
||||
bool result = true;
|
||||
|
||||
unsigned scc_count = sm->scc_count();
|
||||
for (unsigned scc = 0; scc < scc_count; ++scc)
|
||||
for (auto& scc: *si)
|
||||
{
|
||||
if (!sm->is_accepting_scc(scc))
|
||||
if (!scc.is_accepting())
|
||||
continue;
|
||||
// Accepting SCCs should have only one state.
|
||||
auto& st = sm->states_of(scc);
|
||||
auto& st = scc.states();
|
||||
if (st.size() != 1)
|
||||
{
|
||||
result = false;
|
||||
|
|
@ -58,8 +57,8 @@ namespace spot
|
|||
break;
|
||||
}
|
||||
|
||||
if (need_sm)
|
||||
delete sm;
|
||||
if (need_si)
|
||||
delete si;
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||
// de l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -100,7 +100,7 @@ namespace spot
|
|||
// Fill STATES with any state removed, so that
|
||||
// remove_component() does not have to traverse the SCC
|
||||
// again.
|
||||
root_.front().node.states.push_front(curr);
|
||||
root_.front().node.states_.push_front(curr);
|
||||
|
||||
// When backtracking the root of an SCC, we must also
|
||||
// remove that SCC from the ARC/ROOT stacks. We must
|
||||
|
|
@ -109,23 +109,23 @@ namespace spot
|
|||
if (root_.front().index == h_[curr])
|
||||
{
|
||||
int num = node_.size();
|
||||
for (auto s: root_.front().node.states)
|
||||
for (auto s: root_.front().node.states_)
|
||||
{
|
||||
sccof_[s] = num;
|
||||
h_[s] = num + 1;
|
||||
}
|
||||
bdd cond = root_.front().in_cond;
|
||||
auto acc = root_.front().node.acc;
|
||||
bool triv = root_.front().node.trivial;
|
||||
auto acc = root_.front().node.acc_marks();
|
||||
bool triv = root_.front().node.is_trivial();
|
||||
node_.emplace_back(acc, triv);
|
||||
std::swap(node_.back().succ, root_.front().node.succ);
|
||||
std::swap(node_.back().states, root_.front().node.states);
|
||||
node_.back().accepting = !triv && aut->acc().accepting(acc);
|
||||
std::swap(node_.back().succ_, root_.front().node.succ_);
|
||||
std::swap(node_.back().states_, root_.front().node.states_);
|
||||
node_.back().accepting_ = !triv && aut->acc().accepting(acc);
|
||||
root_.pop_front();
|
||||
// Record the transition between the SCC being popped
|
||||
// and the previous SCC.
|
||||
if (!root_.empty())
|
||||
root_.front().node.succ.emplace_back(cond, num);
|
||||
root_.front().node.succ_.emplace_back(cond, num);
|
||||
}
|
||||
continue;
|
||||
}
|
||||
|
|
@ -159,7 +159,7 @@ namespace spot
|
|||
--spi;
|
||||
// Record that there is a transition from this SCC to the
|
||||
// dest SCC labelled with cond.
|
||||
auto& succ = root_.front().node.succ;
|
||||
auto& succ = root_.front().node.succ_;
|
||||
scc_succs::iterator i = std::find_if(succ.begin(), succ.end(),
|
||||
[spi](const scc_trans& x) {
|
||||
return (x.dst ==
|
||||
|
|
@ -189,13 +189,13 @@ namespace spot
|
|||
while (threshold > root_.front().index)
|
||||
{
|
||||
assert(!root_.empty());
|
||||
acc |= root_.front().node.acc;
|
||||
acc |= root_.front().node.acc_;
|
||||
acc |= root_.front().in_acc;
|
||||
states.splice(states.end(), root_.front().node.states);
|
||||
states.splice(states.end(), root_.front().node.states_);
|
||||
|
||||
succs.insert(succs.end(),
|
||||
root_.front().node.succ.begin(),
|
||||
root_.front().node.succ.end());
|
||||
root_.front().node.succ_.begin(),
|
||||
root_.front().node.succ_.end());
|
||||
root_.pop_front();
|
||||
}
|
||||
|
||||
|
|
@ -206,24 +206,31 @@ namespace spot
|
|||
|
||||
// Accumulate all acceptance conditions, states, SCC
|
||||
// successors, and conditions into the merged SCC.
|
||||
root_.front().node.acc |= acc;
|
||||
root_.front().node.states.splice(root_.front().node.states.end(),
|
||||
root_.front().node.acc_ |= acc;
|
||||
root_.front().node.states_.splice(root_.front().node.states_.end(),
|
||||
states);
|
||||
root_.front().node.succ.insert(root_.front().node.succ.end(),
|
||||
root_.front().node.succ_.insert(root_.front().node.succ_.end(),
|
||||
succs.begin(), succs.end());
|
||||
// This SCC is no longer trivial.
|
||||
root_.front().node.trivial = false;
|
||||
root_.front().node.trivial_ = false;
|
||||
}
|
||||
|
||||
// An SCC is useful if it is accepting or it has a successor SCC
|
||||
// that is useful.
|
||||
unsigned scccount = scc_count();
|
||||
for (unsigned i = 0; i < scccount; i++)
|
||||
for (unsigned i = 0; i < scccount; ++i)
|
||||
{
|
||||
bool useful = node_[i].accepting;
|
||||
for (auto j: node_[i].succ)
|
||||
useful |= node_[j.dst].useful;
|
||||
node_[i].useful = useful;
|
||||
if (node_[i].is_accepting())
|
||||
{
|
||||
node_[i].useful_ = true;
|
||||
continue;
|
||||
}
|
||||
for (auto j: node_[i].succ())
|
||||
if (node_[j.dst].is_useful())
|
||||
{
|
||||
node_[i].useful_ = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
|
||||
// de l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -25,7 +25,6 @@
|
|||
|
||||
namespace spot
|
||||
{
|
||||
|
||||
class SPOT_API scc_info
|
||||
{
|
||||
public:
|
||||
|
|
@ -41,24 +40,56 @@ namespace spot
|
|||
|
||||
typedef std::vector<scc_trans> scc_succs;
|
||||
|
||||
struct scc_node
|
||||
class scc_node
|
||||
{
|
||||
friend class scc_info;
|
||||
protected:
|
||||
scc_succs succ_;
|
||||
acc_cond::mark_t acc_;
|
||||
std::list<unsigned> states_; // States of the component
|
||||
bool trivial_:1;
|
||||
bool accepting_:1;
|
||||
bool useful_:1;
|
||||
public:
|
||||
scc_node():
|
||||
acc(0U), trivial(true), accepting(false), useful(false)
|
||||
acc_(0U), trivial_(true), accepting_(false), useful_(false)
|
||||
{
|
||||
}
|
||||
|
||||
scc_node(acc_cond::mark_t acc, bool trivial):
|
||||
acc(acc), trivial(trivial), accepting(false), useful(false)
|
||||
acc_(acc), trivial_(trivial), accepting_(false), useful_(false)
|
||||
{
|
||||
}
|
||||
|
||||
scc_succs succ;
|
||||
acc_cond::mark_t acc;
|
||||
std::list<unsigned> states; // States of the component
|
||||
bool trivial:1;
|
||||
bool accepting:1;
|
||||
bool useful:1;
|
||||
bool is_trivial() const
|
||||
{
|
||||
return trivial_;
|
||||
}
|
||||
|
||||
bool is_accepting() const
|
||||
{
|
||||
return accepting_;
|
||||
}
|
||||
|
||||
bool is_useful() const
|
||||
{
|
||||
return useful_;
|
||||
}
|
||||
|
||||
acc_cond::mark_t acc_marks() const
|
||||
{
|
||||
return acc_;
|
||||
}
|
||||
|
||||
const std::list<unsigned>& states() const
|
||||
{
|
||||
return states_;
|
||||
}
|
||||
|
||||
const scc_succs& succ() const
|
||||
{
|
||||
return succ_;
|
||||
}
|
||||
};
|
||||
|
||||
protected:
|
||||
|
|
@ -98,9 +129,22 @@ namespace spot
|
|||
return sccof_[st];
|
||||
}
|
||||
|
||||
auto begin() const
|
||||
SPOT_RETURN(node_.begin());
|
||||
auto end() const
|
||||
SPOT_RETURN(node_.end());
|
||||
auto cbegin() const
|
||||
SPOT_RETURN(node_.cbegin());
|
||||
auto cend() const
|
||||
SPOT_RETURN(node_.cend());
|
||||
auto rbegin() const
|
||||
SPOT_RETURN(node_.rbegin());
|
||||
auto rend() const
|
||||
SPOT_RETURN(node_.rend());
|
||||
|
||||
const std::list<unsigned>& states_of(unsigned scc) const
|
||||
{
|
||||
return node(scc).states;
|
||||
return node(scc).states();
|
||||
}
|
||||
|
||||
unsigned one_state_of(unsigned scc) const
|
||||
|
|
@ -117,32 +161,32 @@ namespace spot
|
|||
|
||||
const scc_succs& succ(unsigned scc) const
|
||||
{
|
||||
return node(scc).succ;
|
||||
return node(scc).succ();
|
||||
}
|
||||
|
||||
bool is_trivial(unsigned scc) const
|
||||
{
|
||||
return node(scc).trivial;
|
||||
return node(scc).is_trivial();
|
||||
}
|
||||
|
||||
acc_cond::mark_t acc(unsigned scc) const
|
||||
{
|
||||
return node(scc).acc;
|
||||
return node(scc).acc_marks();
|
||||
}
|
||||
|
||||
bool is_accepting_scc(unsigned scc) const
|
||||
{
|
||||
return node(scc).accepting;
|
||||
return node(scc).is_accepting();
|
||||
}
|
||||
|
||||
bool is_useful_scc(unsigned scc) const
|
||||
{
|
||||
return node(scc).useful;
|
||||
return node(scc).is_useful();
|
||||
}
|
||||
|
||||
bool is_useful_state(unsigned st) const
|
||||
{
|
||||
return reachable_state(st) && node(scc_of(st)).useful;
|
||||
return reachable_state(st) && node(scc_of(st)).is_useful();
|
||||
}
|
||||
|
||||
/// \brief Return the set of all used acceptance combinations, for
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue