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: