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
open Core
module Auto = Global_compiler.Automaton
module Config = struct
type t = int64 * Packet.T.t [@@deriving compare, hash, sexp]
let of_first (state : int64) (pk : Packet.t) : t =
Int64.(state*2L, pk)
let of_second (state : int64) (pk : Packet.t) : t =
Int64.(state*2L+1L, pk)
end
let check (a1 : Auto.t) (a2 : Auto.t) : bool =
let dead = (Fdd.FDD.drop, Fdd.FDD.drop) in
let dead1 = Auto.add_to_t a1 dead in
let dead2 = Auto.add_to_t a2 dead in
let dom = Domain.(merge (of_automaton a1) (of_automaton a2)) in
let pks = Domain.representative_pks dom in
let worklist = List.map pks ~f:(fun pk -> (a1.source, a2.source, pk)) in
let rel : (Config.t, Config.t Union_find.t) Hashtbl.t =
Hashtbl.create (module Config)
in
let rec loop worklist =
match worklist with
| [] ->
true
| (s1, s2, pk) :: worklist ->
let conf1, conf2 = Config.of_first s1 pk, Config.of_second s2 pk in
let class1 = Hashtbl.find_or_add rel conf1 ~default:(fun () ->
Union_find.create conf1)
in
let class2 = Hashtbl.find_or_add rel conf2 ~default:(fun () ->
Union_find.create conf2)
in
if Union_find.same_class class1 class2 then loop worklist else
let e1, d1 = Hashtbl.find_exn a1.states s1 in
let e2, d2 = Hashtbl.find_exn a2.states s2 in
if not (Set.equal (Packet.eval_e_fdd e1 pk) (Packet.eval_e_fdd e2 pk)) then false else
let () = Union_find.union class1 class2 in
Map.fold2
(Packet.eval_d_fdd d1 pk)
(Packet.eval_d_fdd d2 pk)
~init:worklist
~f:(fun ~key:pk ~data worklist ->
match data with
| `Both (s1, s2) -> (s1, s2, pk) :: worklist
| `Left s1 -> (s1, dead2, pk) :: worklist
| `Right s2 -> (dead1, s2, pk) :: worklist
)
|> loop
in
loop worklist