MODULE m
VAR
	c: boolean;
	n: 0..2;
ASSIGN
	init(c) := FALSE;
	next(c) := case
		c: FALSE;
		n < 2: {TRUE, FALSE};
		n=2: TRUE;
		esac;

	init(n) := 0;
	next(n) := case
		! next(c): (n + 1) mod 3;
		next(c): 0;
		esac;

SPEC AX(c | AX(c | AX c))
SPEC AX(c | AX c)

MODULE main
VAR
	proc: m;