/* Semaphore */

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


property  SEMASPEC(N=3) = S[0],
	  S[0] 		= (up -> S[1]),
	  S[i:1..N-1] 	= (up->S[i+1] | down->S[i-1]),
	  S[N] 		= (down -> S[N-1]).

MENU =(up->MENU| down->MENU).

/* demonstration that SEMASPEC is satisfied */
/* minimise and look at LTS */

||SEMAPHORE(N=4) = (sema[0..N-1]:SEMA(N) || SEMASPEC(N) || MENU)
		   /{sema[i:0..N-2].down/sema[i+1].up,
		     up/sema[0].up,
		     down/sema[N-1].down}@{up,down}.