#define N 5	/* Anzahl Besucher-Prozesse */
#define M 3	/* Anzahl maximal zugelassener Besucher */

mtype = { gruen, gelb, rot };	/* Selbstdefinierter Aufzählungstyp */
mtype licht;

byte drin;		/* Anzahl der Besucher im Museum */

active [N] proctype besucher () {
again:	do	/* Besucher will das Museum betreten */
	:: drin < M && licht == gruen ->
		drin = drin + 1;
		break;
	:: else -> skip;
	od;

	/* Besucher ist im Museum */
	skip;

	/* Besucher verläßt das Museum */
	drin = drin - 1;

	goto again;
}

active proctype aufsicht () {
	licht = gruen;

	do	
	/* Aufsicht will Feierabend machen */
	:: licht == gruen ->
		licht = gelb;
	/* Aufsicht macht Feierabend */
	:: licht == gelb && drin == 0 ->
		licht = rot;
	/* Aufsicht kommt morgens wieder und schließt auf */
	:: licht == rot ->
		licht = gruen;
	od;
}