Module Automata.SDFA

module SDFA: sig .. end

symbolic deterministic automata

type ('s, 'v, 'k, 'o) t = {

	`m : ('s, 'k) Bdd.mem;`
	`t : 's -> ('v, ('s, 'k) Bdd.node) Common.span;`
	`o : 's -> 'o;`
	`output_check : 's -> 's -> bool;`
	`state_info : 's Common.formatter;`

}

print an automaton using the module Trace, possibly excluding the specified node

val trace : ?exclude:'s ->
       'v Common.formatter ->
       'k Common.formatter ->
       'o Common.formatter -> ('s, 'v, 'k, 'o) t -> 's -> unit

number of states and Bdd internal nodes reachable from the given list of states

val size : ('s, 'a, 'b, 'c) t -> 's list -> int * int

generic output check: outputs are computed and copmared physically

val generic_output_check : ('s -> 'o) -> 's -> 's -> bool