spot  2.11.6
Classes | Public Member Functions | Protected Types | Protected Attributes | List of all members
spot::enumerate_cycles Class Reference

Enumerate elementary cycles in a SCC. More...

#include <spot/twaalgos/cycles.hh>

Collaboration diagram for spot::enumerate_cycles:

Classes

struct  dfs_entry
 
struct  state_info
 

Public Member Functions

 enumerate_cycles (const scc_info &map)
 
void run (unsigned scc)
 Run in SCC scc, and call cycle_found() for any new elementary cycle found. More...
 
virtual bool cycle_found (unsigned start)
 Called whenever a cycle was found. More...
 

Protected Types

typedef std::vector< dfs_entrydfs_stack
 

Protected Attributes

const_twa_graph_ptr aut_
 
std::vector< state_infoinfo_
 
const scc_infosm_
 
dfs_stack dfs_
 

Detailed Description

Enumerate elementary cycles in a SCC.

This class implements a non-recursive version of the algorithm on page 170 of [37] . (the additional preprocessings described later in that paper are not implemented).

It should be noted that although the above paper does not consider multiple arcs and self-loops in its definitions, the algorithm they present works as expected in these cases.

For our purpose an elementary cycle is a sequence of transitions that form a cycle and that visit a state at most once. We may have two cycles that visit the same states in the same order if some pair of states are connected by several transitions. Also A cycle may visit only one state if it is a self-loop.

We represent a cycle by a sequence of succ_iterator objects positioned on the transition contributing to the cycle. These succ_itertor are stored, along with their source state, in the dfs_ stack. Only the last portion of this stack may form a cycle.

Calling run(n) will enumerate all elementary cycles in SCC n. Each time an SCC is found, the method cycle_found(s) is called with the initial state s of the cycle: the cycle is constituted from all the states that are on the dfs_ stack after s (including s).

You should inherit from this class and redefine the cycle_found() method to perform any work you would like to do on the enumerated cycles. If cycle_found() returns false, the run() method will terminate. If it returns true, the run() method will search for the next elementary cycle and call cycle_found() again if it finds another cycle.

Member Function Documentation

◆ cycle_found()

virtual bool spot::enumerate_cycles::cycle_found ( unsigned  start)
virtual

Called whenever a cycle was found.

The cycle uses all the states from the dfs stack, starting from the one labeled start. The iterators in the DFS stack are all pointing to the transition considered for the cycle.

This method is not const so you can modify private variables to your subclass, but it should definitely NOT modify the dfs stack or the tags map.

The default implementation, not very useful, will print the states in the cycle on std::cout.

This method method should return false iff no more cycles need should be enumerated by run().

◆ run()

void spot::enumerate_cycles::run ( unsigned  scc)

Run in SCC scc, and call cycle_found() for any new elementary cycle found.

It is safe to call this method multiple times, for instance to enumerate the cycle of each SCC.


The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1