The LSD is used by invariant generation to split its graph using
discover invariants using
step, and prune trivial invariants using
The workflow is that each invariant generation (graph splitting + invariant
k) starts by creating a
base. Once the graph is stable, the
base checker is transformed into a
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.
ksteps away from the initial state.
val kill_base :
base -> unit
val mk_base_checker :
TransSys.t -> Numeral.t -> base
val base_add_invariants :
base -> bool -> Term.t list -> unit
val query_base :
base -> Term.t list -> Model.t option
kstates away from the initial state, where
kis the internal depth of the base checker.
Returns an option of a model falsifying some of the terms.
k-inductive step instance.
val kill_step :
step -> unit
val to_step :
base -> step
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
k) of a step checker.
val step_add_invariants :
step -> bool -> Term.t list -> unit
val query_step :
bool -> step -> (Term.t * 'a) list -> (Term.t * 'a) list
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
T(0,1) and (not inv(1))is unsat.
val pruning_sys :
pruning -> TransSys.t
val kill_pruning :
pruning -> unit
val mk_pruning_checker :
TransSys.t -> pruning
val pruning_add_invariants :
pruning -> bool -> Term.t list -> unit
val query_pruning :
pruning -> Term.t list -> Term.t list * Term.t list
Returns a pair of the trivial and the non-trivial invariants.