Module TraceChecker


module TraceChecker: sig .. end
Trace Checker.

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.
In particular, σ0 (resp. σm) is empty if T starts (resp. ends) with a subset of S.

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:

Hi+1 ⊇ post(Hi ∩ Ui, σi) ∩ Ui+1
where U0 = Um+1 = S, H0 = S and Hm+1 = ∅.

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:

Hi ⊇ pre(Hi+1 ∩ Ui+1, σi) ∩ Ui
where U0 = Um+1 = S, H0 = ∅ and Hm+1 = S.

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:

(i ≤ k) ⇒ (Hi = S) and (i ≥ l) ⇒ (Hi = ∅) and (k < i < l) ⇒ (Ui∖Hi ∉ {∅, Ui})

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:

(i ≤ k) ⇒ (Hi = ∅) and (i ≥ l) ⇒ (Hi = S) and (k < i < l) ⇒ (Ui∖Hi ∉ {∅, Ui})

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: 
functor (A : Model.SEMANTICS_CLOSURE) -> sig .. end
Common interface to all trace-checking engines.
module type S = functor (A : Model.SEMANTICS_CLOSURE) -> sig .. end