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
		   else
			(SEMA /{mid/down} || SEMAPHORE(N-1) /{mid/up})
		   @{up,down}.

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.