Module Safety (.ml)

module Safety: sig .. end
Safety checks

exception Unsafe of Node.t
exception to signal that a safety check failed. In this case the current search must be stopped.
val check : Ast.t_system -> Node.t -> unit
check s n raises Unsafe n if the node n is immediately reachable in the system s, i.e. if n /\ s.init is not unsatifiable. Otherwise it does nothing.