gistfile1.txt

/**
 * Title: Time-independent Pacman game
 * Authors: Dieter Castel (r0256149) & Jonas Devlieghere (r0256709)
 */

vocabulary PacmanVoc{

	/* We guarantee you that dir, Left, Right, Up, Down 
	 * will always be correctly interpreted in structures. 
	 * You should not check this!
	 */
	type dir 
	Down: dir
	Left: dir
	Right: dir
	Up: dir

	/* Coordinates */
	type xCo isa int
	type yCo isa int

	/* The Ghosts and Pacman */
	type agent 
	pacman:agent

	/* Positions on the play board, including walls and non-existing coordinates.  */
	NoPos(xCo,yCo) 
	Wall(xCo,yCo,dir)
	WallBetween(xCo,yCo,xCo,yCo)
	Reachable(xCo,yCo, xCo, yCo)
	Neighboring(xCo,yCo,xCo,yCo,dir)

	/* Locations of gold and agents on the board. */
	Gold(xCo,yCo)
	Position(agent,xCo,yCo)
	
	/* Game status */
	GameLost
	GameWon
	

	/* Movement */
	PreviousMove(agent,dir)
	Move(agent,dir)
	
	Opposite(dir,dir)
}

theory PacmanTheory:PacmanVoc{
	
	{
		Opposite(Down, Up).
		Opposite(Left, Right).
		Opposite(Right,Left).
		Opposite(Up, Down).
	}
	
	{
		! q[xCo] r[yCo] s[xCo] t[yCo] : Reachable(q,r,s,t) <- (~NoPos(q,r) & ~NoPos(s,t) & (? d[dir] : Neighboring(q, r, s, t, d) &  ~WallBetween(q, r, s, t))).
		! q[xCo] r[yCo] s[xCo] t[yCo] : Reachable(q,r,s,t) <- (~NoPos(q,r) & ~NoPos(s,t) & (q ~= s | r ~= t) & (? x[xCo] y[yCo] : Reachable(q, r, x, y) & Reachable(x, y, s, t))).
	}
	
	/* Neighbors */
	! q[xCo] r[yCo] s[xCo] t[yCo] : Neighboring(q,r,s,t,Down) 	<=> q = s & r = t + 1.
	! q[xCo] r[yCo] s[xCo] t[yCo] : Neighboring(q,r,s,t,Up) 		<=> q = s & t = r + 1.
	! q[xCo] r[yCo] s[xCo] t[yCo] : Neighboring(q,r,s,t,Left) 	<=> r = t & q = s + 1.
	! q[xCo] r[yCo] s[xCo] t[yCo] : Neighboring(q,r,s,t,Right) 	<=> r = t & s = q + 1.
	
	/* Wall Between */
	! q[xCo] r[yCo] s[xCo] t[yCo] : WallBetween(q,r,s,t) <=> (? d[dir] : (Neighboring(q,r,s,t,d) & (Wall(q,r,d) | (? o[dir] : Opposite(d,o) & Wall(s,t,o))))). 

	/* 
	 * Alle vakjes zijn aaneengesloten: vanuit elk vakje bestaat er een pad 
	 * dat niet door muren gaat naar elk ander vakje. 
	 */
	! q[xCo] r[yCo] s[xCo] t[yCo] : (~NoPos(q, r) & ~NoPos(s,t) & (q ~= s | r ~= t)) => Reachable(q, r, s, t).

	/* Er kan enkel	 goud liggen op plaatsen waar een vakje is. */
	! x[xCo] y[yCo] : Gold(x,y) => ~NoPos(x,y). 
	
	/* Niemand staat op plaatsen waar geen vakje is. */
	! x[xCo] y[yCo] a[agent] : Position(a,x,y) => ~NoPos(x,y).
	
	/* Iedereen is op exact 1 plaats. */
	! q[xCo] r[yCo] s[xCo] t[yCo] a[agent] : Position(a,q,r) & Position(a,s,t) => (q = s & r = t).
	
	/*  
	 * De speler verliest wanneer de positie van PacMan dezelfde
	 * is als die van een spookje. De speler wint wanneer er geen 
	 * goud meer ligt en het spel niet verloren is.
	 */
	{
		GameWon <- (~? x[xCo] y[yCo] : Gold(x,y)) & ~GameLost.
		GameLost <- ? a[agent] x[xCo] y[yCo] : Position(pacman,x,y) & Position(a,x,y) & (a ~= pacman).
	}
	
	/* Spookjes kunnen in 1 stap hun richting niet omkeren */	
	! a[agent] d[dir] o[dir] : Move(a,d) &  Opposite(d,o) & PreviousMove(a,o) => a = pacman. 
	
	/* Iedereen kan hoogstens in 1 richting tegelijk bewegen. */	
	! a[agent] x[dir] y[dir]: Move(a,x) & Move(a,y) => x = y.
	
	/* Als het spel NIET gedaan is kan iedereen bewegen. */
	(~ GameLost & ~ GameWon) => ! a[agent] : ? d[dir] : Move(a,d).
	/* Als het spel gedaan is mag niemand bewegen. */
	GameLost | GameWon => ! a[agent] d[dir] : ~Move(a,d).
	
	/* Niemand beweegt van het bord. PacMan als spoken kunnen enkel van een vak naar een geconnecteerd vak lopen. */
	! a[agent] d[dir] q[xCo] r[yCo]: Move(a,d) & Position(a,q,r) & ~NoPos(q,r)=> ? s[xCo] t[yCo] : Neighboring(q,r,s,t,d) & ~NoPos(s,t) & ~WallBetween(q, r, s, t).

}


structure Test:PacmanVoc {
	dir = {u;d;l;r}
	Up=u
	Down=d
	Left=l
	Right=r

	xCo = {1..4}
	yCo = {1..4}

	pacman=p
	agent={p; Blinky; Pinky; Inky; Clyde}
	PreviousMove={p,d;Blinky,d;Pinky,d;Inky,d;Clyde,d}
	
	Wall = {1,1,r}
	
	NoPos = {2,1}
	
}

//procedure main(){
//	stdoptions.nbmodels = 1
//	sols = modelexpand(PacmanTheory,Test)
//	print(sols[1])
//}