Module InvGenGraph.Int

module Int: Graph 
Graph of integers with less than or equal.

module Domain: InvGenDomain.Domain 
Domain with an order relation.
type graph 
A graph.
val mk : InvGenGraph.term -> InvGenGraph.set -> graph
Creates a graph from a single equivalence class and its representative.
val has_svars : graph -> bool
Checks whether at least one candidate mentions a state variable.
val mine : bool ->
bool ->
Analysis.param ->
TransSys.t ->
(TransSys.t -> unit) ->
(TransSys.t * graph * InvGenGraph.set * InvGenGraph.set)
list
Mines a system and creates the relevant graphs.

First boolean is top_only, then two_state. Input function is applied to each subsystem. It is used to create the pruning checkers.

val clone : graph -> graph
Clones a graph.
val term_count : graph -> int
Total number of terms in the graph.
val class_count : graph -> int
Total number of classes in the graph.
val is_stale : graph -> bool
Returns true if all classes in the graph only have one candidate term.
val drop_class_member : graph -> InvGenGraph.term -> InvGenGraph.term -> unit
Drops a term from the class corresponding to a representative.
val fmt_graph_dot : Format.formatter -> graph -> unit
Formats a graph in dot format. Only the representatives will appear.

Formats the eq classes of a graph in dot format.

val fmt_graph_classes_dot : Format.formatter -> graph -> unit
val check_graph : graph -> bool
Checks that a graph makes sense. Dumps the graph and its classes in dot format in the current directory if the graph does not make sense.
val terms_of : graph ->
(InvGenGraph.term -> bool) -> InvGenGraph.term list
Minimal list of terms encoding the current state of the graph. Contains Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

Used when querying the base instance of the LSD (graph stabilization). See also equalities_of and relations_of, used for the step instance (induction check).

val equalities_of : graph ->
(InvGenGraph.term -> bool) ->
(InvGenGraph.term * (InvGenGraph.term * InvGenGraph.term)) list
Equalities coming from the equivalence classes of a graph.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

Generates a list of pairs term * (term * term). The first term is the candidate invariant, while the second element stores the representative of the class the candidate comes from, and the term that can be dropped from it if the candidate is indeed invariant.

val relations_of : graph ->
(InvGenGraph.term * unit) list ->
(InvGenGraph.term -> bool) -> (InvGenGraph.term * unit) list
Appends the relations from a graph to the input term list.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

More precisely, generates implications between representatives and the representative and terms of each equivalence class they're a parent of.

Generates a list of pairs term * unit. The useless unit second element is just there to be compatible with the signature of the lsd step query function. This is to accomodate with the information we need to keep around for the equalities of a graph (see equalities_of).

val stabilize : graph ->
TransSys.t -> (InvGenGraph.term -> bool) -> Lsd.base -> unit
Queries the lsd and updates the graph. Terminates when the graph is stable, meaning all terms the graph represents are unfalsifiable in the current lsd.

Input function returns true for candidates we want to ignore, typically candidates we have already proved true.

val step_stabilize : bool ->
graph ->
TransSys.t ->
(InvGenGraph.term -> bool) ->
Lsd.step -> ((Term.t * Certificate.t) list -> unit) -> Term.t list
Clones the graph, and splits it in step.

Stabilizes eq classes one by one, communicates invariants at each step. Then stabilizes relations, communicating by packs.