Functor Safa.Make

module Make: 
functor (Q : Common.QUEUE) -> sig .. end

Symbolic equivalence check, using queues Q

Candidates for Q include:

• fifo queues for breadth-first exploration (Queues.BFS)
• lifo queues for depth-first exploration (Queues.DFS)
• random queues for random exploration (Queues.RFS)

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.)

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