Module Pre (.ml)

module Pre: sig .. end
Pre-image computation

Pre-image computation
val make_tau : Ast.transition_info -> Ast.transition_func
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.