Module Automata.SNFA

module SNFA: sig .. end

symbolic non-deterministic automata

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

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

}

reindex and memoise an NFA

val reindex : ('s Common.hval, 's Common.hset, 'v, 'k, 'o) t ->
       (int, Common.int_set, 'v, 'k, 'o) t *
       ('s Common.hset -> Common.int_set)

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

val size : (int, Common.int_set, 'a, 'b, 'c) t ->
       Common.int_set -> int * int