B.8 Re-Labeling and Hiding

The re-labeling and hiding operators can be applied to both processes and composite processes.

 Relabel:             /{ RelabelDefs } RelabelDefs:             RelabelDef             RelabelDefs, RelabelDef RelabelDef:              ActionLabels / ActionLabels              forall IndexRanges { RelabelDefs }

FSP supports relational re-labeling. The re-labeling operator applies a relation to a process, which can result in replacing many labels with a single label and replacing one label with multiple labels. The re-labeling relation is defined by a set of pairs. Each pair takes the form newlabel/oldlabel. Sets of labels and the replication construct permit the concise definition of the re-labeling relation. In each of the examples below, both the concise form and the equivalent expanded form of the relation are given.

Examples

 /* one to one re-labeling */ P/{ forall[i:1..3] {a[i]/x[i]}} /* equivalent */ P/{ a[1]/x[1], a[2]/x[2], a[3]/x[3] } /* one to many re-labeling */ P/{ {x,y,z}/a } /* equivalent */ P/{ x/a, y/a, z/a } /* many to one re-labeling */ P/{ a/{x,y,z} } /* equivalent */ P/{ a/x, a/y, a/z } /* many to many re-labeling */ P/{ {a,b}/{x,y} } /* equivalent */ P/{ a/x, a/y, b/x , b/y }

If the old label does not appear in the alphabet of P, then the re-labeling pair newlabel/oldlabel has no effect. Re-labeling in FSP is always applied before parallel composition such that for a re-labeling relation R, (P||Q)/R is equivalent to (P/R||Q/R).

 Hiding:            \Set            @ Set

There are two forms of the hiding operator: \ applies a set of labels to a process such that the labels that occur in both the alphabet of the process and the set are hidden; @ applies a set of labels to a process such that every label in the alphabet is hidden except those that occur in the set.

Prefix Matching

Action labels in hiding sets, priority sets and on the right-hand side of a re-labeling pair match prefixes of labels in the alphabet of the process to which they are applied. For example, an action label a in a hiding set will hide all labels prefixed by a, e.g. a.b, a[1], a.x.y. Similarly, the re-labeling pair x/a would replace these labels with x.b, x[1], x.x.y. Prefix matching permits label details to be ignored when processes are composed.