module type Graph =`sig`

..`end`

Signature of the modules created by the graph functor.

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

- equality between representatives and their class, and
- comparison terms between representatives.

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.