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)
		   /{sema[i:0..N-2].down/sema[i+1].up,
		     up/sema[0].up,
		     down/sema[N-1].down}
                   @{up,down}.

Minimised LTS for SEMAPHORE: