Conformation of device to its environment

This is to verify the conformation of the device (the current work file) to its environment (a user-selected work file).

1. Check prerequisites
   1. Device STG has places (this requirement can be eased by modifying Reach expression)
   2. Devise STG does not have disconnected transitions
   3. Outputs of the device STG and the environment STG are the same
   4. Inputs of the device STG are a subset of inputs of the environment STG
2. Prepare the device STG
   1. Obtain device STG from the current work
      • For STG work it is just a copy STG (it later will be modified)
      • For Circuit work it is a result of Circuit-to-STG conversion
   2. Convert internal signals of the device STG to dummies
      • Keep track of renaming internal signal transitions into dummies in substitutions map (this is necessary for restoring the transition names when projecting the violation trace of the composition STG back on the original device STG)
   3. Export modified device STG into dev.g file
3. Prepare the environment STG
   1. Load the environment STG from a work file specified by the user
   2. Convert internal signals of the environment STG to dummies
   3. Change the signal types of the environment STG so they match those of the device STG
   4. Export modified environment STG into env.g file
4. Prepare composition STG with shadow transitions
   1. Perform parallel composition of dev.g and env.g and save the result into sys.g: 

      pcomp -o -fsys.g -ldetail.xml dev.g env.g

   2. Import the composition STG from sys.g file
   3. Load the composition details from detail.xml file (this is necessary for identifying composition STG places that belong to the device STG component)
   4. Insert shadow transitions for device outputs into the composition STG
   5. Export the modified composition STG with shadow transitions into sys-mod.g file

1. Build unfolding prefix for the composition STG with shadow transitions and save it in sys-mod.pnml file: 

   punf -r -m=sys-mod.pnml sys-mod.g

2. Populate the Reach expression pattern for conformation check with the list of shadow transitions and save it in assertion.txt file
3. Run MPSat to verify the Reach expression assertion.txt for sys-mod.pnml unfolding prefix and save the verification results in solutions.xml file: 

   mpsat -Fs -d @assertion.txt -v0 -f sys-mod.pnml solutions.xml

4. Store composed STG without shadow transitions (the one in sys.g) together with MPSat verification result (this is necessary for subsequent interpretation of violation traces)

An example Reach expression for conformation check with shadow transitions x+/1 and x-/2:

// Check whether several STGs conform to each other.
// The enabled-via-dummies semantics is assumed for @.
// Configurations with maximal dummies are assumed to be allowed.
let
    // Set of phantom output transition names in the whole composed STG.
    SHADOW_OUTPUT_TRANSITIONS_NAMES = {"x+/1", "x-/2", ""} \ {""},
    SHADOW_OUTPUT_TRANSITIONS = gather n in SHADOW_OUTPUT_TRANSITIONS_NAMES { T n }
{
    // Optimisation: make sure phantom events are not in the configuration.
    forall e in ev SHADOW_OUTPUT_TRANSITIONS \ CUTOFFS { ~$e }
    &
    // Check if some output signal is enabled due to phantom transitions only;
    // this would mean that some component STG does not conform to the rest of the composition.
    exists o in OUTPUTS {
        let tran_o = tran o {
            exists t in tran_o * SHADOW_OUTPUT_TRANSITIONS {
                forall p in pre t { $p }
            }
            &
            forall tt in tran_o \ SHADOW_OUTPUT_TRANSITIONS { ~@tt }
        }
    }
}

If there is no solution reported by MPSat, then 1-way conformation property holds.

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

1. Project a violation of the composition STG to the original device STG
   1. Use the composition details in details.xml file to map trace transitions on device STG component
   2. Use substitutions map to restore the internal signals in the trace projection
2. Extend the violation trace with the device output transition that is not expected by the environment
   1. Load the composition STG (without shadow transitions) from sys.g file and reach the problematic state by executing the composition violation trace
   2. Obtain the original device STG from the device work (with all the internal signals) and reach the problematic state by executing the projected violation trace
   3. Identify an enabled output transition in the original device STG that is not enabled in the composition STG (note that a signal transition may be enabled through a dummy)
   4. If a violation transition is identified then add it to the violation trace; otherwise add all suspicious signals to the trace description