Refinement

This notion is similar to 1-way conformation but without flaws. It is based on Def. 6.1 of [1].

An STG is defined as a tuple N = (P, T, W, M_N , In, Out, Int, l), where Int is the set of internal signals, such that Int ∩ (In ∪ Out) = ∅, and l is extended accordingly. We will denote by Ext = In ∪ Out the set of external signals of N.

Definition 6.1. (Correct Implementation with Internal Signals) A deterministic STG C (with internal signals) is a correct implementation of an STG N without internal signals if In_C ⊆ In_N, Out_C = Out_N, Int_C ∩ Ext_N = ∅, and for all w and all M such that M_N [w»M the following hold:

(IC1) There is a trace v of C such that M_C[v» with v|_ExtC = w|_ExtC.

For every trace v of C such that M_C[v»M′ with v|_ExtC = w|_ExtC:

(IC2) If a ∈ In_N and M[a±», then either M′[a±» or a∉In_C.

(IC3) If x ∈ Out_N , then M[x±» iff M′[v_Cx±» for some v_C∈(Int_C±)^∗.

A violation witness is a reachable marking (MC,MN) of C×N such that some of the following conditions holds:

• MN[a±» (can replace by MN[a±>), where a± is an input of N that is not ignored by C, and ¬MC[a±» (where the enabledness is via dummies but not internal; if we know that in C no internal signal can trigger an output, e.g. C is input-proper, then can replace this by enabledness via dummies and internal).
  Note: this requirement always holds (and thus does not have to be checked) if C is a circuit-STG, provided that the initial states of inputs are the same in both STGs.
• MN[x±» (can replace by MN[x±>), where x± is an output of both N and C, and ¬MC[x±» (where the enabledness is via dummies and internal).
  Note: this requirement makes refinement relation different from 1-way conformation, and so one can drop it if, e.g., a concurrency reduction has been performed.
• MC[x±» (can replace by MC[x±>), where x± is an output of both N and C, and ¬MN[x±» (where the enabledness is via dummies and internal).

If some of the transformations required for refinement check are skipped, then the same REACH expression can be used to verify a weaker 1-way conformation property (it allows removing traces, e.g. due to concurrency reduction). Such transformation steps that need to be skipped are annotated in brackets.

• We assume that both STGs are input-proper.
• We assume that both STGs are output-determinate whatever the interpretation of internal signals is (as dummies or as outputs). we likely have to require full determinacy, not just output-determinacy, e.g. if one makes the STG for (a|b)+(a|c) with all signals being inputs and a choice implemented by two dummy transitions which are then contracted, the resulting output-determinate but not determinate STG will not be a refinement of itself and will fail the test below.
• In_C ⊆ In_N and Out_C = Out_N.

1. Replace internal signals by dummies for:
   • in N
   • in C (skip this step for 1-way conformation check)
2. Compose the two STGs using PCOMP with option -o to enable composing outputs.
3. Add shadow transitions into the composition for:
   • all inputs of N known to C (skip this step if C is a circuit-STG and the initial states of input signals are the same in both STGs)
   • all outputs of N (skip this step for 1-way conformation check)
   • all outputs of C
4. Add a choice place for all shadow transitions; this is to enforce consistency and simplify unfolding.

Check the following REACH property on the modified composition STG:

// Check whether one STG (implementation) refines another STG (specification).
// The enabled-via-dummies semantics is assumed for @, and configurations with maximal
// dummies are assumed to be allowed - this corresponds to the -Fe mode of MPSAT.
let
    // Names of all shadow transitions in the composed STG.
    SHADOW_TRANSITIONS_NAMES = {"a+", "a-", "x+/1", "x-/2", ""} \ {""},
    SHADOW_TRANSITIONS = gather n in SHADOW_TRANSITIONS_NAMES { T n }
{
    // Optimisation: make sure shadow events are not in the configuration.
    forall e in ev SHADOW_TRANSITIONS \ CUTOFFS { ~$e }
    &
    // Check if some signal is enabled due to shadow transitions only,
    // which would mean that some condition of violation witness holds 
    exists s in (INPUTS + OUTPUTS) {
        let tran_s = tran s {
            exists t in tran_s * SHADOW_TRANSITIONS {
                forall p in pre t { $p }
            }
            &
            forall tt in tran_s \ SHADOW_TRANSITIONS { ~@tt }
        }
    }
}

In many practical cases if the grants of a mutex are internal, hiding them will result in an non-output-determinate STG. E.g. if we take a mutex STG and buffer the grants, so that the mutex grants become internal and the outputs of buffers become outputs – then executions r1+;r2+;(g1+) and r1+;r2+;(g2+) have the same projections on the visible signals but enable different outputs (buf1+ and buf2+, respectively).

Hence we handle an STG with K mutex places as an abbreviation for a product of K mutex STGs with the controller STG that can be obtained from the original STG as follows:

• mutex grants become inputs;
• internal mutex requests become outputs;
• mutex places are replaced by normal places.

Conjecture: the mutex implementability check then implies the N-way conformation passes. Note that this should be checked for both strict and relaxed mutex protocols.

Hence, in a hierarchical model, one more level of hierarchy is introduced.

For simplicity, let's assume that there is one-to-one correspondence between mutex places in the two STGs. This can be established by checking that:

• The number of mutex places is the same.
• The mutex can be uniquely identified by its grants, as no two mutexes can share a grant; so we can establish the 1-to-1 correspondence between mutex places by looking at the grants.
• The requests of the corresponding mutexes are the same.

If these properties hold, we check the refinement of the controller STGs (see above) rather than composed STGs.

In the most general case, the mutexes can be different, and the refinement of compositions needs to be checked. However, this case seems rare in practice, so can just tell to the user that this kind of refinement check is not supported.

If there is no solution reported by MPSat, then the property holds.

If a solution (or a collection of solutions) is reported for the composition STG with shadow transitions, then the following processing of each violation trace needs to be performed:

1. Project the violation of the composition STG to the original implementation STG. Use PCOMP composition details in details.xml and dummy substitutions map.
2. Determine unexpectedly enabled and unexpectedly disabled interface signals. Use MPSAT continuations to identify in the signal enabledness after the violation trace via dummies.