MODULE main
VAR
	singing : boolean;
	laughter : boolean;
	incense : boolean;
	organ : boolean;
ASSIGN
	init( singing ) := 1;
	init( laughter ) := 1;

	next( singing ) := case
		organ & !laughter: !singing;
		!(organ & !laughter) : singing;
		esac;

	next( laughter ) := case
		incense : singing;
		!incense : ! singing;
		esac;
DEFINE
	target := !singing & !laughter;
SPEC
	EF EG target