Module Trace.Selected (.ml)

module Selected: S 

The certificate generator selected by the command line options. Contains a dummy generator if no -trace option was specified.


val certificate : Ast.t_system -> Node.t list -> unit

this takes a system in input and the list of visited nodes, of which the disjunction constitutes an inductive invariant for the system.

certificate s visited must write on the disk a certificate of induction (initialization, preservation, and implication) and print the location of the generated certificate on stdout.