Module TraceCheckerUtil


module TraceCheckerUtil: sig .. end
Common utility functor for trace-checking engines.

module Common: 
functor (A : Model.SEMANTICS_CLOSURE) -> sig .. end
Common utility functor for trace-checking engines.
module Reverse: 
functor (E : TraceChecker.S) -> TraceChecker.S
Functor reversing a given trace-checking engine.
module DiscardStates: 
functor (E : TraceChecker.S) -> TraceChecker.S
Functor transforming a given trace-checking engine by discarding `State regions and then reducing the obtained trace invariant.
module Validate: 
functor (E : TraceChecker.S) -> TraceChecker.S
Functor wrapping a given trace-checking engine with result validation.