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

scc_info: make it possible to ignore or cut edges

Browse source 
* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Take
a filter function as optional argument.
* tests/core/sccif.cc, tests/core/sccif.test: New files.
* tests/Makefile.am, tests/core/.gitignore: Adjust.
* NEWS: Mention the new feature.
This commit is contained in:
Alexandre Duret-Lutz 2017-05-20 11:14:39 +02:00
parent 4da6a5cde1
commit 425620150a
7 changed files with 287 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

53
spot/twaalgos/sccinfo.cc
View file

@ -47,8 +47,12 @@ namespace spot
};
}
scc_info::scc_info(const_twa_graph_ptr aut)
: aut_(aut)
scc_info::scc_info(const_twa_graph_ptr aut,
unsigned initial_state,
edge_filter filter,
void* filter_data)
: aut_(aut), initial_state_(initial_state),
filter_(filter), filter_data_(filter_data)
{
unsigned n = aut->num_states();
sccof_.resize(n, -1U);
@ -74,10 +78,28 @@ namespace spot
std::stack<stack_item> todo_;
auto& gr = aut->get_graph();
std::deque<unsigned> init_states;
std::vector<bool> init_seen(n, false);
auto push_init = [&](unsigned s)
{
if (h_[s] != 0 || init_seen[s])
return;
init_seen[s] = true;
init_states.push_back(s);
};
// Setup depth-first search from the initial state. But we may
// have a conjunction of initial state in alternating automata.
for (unsigned init: aut->univ_dests(aut->get_init_state_number()))
if (initial_state_ == -1U)
initial_state_ = aut->get_init_state_number();
for (unsigned init: aut->univ_dests(initial_state_))
push_init(init);
while (!init_states.empty())
{
unsigned init = init_states.front();
init_states.pop_front();
int spi = h_[init];
if (spi > 0)
continue;
@ -133,6 +155,17 @@ namespace spot
for (auto& t: aut->out(s))
for (unsigned d: aut->univ_dests(t))
{
// If edges are cut, we are not able to
// maintain proper successor information.
if (filter_)
switch (filter_(t, d, filter_data_))
{
case edge_filter_choice::keep:
break;
case edge_filter_choice::ignore:
case edge_filter_choice::cut:
continue;
}
unsigned n = sccof_[d];
assert(n != -1U);
if (n == num)
@ -179,6 +212,7 @@ namespace spot
// We have a successor to look at.
// Fetch the values we are interested in...
auto& e = gr.edge_storage(tr_succ);
unsigned dest = e.dst;
if ((int) dest < 0)
{
@ -203,6 +237,19 @@ namespace spot
todo_.top().out_edge = e.next_succ;
}
// Do we really want to look at this
if (filter_)
switch (filter_(e, dest, filter_data_))
{
case edge_filter_choice::keep:
break;
case edge_filter_choice::ignore:
continue;
case edge_filter_choice::cut:
push_init(e.dst);
continue;
}
auto acc = e.acc;
// Are we going to a new state?

45
spot/twaalgos/sccinfo.hh
View file

@ -277,12 +277,45 @@ namespace spot
// support that yet.
typedef scc_info_node scc_node;
typedef scc_info_node::scc_succs scc_succs;
/// @{
/// \brief An edge_filter may be called on each edge to decide what
/// to do with it.
///
/// The edge filter is called with an edge and a destination. (In
/// existential automata the destination is already given by the
/// edge, but in alternating automata, one edge may have several
/// destinations, and in this case the filter will be called for
/// each destination.) The filter should return a value from
/// edge_filter_choice.
///
/// \c keep means to use the edge normally, as if no filter had
/// been given. \c ignore means to pretend the edge does not
/// exist (if the destination is only reachable through this edge,
/// it will not be visited). \c cut also ignores the edge, but
/// it remembers to visit the destination state (as if it were an
/// initial state) in case it is not reachable otherwise.
///
/// Note that successors between SCCs can only be maintained for
/// edges that are kept. If some edges are ignored or cut, the
/// SCC graph that you can explore with scc_info::initial() and
/// scc_info::succ() will be restricted to the portion reachable
/// with "keep" edges. Additionally SCCs might be created when
/// edges are cut, but those will not be reachable from
/// scc_info::initial()..
enum class edge_filter_choice { keep, ignore, cut };
typedef edge_filter_choice
(*edge_filter)(const twa_graph::edge_storage_t& e, unsigned dst,
void* filter_data);
/// @}
protected:
std::vector<unsigned> sccof_;
std::vector<scc_node> node_;
const_twa_graph_ptr aut_;
unsigned initial_state_;
edge_filter filter_;
void* filter_data_;
// Update the useful_ bits. Called automatically.
void determine_usefulness();
@ -293,7 +326,13 @@ namespace spot
}
public:
scc_info(const_twa_graph_ptr aut);
// Use ~0U instead of -1U to work around a bug in Swig.
// See https://github.com/swig/swig/issues/993
scc_info(const_twa_graph_ptr aut,
unsigned initial_state = ~0U,
edge_filter filter = nullptr,
void* filter_data = nullptr);
const_twa_graph_ptr get_aut() const
{
@ -389,8 +428,8 @@ namespace spot
/// \brief Get number of the SCC containing the initial state.
unsigned initial() const
{
SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number()));
return scc_count() - 1;
SPOT_ASSERT(filter_ || scc_count() - 1 == scc_of(initial_state_));
return scc_of(initial_state_);
}
const scc_succs& succ(unsigned scc) const