Conditionals and Recursion

Conditionals can be used in the definition of composite processes as well as primitive processes. The example below uses a conditional to give a recursive definition of SEMAPHORE

/* Semaphore */

SEMA = (up->down->SEMA).  // up is the V operation and down the P operation

||SEMAPHORE(N=16) = if N==1 then
			(SEMA /{mid/down} || SEMAPHORE(N-1) /{mid/up})

LTSA minimises each version of a recursively defined composite e.g. SEMAPHORE(1), SEMAPHORE(2)Consequently, it is often possible to deal with larger systems when defined recursively as opposed to defined as the composition of an indexed set of processes.