Functor TraceCheckerUtil.Reverse


module Reverse: 
functor (E : TraceChecker.S) -> TraceChecker.S
Functor reversing a given trace-checking engine. Conceptually, reversion means that the given trace-checking engine is applied to the reversed model, where:
  • the source and target of each transition are swapped, and
  • the semantics of each command is inversed.

Parameters:
E : TraceChecker.S

include ??
val trace_check : 'a Trace.t -> 'a Result.t
The trace-checking function.