module Common:
Common utility functor for trace-checking engines.
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.