MODULE ob(ix, iy)
VAR
	x: 0..7;
	y: 0..7;
INIT x=ix & y=iy
INVAR (x=0 & (y=0 | y=5 | y=6 | y=7)) |
	(x=1 & (y=0 | y=2 | y=3 | y=7)) |
	(x=3 & (y=1 | y=2 | y=3 | y=5)) |
	(x=4 & (y=1 | y=2 | y=3 | y=4 | y=5 | y=6)) |
	(x=5 & (y=1 | y=2 | y=4 | y=5 | y=6)) |
	(x=2 & (y=2 | y=3 | y=4 | y=5 | y=7)) |
	(x=6 & (y=2 | y=3 | y=4))

MODULE main
VAR
	agent: ob(4, 3);
	b0: ob(2, 2);
	b1: ob(3, 2);
	b2: ob(3, 5);
	b3: ob(4, 5);
	movement: {left, up, right, down, finished};
--Handy variable for deltas
DEFINE dx := case
		movement = left : -1;
		movement = right: +1;
		TRUE:              0;
	esac;
	dy := case
		movement = up  : -1;
		movement = down: +1;
		TRUE:             0;
	esac;
--Agent not on the box
INVAR !(b0.x = agent.x & b0.y = agent.y) &
	!(b1.x = agent.x & b1.y = agent.y) &
	!(b2.x = agent.x & b2.y = agent.y) &
	!(b3.x = agent.x & b3.y = agent.y);
--Box not on box
INVAR !(b0.x=b1.x &b0.y=b1.y) & !(b0.x=b2.x &b0.y=b2.y) & !(b0.x=b3.x &b0.y=b3.y) &
	!(b1.x=b2.x &b1.y=b2.y) & !(b1.x=b3.x &b1.y=b3.y) &
	!(b2.x=b3.x &b2.y=b3.y) &
	TRUE;
--Goal state
INVAR ((b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) |
	(b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b3.x = 4 & b3.y = 5) |
	(b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
	(b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b3.x = 4 & b3.y = 5) |
	(b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
	(b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b3.x = 4 & b3.y = 5) |
	(b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
	(b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b0.x = 4 & b0.y = 5) |
	(b2.x = 4 & b2.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
	(b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
	(b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b0.x = 4 & b0.y = 5) |
	(b1.x = 4 & b1.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b0.x = 4 & b0.y = 5) |
	(b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
	(b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b1.x = 3 & b1.y = 3 & b2.x = 4 & b2.y = 5) |
	(b0.x = 4 & b0.y = 2 & b1.x = 5 & b1.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
	(b3.x = 4 & b3.y = 2 & b1.x = 5 & b1.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
	(b1.x = 4 & b1.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b2.x = 4 & b2.y = 5) |
	(b1.x = 4 & b1.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b2.x = 4 & b2.y = 5) |
	(b3.x = 4 & b3.y = 2 & b0.x = 5 & b0.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
	(b0.x = 4 & b0.y = 2 & b3.x = 5 & b3.y = 2 & b2.x = 3 & b2.y = 3 & b1.x = 4 & b1.y = 5) |
	(b0.x = 4 & b0.y = 2 & b2.x = 5 & b2.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5) |
	(b3.x = 4 & b3.y = 2 & b2.x = 5 & b2.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
	(b2.x = 4 & b2.y = 2 & b3.x = 5 & b3.y = 2 & b0.x = 3 & b0.y = 3 & b1.x = 4 & b1.y = 5) |
	(b2.x = 4 & b2.y = 2 & b0.x = 5 & b0.y = 2 & b3.x = 3 & b3.y = 3 & b1.x = 4 & b1.y = 5))<->movement=finished;
--Agent movement
TRANS next(agent.x) = agent.x + dx & next(agent.y) = agent.y + dy;
--Box movement
TRANS next(b0.x) = case
		next(agent.x) = b0.x & next(agent.y) = b0.y: b0.x + dx;
		TRUE: b0.x;
	esac;
TRANS next(b0.y) = case
		next(agent.x) = b0.x & next(agent.y) = b0.y: b0.y + dy;
		TRUE: b0.y;
	esac;
TRANS next(b1.x) = case
		next(agent.x) = b1.x & next(agent.y) = b1.y: b1.x + dx;
		TRUE: b1.x;
	esac;
TRANS next(b1.y) = case
		next(agent.x) = b1.x & next(agent.y) = b1.y: b1.y + dy;
		TRUE: b1.y;
	esac;
TRANS next(b2.x) = case
		next(agent.x) = b2.x & next(agent.y) = b2.y: b2.x + dx;
		TRUE: b2.x;
	esac;
TRANS next(b2.y) = case
		next(agent.x) = b2.x & next(agent.y) = b2.y: b2.y + dy;
		TRUE: b2.y;
	esac;
TRANS next(b3.x) = case
		next(agent.x) = b3.x & next(agent.y) = b3.y: b3.x + dx;
		TRUE: b3.x;
	esac;
TRANS next(b3.y) = case
		next(agent.x) = b3.x & next(agent.y) = b3.y: b3.y + dy;
		TRUE: b3.y;
	esac;
CTLSPEC ! EF (movement = finished);