Module TraceChecker
module TraceChecker:Trace Checker.sig
..end
This module defines the interface of trace-checking engines, as a functor taking as argument a semantics+closure module, and returning a module with a forward/backward trace-checking function. A trace-checking function checks whether a given trace is feasible, and provides a trace invariant when it is not feasible.
The following presents in detail the expected behavior of trace-checking engines. Given a transition system (S, A, →), a trace is a (finite) sequence X0, ..., Xn where each Xi is either a subset of S or an action in A. Such a trace may, equivalently, be seen as the alternating sequence σ0, U1, σ1, ..., Um, σm where:
- U1, ..., Um is the subsequence of X0, ..., Xn composed of subsets of S, and
- σ0, ..., σm ∈ A* are the (potentially empty) action sequences in between.
A trace T = X0, ..., Xn is feasible if there exists m+2 states s0 ∈ S, s1 ∈ U1, ..., sm ∈ Um, sm+1 ∈ S such that, for each 0 ≤ i ≤ m, the transition system contains a path from si to si+1 labeled by σi. Otherwise, the trace is called unfeasible.
A forward trace invariant for T is a sequence H1, ..., Hm of subsets of S, such that, for every i with 0 ≤ i ≤ m, it holds that:
A backward trace invariant for T is a sequence H1, ..., Hm of subsets of S, such that, for every i with 0 ≤ i ≤ m, it holds that:
Remark that every forward trace invariant may be converted into a backward one, and vice versa. Indeed, H1, ..., Hm is a forward trace invariant if and only if (S∖H1), ..., (S∖Hm) is a backward trace invariant. Notice also that a trace is unfeasible if and only if it admits a (forward or backward) trace invariant.
A forward trace invariant H1, ..., Hm is called irreducible if there exists k, l, with 0 ≤ k ≤ l ≤ m+1, such that, for every 1 ≤ i ≤ m, the following conditions hold:
A backward trace invariant H1, ..., Hm is called irreducible if there exists k, l, with 0 ≤ k ≤ l ≤ m+1, such that, for every 1 ≤ i ≤ m, the following conditions hold:
Remark that irreducibility is preserved under the above-mentioned conversion of trace invariants (from forward to backward, and vice versa).
For more flexibility, trace-checking engines may use a relaxed variant of
feasibility, where the sets Ui are discarded. Formally, a trace
T = X0, ..., Xn is weakly feasible if there exists m+2
states s0, ..., sm+1 ∈ S such that, for each 0 ≤ i ≤ m, the
transition system contains a path from si to si+1 labeled by
σi. To prevent confusion, standard feasibility shall be called
strong feasibility.
module T:
module type S =functor (
A
:
Model.SEMANTICS_CLOSURE
) ->
sig
..end