Module Bwd.Selected (.ml)

module Selected: Strategy 

Strategy selected by the options of the command line


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.