Functor TraceCheckerUtil.Common


module Common: 
functor (A : Model.SEMANTICS_CLOSURE) -> sig .. end
Common utility functor for trace-checking engines.
Parameters:
A : Model.SEMANTICS_CLOSURE

include ??
val atom_strong_post : A.Region.t -> 'a Atom.t -> A.Region.t
val atom_strong_pre : A.Region.t -> 'a Atom.t -> A.Region.t
val atom_weak_post : A.Region.t -> 'a Atom.t -> A.Region.t
val atom_weak_pre : A.Region.t -> 'a Atom.t -> A.Region.t
val num_state_atoms : 'a Atom.t array -> int -> int -> int
num_state_atoms a m n returns the number of `State atoms in the array a, between the indexes m and n (inclusive).
val reduce_fwd_invariant : 'a Result.invariant -> 'a Result.invariant
reduce_fwd_invariant inv takes a forward trace invariant (that might be reducible), reduces it and returns the resulting irreducible forward trace invariant.
val reduce_bwd_invariant : 'a Result.invariant -> 'a Result.invariant
reduce_bwd_invariant inv takes a backward trace invariant (that might be reducible), reduces it and returns the resulting irreducible backward trace invariant.