package incremental_cycles

  1. Overview
  2. Docs

Module type Incremental_cycles.Raw_graphSource

Signature for the graph data structure on which the algorithm operates. It is the input signature of the Make functor.

This corresponds to a standard imperative directed graph structure.

Additionally, extra meta-data is associated to each node, to hold internal data of the cycle detection algorithm. The meta-data is written and accessed by the algorithm through the corresponding set_* and get_* functions; it must not be modified otherwise.

The standard graph operations provided by Raw_graph are:

  • adding a new vertex;
  • adding a new edge between two existing vertices;
  • returning the list of successors of a vertex;
  • testing for equality of vertices.

The extra meta-data that Raw_graph must provide is:

  • Vertices can be marked, and it must be possible to generate fresh marks. Intuitively, a mark can be implemented as an integer, and generating a fresh mark as incrementing some mark counter.
  • Each vertex has an associated integer "level", which can be read and set.
  • Each vertex has an associated list of "incoming" vertices.
  • Each vertex has an associated "parent", which can be read and set to an other vertex of the graph.

No particular assumption should be made by the implementor of Raw_graph about the contents of these fields.

Types

type graph

The graph data structure that is modified by the operations below.

type vertex

The type of vertices of the graph.

type mark

The type of marks (each vertex has an associated mark).

Standard graph operations

NB: One must not call raw_add_edge and raw_add_vertex manually, as it would break the internal invariants of the cycle detection algorithm. One must use instead the safe wrappers add_vertex and add_edge_or_detect_cycle that are provided as output of the Incremental_cycles.Make functor.

val vertex_eq : vertex -> vertex -> bool

vertex_eq v1 v2 tests whether vertices v1 and v2 are equal.

val get_outgoing : graph -> vertex -> vertex list

get_outgoing g v returns the list of successors of v in the graph.

val raw_add_edge : graph -> vertex -> vertex -> unit

raw_add_edge g v w inserts a new (directed) arc between vertices v and w.

v and w must have been previously added to the graph using raw_add_vertex, and the arc v->w must not already be in the graph.

val raw_add_vertex : graph -> vertex -> unit

raw_add_vertex g v inserts a new vertex v into the graph.

  • The mark of a new vertex must be some "default mark" which is different from all marks that can be returned by new_mark.
  • The level (returned by get_level) of a new vertex must be 1.
  • The incoming vertices (returned by get_incoming) of a new vertex must be [] (the empty list).

Operations on graph meta-data

val new_mark : graph -> mark

new_mark g generates a fresh mark.

More specifically, this mark must be different from all the marks previously returned by new_mark g (on the same graph g). It must also be different from all the marks currently associated to vertices of the graph g.

val is_marked : graph -> vertex -> mark -> bool

is_marked g v m tests whether the vertex v has mark m.

NB: is_marked g v m can only hold if set_mark g v m has been called previously.

val set_mark : graph -> vertex -> mark -> unit

set_mark g v m sets the mark of vertex v to be m.

val get_level : graph -> vertex -> int

get_level g v returns the level of node v.

It is either the value previously set by set_level, or the default value for a newly created vertex (i.e. 1, see raw_add_vertex).

val set_level : graph -> vertex -> int -> unit

set_level g v l sets the level of node v to be l.

val get_incoming : graph -> vertex -> vertex list

get_incoming g v returns the list of "incoming" vertices of node v.

It corresponds to either the default value for a newly created vertex (i.e. the empty list, see raw_add_vertex), or the result of previous calls to clear_incoming and add_incoming.

val clear_incoming : graph -> vertex -> unit

clear_incoming g v sets the list of "incoming" vertices of v to be the empty list.

val add_incoming : graph -> vertex -> vertex -> unit

add_incoming g v w adds w to the list of "incoming" vertices of v.

val get_parent : graph -> vertex -> vertex

get_parent g v returns the "parent" of node v, as set by set_parent.

Note: there is no default value for get_parent. It is fine for get_parent g v to fail if it is called while set_parent g v w has not be called beforehand.

val set_parent : graph -> vertex -> vertex -> unit

set_parent g v w sets the "parent" of node v to be w.

Asymptotic complexity

All the operations provided by Raw_graph must run in constant time.