Agda.Utils.Graph.AdjacencyMap.Unidirectional

Directed graphs (can of course simulate undirected graphs).

Represented as adjacency maps in direction from source to target.

Each source node maps to a adjacency map of outgoing edges, which is a map from target nodes to edges.

This allows to get outgoing edges in O(log n) time where n is the number of nodes in the graph.

Documentation

newtype Graph s t e

Graph s t e is a directed graph with source nodes in s target nodes in t and edges in e.

Admits at most one edge between any two nodes. Several edges can be modeled by using a collection type for e.

Represented as "adjacency list", or rather, adjacency map. This allows to get all outgoing edges for a node in O(log n) time where n is the number of nodes of the graph.

Constructors

Graph

Fields

graph :: Map s (Map t e)

Forward edges.

Instances

(Ord r, Ord f) => SetToInfty f (ConGraph r f)

Functor (Graph s t)

(Eq s, Eq t, Eq e) => Eq (Graph s t e)

(Show s, Show t, Show e) => Show (Graph s t e)

(Ord n, SemiRing e, Arbitrary n, Arbitrary e) => Arbitrary (Graph n n e)

(Ord r, Ord f, Negative a) => Negative (Graphs r f a)

(Ord r, Ord f, Negative a) => Negative (Graph r f a)

A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

data Edge s t e

Constructors

Edge

Fields

source :: s

Outgoing node.

target :: t

Incoming node.

label :: e

Edge label (weight).

Instances

