Module `LockStepDriver`

Lock Step Driver (LSD).

The LSD is used by invariant generation to split its graph using base, discover invariants using step, and prune trivial invariants using pruning.

The workflow is that each invariant generation (graph splitting + invariant discovery at k) starts by creating a base. Once the graph is stable, the base checker is transformed into a step using to_step.

To query a step checker one gives a list of Term.t * 'a where 'a is some information. Typically, it's used to when checking invariants of candidates coming from equivalence classes. If an equality is invariant, then we can remove the term from the eq class of the corresponding representative. In this case the information has type Term.t * Term.t and stores the representative and the term to drop.

type base: The base checker is used to check whether some candidate invariants hold k steps away from the initial state.

val kill_base : base -> unit: Kills a base checker.

val mk_base_checker : TransSys.t -> Numeral.t -> base: Creates a base checker for some system at some depth.

val base_add_invariants : base -> bool -> Term.t list -> unit: Adds some invariants to a base checker. Second argument is the one-state invariants, third is the two-state ones.

val query_base : base -> Term.t list -> Model.t option

Checks whether some terms are falsifiable k states away from the initial state, where k is the internal depth of the base checker.

Returns an option of a model falsifying some of the terms.

type step: The step checker is used to check whether some candidate invariants hold in the k-inductive step instance.

val kill_step : step -> unit: Kills a step checker.

val to_step : base -> step

Transforms a base checker into a step checker.

The step checker thus obtained correspond to the k-induction step instance the base checker corresponds to. That is, the transition relation is unrolled one step further and the initial state constraint is removed.

val step_cert : step -> int: Certificate (k) of a step checker.

val step_add_invariants : step -> bool -> Term.t list -> unit: Adds invariants to a step checker. Second argument is the one-state invariants, third is the two-state ones.

val query_step : bool -> step -> (Term.t * 'a) list -> (Term.t * 'a) list

Queries step.

Takes some candidates, a list of elements of type (Term.t, 'a). The second element is understood as some information about the candidate.

The "information" represented by 'a is used when checking equality candidate invariants coming from equivalence classes from the graph. The info is then a pair representative / eq class member meaning that if the candidate is indeed invariant, we can drop the class member from the equivalence class.

Returns the elements of candidates for which the first element of the pair (the term) is an invariant.

val nu_query_step : bool -> step -> Term.t list -> Model.t option: Queries step, returns an option of the model.

type pruning: Used to check whether some invariants are implied by the transition relation alone. That is, T(0,1) and (not inv(1)) is unsat.

val pruning_sys : pruning -> TransSys.t: System associated with a pruning checker.

val kill_pruning : pruning -> unit: Kills a pruning checker.

val mk_pruning_checker : TransSys.t -> pruning: Creates a pruning checker for a system.

val pruning_add_invariants : pruning -> bool -> Term.t list -> unit: Adds invariants to a pruning checker. Second argument is the one-state invariants, third is the two-state ones.

val query_pruning : pruning -> Term.t list -> Term.t list * Term.t list

Checks if some terms are trivially implied by the transition relation.

Returns a pair of the trivial and the non-trivial invariants.