Functor Safa.Make

module Make: 
functor (Q : Common.QUEUE) -> sig .. end
Symbolic equivalence check, using queues Q

Candidates for Q include:

By changing the BDD unifier, we get either the naive or the Hopcroft and Karp like algorithm.

The first argument allows one to trace the execution of the algorithm, a priori using the module Trace. (Cf. Symbolic_kat for a concrete usage.)

Return None if the states were language-equivalent, or a path leading to two states whose output value differ. (Note that the path is reversed.)

Q : Common.QUEUE

val equiv : ?tracer:([ `CE | `OK | `Skip ] -> 's -> 's -> unit) ->
('s, 'k) Bdd.unifier ->
('s, 'v, 'k, 'o) Automata.sdfa ->
's -> 's -> ('s * 's * ('v, 'k) Common.gstring_) option
val equiv_c : ?tracer:([ `CE | `OK | `Skip ] -> Common.int_set -> Common.int_set -> unit) ->
(Common.int_set, 'k) Bdd.unifier ->
(Common.int_set, 'v, 'k, 'o) Automata.sdfa ->
Common.int_set ->
Common.int_set ->
(Common.int_set * Common.int_set * ('v, 'k) Common.gstring_) option
same algorithms, further enhanced using up to congruence