sig
module Common :
functor (A : Model.SEMANTICS_CLOSURE) ->
sig
module Atom :
sig
type 'a t =
[ `Command of A.Command.t
| `Guard of A.Region.t
| `State of 'a * A.Region.t ]
val print :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit
end
module Trace :
sig
type 'a t = 'a Atom.t Util.Sequence.t
val print :
(Format.formatter -> 'a -> unit) ->
Format.formatter -> 'a t -> unit
end
module Result :
sig
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
end
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
val reduce_fwd_invariant : 'a Result.invariant -> 'a Result.invariant
val reduce_bwd_invariant : 'a Result.invariant -> 'a Result.invariant
end
module Reverse : functor (E : TraceChecker.S) -> TraceChecker.S
module DiscardStates : functor (E : TraceChecker.S) -> TraceChecker.S
module Validate : functor (E : TraceChecker.S) -> TraceChecker.S
end
Loading...