Module Pre (.ml)

module Pre: sig .. end

type reset_memo = unit -> unit

Pre-image computation

val make_tau : Ast.transition_info -> Ast.transition_func * reset_memo

functional form of transition

val pre_image : Ast.transition list -> Node.t -> Node.t list * Node.t list

pre-image tau n returns the pre-image of n by the transition relation tau as a disjunction of cubes in the form of two lists of new nodes. The second list is used to store nodes to postpone depending on a predefined strategy.