# ### Site Tools

devel:verification:refinement

# Refinement

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

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.

Deﬁnition 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±).

## Violation witness

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 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 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 is an output of both N and C, and ¬MN[x±» (where the enabledness is via dummies and internal).

## How to verify this property

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.

#### Prerequisites

• 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.
• InC ⊆ InN and OutC = OutN.

#### Transformations

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.
• 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.

#### REACH property

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", ""} \ {""},
{
// 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 }
}
}
}```

## Handling mutexes

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.

## Processing violation traces

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.

 V. Khomenko, M. Schaefer, W. Vogler: Output-Determinacy and Asynchronous Circuit Synthesis (388 KiB), Fundamenta Informaticae vol. 88(4), pp. 541–579, 2008. 