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, MN , 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 InC ⊆ InN, OutC = OutN, IntC ∩ ExtN = ∅, and for all w and all M such that MN [w»M
the following hold:
(IC1) There is a trace v of C such that MC[v» with v|ExtC = w|ExtC.
For every trace v of C such that MC[v»M′ with v|ExtC = w|ExtC:
(IC2) If a ∈ InN and M[a±», then either M′[a±» or a∉InC.
(IC3) If x ∈ OutN , then M[x±» iff M′[vCx±» for some vC∈(IntC±)∗.
A violation witness is a reachable marking (MC,MN) of C×N such that some of the following conditions holds:
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.
-o
to enable composing outputs.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 original STG, i.e. in a hierarchical model one more level of hierarchy is introduced. 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.
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:
details.xml
and dummy substitutions map.