Up  Next

Functor Bwd.Make (.ml)

module Make: 
functor (Q : PriorityNodeQueue) -> Strategy

Functor for creating a strategy given a priority queue

Parameters:
Q : PriorityNodeQueue 
val search : ?invariants:Node.t list ->
       ?candidates:Node.t list -> Ast.t_system -> Bwd.result

Backward reachability search on a system. The user can also provide invariants that are true of the system to help the search. Candidate invariants can also be provided, they will be proven as real invariants if necessary.