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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2010-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
(** Operations on relations *)
module type S = sig
type elt0
module Elts : MySet.S with type elt = elt0
include Rel.S with
type elt1 = elt0 and type elt2 = elt0
and module Elts1 = Elts and module Elts2 = Elts
(* Map representation *)
module M : sig
module ME : Map.S with type key = elt0
type map = Elts.t ME.t
val succs : elt0 -> map -> Elts.t
val add : elt0 -> elt0 -> map -> map
val subrel : map -> map -> bool
val exists_path : (elt0 * elt0) -> map -> bool
val to_map : t -> map
val of_map : map -> t
end
(* All elements related *)
val nodes : t -> Elts.t
(* Operations on nodes, ie all elements related *)
val filter_nodes : (elt0 -> bool) -> t -> t
val map_nodes: (elt0 -> elt0) -> t -> t
(* Inverse *)
val inverse : t -> t
(* Set to relation *)
val set_to_rln : Elts.t -> t
(* Are e1 and e2 related by the transitive closure of relation.
Does not detect cycles *)
val exists_path : elt1 * elt2 -> t -> bool
(* Nodes reachable from node and set of nodes [argument included in result] *)
val reachable : elt0 -> t -> Elts.t
val reachable_from_set : Elts.t -> t -> Elts.t
(* One path from one node to another, returns [] if none *)
val path : elt0 -> elt0 -> t -> elt0 list
(* All leaves *)
val leaves : t -> Elts.t
(* All leaves reachable from node *)
val leaves_from : elt0 -> t -> Elts.t
(* All roots, ie all nodes with no predecessor *)
val roots : t -> Elts.t
(* Idem backwards *)
val up : elt0 -> t -> Elts.t
val up_from_set : Elts.t -> t -> Elts.t
(* Transitive closure, the fist function returns Map form *)
val transitive_to_map : t -> Elts.t M.ME.t
val transitive_closure : t -> t
(* Direct cycles *)
val is_reflexive : t -> bool
val is_irreflexive : t -> bool
(* Explicit acyclicity check, cost (one dfs) is neglectible
w.r.t. transitive closure *)
val get_cycle : t -> elt0 list option
val is_acyclic : t -> bool
val is_cyclic : t -> bool
(* Transformation 'order' like lists into relations *)
(* without transitive closure *)
val order_to_succ : elt0 list -> t
(* with transitive closure *)
val order_to_rel : elt0 list -> t
(* Also for cycles *)
val cycle_to_rel : elt0 list -> t
val cycle_option_to_rel : elt0 list option -> t
(* All toplogical order computing functions
raise Cyclic in case of cycle *)
exception Cyclic
(* One topoligical order *)
val topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a
val topo : Elts.t -> t -> elt0 list
(* By exception to the general rule,
The function [pseudo_topo_kont] does not
fail. Instead, it acts as if the backward edge
it discovers is non-existent *)
val pseudo_topo_kont : (elt0 -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a
(****************************************************)
(* Continuation based all_topos (see next function) *)
(****************************************************)
(* Enhancement: all_topos nodes edges still works
when edges relates elts not in nodes *)
(* Orders as a lists *)
val all_topos_kont : Elts.t -> t -> (elt0 list -> 'a -> 'a) -> 'a -> 'a
(* Orders as relations *)
val all_topos_kont_rel :
Elts.t -> t -> (t -> 'a) -> (t -> 'a -> 'a) -> 'a -> 'a
(* All toplogical orders, raises Cyclic in case of cycle
Enhancement: all_topos nodes edges still works
when edges relates elts not in nodes *)
val all_topos : bool (* verbose *)-> Elts.t -> t -> elt0 list list
(* Strongly connected components, processed in inverse dependency order. *)
val scc_kont : (elt0 list -> 'a -> 'a) -> 'a -> Elts.t -> t -> 'a
(* Is the parent relation of a hierarchy *)
val is_hierarchy : Elts.t -> t -> bool
(* Remove any transitivity edges
[LUC: set argument. removed, it is useless, since set = nodes rel is ok]
remove_transitive_edges [set] rel
[assumes rel \in set \times set]
returns rel' \subset rel such that rel'
does not have (e1, e2) if it has both (e1, e3) and (e3, e2),
but transitive_closure rel' = transitive_closure rel
*)
val remove_transitive_edges : t -> t
(* Sequence composition of relation *)
val sequence : t -> t -> t
val transitive3 : t -> t (* returns r;r;r *)
val sequences : t list -> t
(* Equivalence classes, applies to symetric relations only (unchecked) *)
val classes : t -> Elts.t list
(* strata ie sets of nodes by increasing distance *)
val strata : Elts.t -> t -> Elts.t list
(*****************************************************************************)
(* "Bisimulation" w.r.t. relation r, with initial equivalence relation equiv *)
(*****************************************************************************)
(*
`bisimulation T E0` computes the greater equivalence E such that
E0 greater than E
e1 <-E-> e2, e1 -T-> e1' ==> exists e2' s.t. e2 -T-> e2', e1' <-E-> e2'
e1 <-E-> e2, e2 -T-> e2' ==> exists e1' s.t. e1 -T-> e1', e2' <-E-> e1'
*)
val bisimulation : t (* transition *) -> t (* equivalence *)-> t
end
module Make:
functor (O:MySet.OrderedType) -> S
with type elt0 = O.t and module Elts = MySet.Make(O)
|