Eq f => SetToInfty f (Edge' r f a)

Functor (Edge s t)

(Eq s, Eq t, Eq e) => Eq (Edge s t e)

(Ord s, Ord t, Ord e) => Ord (Edge s t e)

(Show s, Show t, Show e) => Show (Edge s t e)

(CoArbitrary s, CoArbitrary t, CoArbitrary e) => CoArbitrary (Edge s t e)

(Arbitrary s, Arbitrary t, Arbitrary e) => Arbitrary (Edge s t e)

(Show r, Show f, Show a, Ord r, Ord f, Dioid a) => Dioid (Edge' r f a)

(Show r, Show f, Show a, Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a)

(Ord r, Ord f, Top a) => Top (Edge' r f a)

Negative a => Negative (Edge' r f a)

An edge is negative if its label is.

transposeEdge :: Edge s t e -> Edge t s e

Reverse an edge.

edges :: (Ord s, Ord t) => Graph s t e -> [Edge s t e]

Turn a graph into a list of edges. O(n + e)

edgesFrom :: (Ord s, Ord t) => Graph s t e -> [s] -> [Edge s t e]

All edges originating in the given nodes. (I.e., all outgoing edges for the given nodes.)

Roughly linear in the length of the result list O(result).

edgesTo :: (Ord s, Ord t) => Graph s t e -> [t] -> [Edge s t e]

All edges ending in the given nodes. (I.e., all incoming edges for the given nodes.)

Expensive: O(n * |ts| * log n).

diagonal :: Ord n => Graph n n e -> [Edge n n e]

Get all self-loops.

lookup :: (Ord s, Ord t) => s -> t -> Graph s t e -> Maybe e

Lookup label of an edge.

neighbours :: (Ord s, Ord t) => s -> Graph s t e -> [(t, e)]

Get a list of outgoing edges with target.

sourceNodes :: (Ord s, Ord t) => Graph s t e -> Set s

Returns all the nodes with outgoing edges. O(n).

targetNodes :: (Ord s, Ord t) => Graph s t e -> Set t

Returns all the nodes with incoming edges. Expensive! O(e).

data Nodes n

For homogeneous graphs, (s = t) we can compute a set of all nodes.

Structure Nodes is for computing all nodes but also remembering which were incoming and which outgoing. This is mostly for efficiency reasons, to avoid recomputation when all three sets are needed.

Constructors

Nodes

Fields

srcNodes :: Set n

tgtNodes :: Set n

allNodes :: Set n

computeNodes :: Ord n => Graph n n e -> Nodes n

nodes :: Ord n => Graph n n e -> Set n

The set of all nodes (outgoing and incoming).

fromNodes :: Ord n => [n] -> Graph n n e

Constructs a completely disconnected graph containing the given nodes. O(n).

fromList :: (Ord s, Ord t) => [Edge s t e] -> Graph s t e

Constructs a graph from a list of edges. O(e log n)

Later edges overwrite earlier edges.

fromListWith :: (Ord s, Ord t) => (e -> e -> e) -> [Edge s t e] -> Graph s t e

Constructs a graph from a list of edges. O(e log n)

Later edges are combined with earlier edges using the supplied function.

toList :: (Ord s, Ord t) => Graph s t e -> [Edge s t e]

Convert a graph into a list of edges. O(e)

empty :: Graph s t e

Empty graph (no nodes, no edges).

singleton :: (Ord s, Ord t) => s -> t -> e -> Graph s t e

A graph with two nodes and a single connecting edge.

insert :: (Ord s, Ord t) => s -> t -> e -> Graph s t e -> Graph s t e

Insert an edge into the graph.

insertWith :: (Ord s, Ord t) => (e -> e -> e) -> s -> t -> e -> Graph s t e -> Graph s t e

Insert an edge, possibly combining old edge weight with new weight by given function f into f new old.

insertEdge :: (Ord s, Ord t) => Edge s t e -> Graph s t e -> Graph s t e

insertEdgeWith :: (Ord s, Ord t) => (e -> e -> e) -> Edge s t e -> Graph s t e -> Graph s t e

union :: (Ord s, Ord t) => Graph s t e -> Graph s t e -> Graph s t e

Left-biased union.

unionWith :: (Ord s, Ord t) => (e -> e -> e) -> Graph s t e -> Graph s t e -> Graph s t e

unions :: (Ord s, Ord t) => [Graph s t e] -> Graph s t e

unionsWith :: (Ord s, Ord t) => (e -> e -> e) -> [Graph s t e] -> Graph s t e

removeNode :: Ord n => n -> Graph n n e -> Graph n n e

Removes the given node, be it source or target, and all corresponding edges, from the graph.

Expensive! O(n log n).

removeEdge :: (Ord s, Ord t) => s -> t -> Graph s t e -> Graph s t e

removeEdge s t g removes the edge going from s to t, if any.

O((log n)^2).

filterEdges :: (Ord s, Ord t) => (e -> Bool) -> Graph s t e -> Graph s t e

Keep only the edges that satisfy the predicate. O(e).

unzip :: Graph s t (e, e') -> (Graph s t e, Graph s t e')

Unzipping a graph (naive implementation using fmap).

sccs' :: Ord n => Graph n n e -> [SCC n]

The graph's strongly connected components, in reverse topological order.

sccs :: Ord n => Graph n n e -> [[n]]

The graph's strongly connected components, in reverse topological order.

acyclic :: Ord n => Graph n n e -> Bool

Returns True iff the graph is acyclic.

composeWith :: (Ord s, Ord t, Ord u) => (c -> d -> e) -> (e -> e -> e) -> Graph s t c -> Graph t u d -> Graph s u e

composeWith times plus g g' finds all edges s --c_i--> t_i --d_i--> u and constructs the result graph from edge(s,u) = sum_i (c_i times d_i).

Complexity: for each edge s --> t in g we lookup up all edges starting in with t in g'.

transitiveClosure1 :: (Eq e, SemiRing e, Ord n) => Graph n n e -> Graph n n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on the entire graph at once.

transitiveClosure :: (Eq e, SemiRing e, Ord n) => Graph n n e -> Graph n n e

Computes the transitive closure of the graph.

Note that this algorithm is not guaranteed to be correct (or terminate) for arbitrary semirings.

This function operates on one strongly connected component (SCC) at a time.

For each SCC, it uses a saturation algorithm on state (g, es) where initially es is the set of edges of the SCC and g the graph. The algorithm finishes if es has not changed in an iteration. At each step, all es are composed with g, the resulting new graphs are unioned with g. The new es is then computed as the edges of the SCC in the new g.

findPath :: (SemiRing e, Ord n) => (e -> Bool) -> n -> n -> Graph n n e -> Maybe e

Find a path from a source node to a target node.

The path must satisfy the given predicate good :: e -> Bool.

allPaths :: (SemiRing e, Ord n, Ord c) => (e -> c) -> n -> n -> Graph n n e -> [e]

allPaths classify a b g returns a list of pathes (accumulated edge weights) from node a to node b in g. Alternative intermediate pathes are only considered if they are distinguished by the classify function.

nodeIn :: (Ord n, Arbitrary n) => Graph n n e -> Gen n

Generates a node from the graph. (Unless the graph is empty.)

edgeIn :: (Ord n, Arbitrary n, Arbitrary e) => Graph n n e -> Gen (Edge n n e)

Generates an edge from the graph. (Unless the graph contains no edges.)

tests :: IO Bool

All tests.