sig
type base
val kill_base : LockStepDriver.base -> unit
val mk_base_checker : TransSys.t -> Numeral.t -> LockStepDriver.base
val base_add_invariants :
LockStepDriver.base -> bool -> Term.t list -> unit
val query_base : LockStepDriver.base -> Term.t list -> Model.t option
type step
val kill_step : LockStepDriver.step -> unit
val to_step : LockStepDriver.base -> LockStepDriver.step
val step_cert : LockStepDriver.step -> int
val step_add_invariants :
LockStepDriver.step -> bool -> Term.t list -> unit
val query_step :
bool -> LockStepDriver.step -> (Term.t * 'a) list -> (Term.t * 'a) list
val nu_query_step :
bool -> LockStepDriver.step -> Term.t list -> Model.t option
type pruning
val pruning_sys : LockStepDriver.pruning -> TransSys.t
val kill_pruning : LockStepDriver.pruning -> unit
val mk_pruning_checker : TransSys.t -> LockStepDriver.pruning
val pruning_add_invariants :
LockStepDriver.pruning -> bool -> Term.t list -> unit
val query_pruning :
LockStepDriver.pruning -> Term.t list -> Term.t list * Term.t list
end