Module TraceChecker.T.Result


module Result: sig .. end
Type of possible results for the trace-checking function. The meaning of these values is detailed in the documentation of the TraceChecker module. Trace invariants shall be irreducible, and encoded as triples (m, H, n) that expose the interesting factor in the sequence:
  • `Invariant_forward (m, H, n) denotes the irreducible forward trace invariant (S)m, H, (∅)n.
  • `Invariant_backward (m, H, n) denotes the irreducible backward trace invariant (∅)m, H, (S)n.
In both cases, the sequence H consists of pairs ((s, r), h) where (s, r) is the original `State atom in the trace, and h is the corresponding invariant region, which must be distinct from and S.

type 'a invariant = int * (('a * A.Region.t) * A.Region.t) Util.Sequence.t * int 
type 'a t = [ `Feasible of [ `Strong | `Weak ]
| `Invariant_backward of 'a invariant
| `Invariant_forward of 'a invariant ]
val print : (Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit