`module Lsd: ``LockStepDriver`

LSD module.

`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.