====== Refinement ======

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

An STG is defined as a tuple //N = (P, T, W, M<sub>N</sub> , 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<sub>C</sub> ⊆ In<sub>N</sub>, Out<sub>C</sub> = Out<sub>N</sub>, Int<sub>C</sub> ∩ Ext<sub>N</sub> = ∅,// and for all //w// and all //M// such that //M<sub>N</sub> [w>>M//
the following hold:\\ 

(IC1) There is a trace //v// of //C// such that //M<sub>C</sub>[v>>// with //v|<sub>ExtC</sub> = w|<sub>ExtC</sub>.//\\ 

For every trace //v// of //C// such that //M<sub>C</sub>[v>>M′// with //v|<sub>ExtC</sub> = w|<sub>ExtC</sub>//:\\ 

(IC2) If //a ∈ In<sub>N</sub>// and //M[a±>>//, then either //M′[a±>>// or //a∉In<sub>C</sub>//.\\ 

(IC3) If //x ∈ Out<sub>N</sub>// , then //M[x±>>// iff //M′[v<sub>C</sub>x±>>// for some //v<sub>C</sub>∈(Int<sub>C</sub>±)<sup>∗</sup>.// \\


===== 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 //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).


===== 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). FIXME 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<sub>C</sub> ⊆ In<sub>N</sub>// and //Out<sub>C</sub> = Out<sub>N</sub>//.

=== Transformations ===
  - Replace internal signals by dummies for:
    * in N
    * in C (skip this step for 1-way conformation check)
  - Compose the two STGs using PCOMP with option ''-o'' to enable composing outputs.
  - 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
  - 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:
<code reach>
// 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 }
        }
    }
}
</code>

===== 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:
  - Project the violation of the composition STG to the original implementation STG. Use PCOMP composition details in ''details.xml'' and dummy substitutions map.
  - Determine unexpectedly enabled and unexpectedly disabled interface signals. Use MPSAT //continuations// to identify in the signal enabledness after the violation trace via dummies.


[(Khomenko_2008_fi>V. Khomenko, M. Schaefer, W. Vogler: //{{ :devel:verification:output-determinacy.pdf |Output-Determinacy and Asynchronous Circuit Synthesis}}//, Fundamenta Informaticae vol.\ 88(4), pp.\ 541--579, 2008.)]