Hiding "\" and "@"

Hiding removes action names from the alphabet of a process and thus makes these concealed actions "silent". By convention, these silent actions are labelled "tau". The general form of a hiding expression is /{set of labels to be hidden}. Sometimes it is more convenient to state the set of action labels, which are visible and hide all other labels. This is expressed by @{set of visible labels }. Hiding expressions can be applied to both primitive and composite processes but are generally used in defining composites.

In the previous section on relabelling, we saw an example which introduced a new action name mid to synchronise two processes. However, processes external to SEMA2 should not use this name. A definition of SEMA2 which hides this name is given below:

SEMA = (up -> down -> SEMA).
||SEMA2 = ( SEMA/{mid/down} || SEMA/{mid/up} ) \{mid}.

Note the mid action has been replaced by tau. LTSA can be directed to produce the minimal LTS, which is observationally equivalent. The minimised LTS for SEMA2 is shown below:

It is usually clearer to specify the visible actions directly rather than hiding those not required. Using "@" the interface to a process can be expressed explicitly as has been done below for SEMAPHORE.

SEMA = (up->down->SEMA).
||SEMAPHORE(N=4) = (sema[0..N-1]:SEMA)

Minimised LTS for SEMAPHORE: