Source file `weakTopological.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(**************************************************************************)
(*                                                                        *)
(*  Ocamlgraph: a generic graph library for OCaml                         *)
(*  Copyright (C) 2004-2010                                               *)
(*  Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles        *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

(* Copyright © 2015 Thibault Suzanne <thi.suzanne (@) gmail.com>
 * École Normale Supérieure, Département d'Informatique
 * Paris Sciences et Lettres
*)

(* Original algorithm by François Bourdoncle. See :
 * "Efficient chaotic iteration strategies with widenings",
 * Formal Methods in Programming and their Applications,
 * Springer Berlin Heidelberg, 1993.
*)

module type G = sig
  type t
  module V : Sig.COMPARABLE
  val iter_vertex : (V.t -> unit) -> t -> unit
  val iter_succ : (V.t -> unit) -> t -> V.t -> unit
end

type 'a element =
  | Vertex of 'a
  | Component of 'a * 'a t

and 'a t = 'a element list

let fold_left = List.fold_left

module Make (G : G) = struct

  module HT = Hashtbl.Make(G.V)

  let recursive_scc g root_g =
    (* Straight OCaml implementation of the Section 4.3,
       fig. 4 algorithm in Bourdoncle's paper *)
    let stack = Stack.create () in
    let dfn = HT.create 1024 in
    let num = ref 0 in
    let partition = ref [] in

    G.iter_vertex (fun v -> HT.add dfn v 0) g;

    let rec visit vertex partition =
      let head = ref 0 in
      let loop = ref false in
      Stack.push vertex stack;
      incr num;
      HT.replace dfn vertex !num;
      head := !num;
      G.iter_succ
        (fun succ ->
           let dfn_succ = HT.find dfn succ in
           let min =
             if dfn_succ = 0
             then visit succ partition
             else dfn_succ in
           if min <= !head then begin
             head := min;
             loop := true
           end)
        g vertex;
      if !head = HT.find dfn vertex
      then begin
        HT.replace dfn vertex max_int;
        let element = ref (Stack.pop stack) in
        if !loop then begin
          while G.V.compare !element vertex <> 0 do
            HT.replace dfn !element 0;
            element := Stack.pop stack;
          done;
          partition := component vertex :: !partition;
        end
        else partition := Vertex vertex :: !partition
      end;
      !head

    and component vertex =
      let partition = ref [] in
      G.iter_succ
        (fun succ ->
           if HT.find dfn succ = 0
           then ignore (visit succ partition : int))
        g vertex;
      Component (vertex, !partition)

    in
    let (_ : int) = visit root_g partition in
    !partition

end