Module InvGenGraph.Lsd

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.