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_entry >	dfs_stack

Protected Attributes
const_twa_graph_ptr	aut_
std::vector< state_info >	info_
const scc_info &	sm_
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 [40] . (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_iterator 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:

• spot/twaalgos/cycles.hh