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