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
175
176
177
178
179
180
181
182
183
184
open Strong
module type DFA = sig
module States : Finite.Set
module Transitions : Finite.Set
module Label : Map.OrderedType
val label : Transitions.n Finite.elt -> Label.t
val source : Transitions.n Finite.elt -> States.n Finite.elt
val target : Transitions.n Finite.elt -> States.n Finite.elt
val initial_state : States.n Finite.elt
module Final : Finite.Map with type codomain = States.n Finite.elt
end
let index_transitions (type state) (type transition)
(states : state Finite.set)
(transitions : transition Finite.set)
(target : transition Finite.elt -> state Finite.elt)
: state Finite.elt -> transition Finite.elt Finite.map
=
let f = Array.make (Finite.cardinal states + 1) 0 in
Finite.iter_set transitions (fun t ->
let state = (target t :> int)
in f.(state) <- f.(state) + 1
);
for i = 0 to Finite.cardinal states - 1 do
f.(i + 1) <- f.(i + 1) + f.(i)
done;
let a = Array.make (Finite.cardinal transitions)
(Finite.elt_of_int transitions 0)
in
Finite.rev_iter_set transitions (fun t ->
let state = (target t :> int) in
let index = f.(state) - 1 in
f.(state) <- index;
a.(index) <- t
);
(fun st ->
let st = (st : state Finite.elt :> int) in
let offset = f.(st) in
let n = f.(st + 1) - offset in
let module Domain = Natural.Nth(struct let n = n end) in
(module struct
type domain = Domain.n
let domain = Domain.n
type codomain = transition Finite.elt
let get n = a.(offset + (n : Domain.n Finite.elt :> int))
end))
let discard_unreachable
(type state) (type transition)
(blocks : state Partition.t)
(transitions_of : state Finite.elt -> transition Finite.elt Finite.map)
(target : transition Finite.elt -> state Finite.elt)
=
Partition.iter_marked_elements blocks 0 (fun state ->
Finite.iter_map (transitions_of state)
(fun transition -> Partition.mark blocks (target transition));
);
Partition.discard_unmarked blocks
module Minimize (DFA: DFA) : sig
include DFA with module Label = DFA.Label
val transport_state :
DFA.States.n Finite.elt -> States.n Finite.elt option
val transport_transition :
DFA.Transitions.n Finite.elt -> Transitions.n Finite.elt option
val represent_state :
States.n Finite.elt -> DFA.States.n Finite.elt
val represent_transition :
Transitions.n Finite.elt -> DFA.Transitions.n Finite.elt
end = struct
let blocks = Partition.create DFA.States.n
let () =
Partition.mark blocks DFA.initial_state;
let transitions_source =
index_transitions DFA.States.n DFA.Transitions.n DFA.source
in
discard_unreachable blocks transitions_source DFA.target
let transitions_targeting =
index_transitions DFA.States.n DFA.Transitions.n DFA.target
let () =
Finite.iter_map (module DFA.Final) (Partition.mark blocks);
discard_unreachable blocks transitions_targeting DFA.source
let () =
Finite.iter_map (module DFA.Final) (Partition.mark blocks);
Partition.split blocks
let cords = Partition.create
DFA.Transitions.n
~partition:(fun t1 t2 ->
let l1 = DFA.label t1 in
let l2 = DFA.label t2 in
DFA.Label.compare l1 l2
)
let () =
Partition.discard cords
(fun t ->
Partition.set_of blocks (DFA.source t) = -1 ||
Partition.set_of blocks (DFA.target t) = -1)
let () =
let block_set = ref 1 in
let cord_set = ref 0 in
while !cord_set < Partition.set_count cords do
Partition.iter_elements cords !cord_set
(fun transition -> Partition.mark blocks (DFA.source transition));
Partition.split blocks;
while !block_set < Partition.set_count blocks do
Partition.iter_elements blocks !block_set (fun state ->
Finite.iter_map (transitions_targeting state) (Partition.mark cords)
);
Partition.split cords;
incr block_set;
done;
incr cord_set;
done
module States = Natural.Nth(struct let n = Partition.set_count blocks end)
module Transitions = Natural.Nth(struct let n = Partition.set_count cords end)
module Label = DFA.Label
let transport_state_unsafe state =
Finite.elt_of_int
States.n (Partition.set_of blocks state)
let represent_state state =
Partition.choose blocks
(state : States.n Finite.elt :> int)
let represent_transition transition =
Partition.choose cords
(transition : Transitions.n Finite.elt :> int)
let label transition : Label.t =
DFA.label (represent_transition transition)
let source transition =
transport_state_unsafe (DFA.source (represent_transition transition))
let target transition =
transport_state_unsafe (DFA.target (represent_transition transition))
let initial_state =
Finite.elt_of_int States.n
(Partition.set_of blocks DFA.initial_state)
module Final = Finite.Map_of_array(struct
type codomain = States.n Finite.elt
let table =
Finite.iter_map (module DFA.Final) (Partition.mark blocks);
let sets = Partition.marked_sets blocks in
Partition.clear_marks blocks;
Array.map (Finite.elt_of_int States.n) (Array.of_list sets)
end)
let transport_state state =
match Partition.set_of blocks state with
| -1 -> None
| n -> Some (Finite.elt_of_int States.n n)
let transport_transition transition =
match Partition.set_of cords transition with
| -1 -> None
| n -> Some (Finite.elt_of_int Transitions.n n)
end