(**************************************************************************) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) (* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) (* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) (* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) (* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) (* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) (* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) (* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) (* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) (* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) (* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) (* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) (* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) (* SUCH DAMAGE. *) (**************************************************************************) (** Generic graph type based on OCaml Set and Map *) module type OrderedType = sig type t val compare : t -> t -> int end module type S = sig type node type graph type node_set val leaves : graph -> node_set val empty : graph (** Add an edge from the first node to the second node, creating the nodes if they do not exist. *) val add_edge : node -> node -> graph -> graph val add_edges : node -> node list -> graph -> graph val children : graph -> node -> node list (** Return the set of nodes that are reachable from the first set of nodes (roots), without passing through the second set of nodes (cuts). *) val reachable : node_set -> node_set -> graph -> node_set (** Prune a graph from roots to cuts. *) val prune : node_set -> node_set -> graph -> graph val remove_self_loops : graph -> graph val reverse : graph -> graph exception Not_a_DAG of node * graph;; (** Topologically sort a graph. Throws Not_a_DAG if the graph is not directed acyclic. *) val topsort : graph -> node list (** Find strongly connected components using Tarjan's algorithm. This algorithm also returns a topological sorting of the graph components. *) val scc : ?original_order:(node list) -> graph -> node list list val make_dot : (node -> string) -> (node -> node -> string) -> (node -> string) -> out_channel -> graph -> unit end module Make(Ord: OrderedType) : S with type node = Ord.t and type node_set = Set.Make(Ord).t and type graph = Set.Make(Ord).t Map.Make(Ord).t