module examples/toys/pacman

open util/ordering[State] as ord

abstract sig Position { adjacent : set Position }

one sig p00,p01,p02,
        p10,p11,p12,
        p20,p21,p22 
	extends Position {}
 
fact AdjacentPositions {
	adjacent = 
		p00 -> p01 + p00 -> p10 +				
		p01 -> p00 + p01 -> p02 + p01 -> p11 +
		p02 -> p01 + p02 -> p12 +
		p10 -> p00 + p10 -> p11 + p10 -> p20 +
		p11 -> p10 + p11 -> p12 + p11 -> p01 + p11 -> p21 +
		p12 -> p11 + p12 -> p02 + p12 -> p22 +
		p20 -> p10 + p20 -> p21 +
		p21 -> p20 + p21 -> p11 + p21 -> p22 +
		p22 -> p12 + p22 -> p21
}

abstract sig Status {}

one sig Play, Won, Lost extends Status {}

sig State {
	walls : set Position,
	food : set Position,
	pacman : Position,
	blinky : Position,
	status : Status
}

fact WallsAreSolid {
	all s : State | 
		s.walls & s.food = none and
		not (s.pacman in (s.walls)) and
		not (s.blinky in (s.walls))
}

fact GameIsWonWhenAllTheFoodIsGone {
	all s : State |
		s.status= Won iff s.food = none
}

fact GameIsLostWhenBlinkyGetsPacman {
	all s : State |
		s.status = Lost iff s.blinky = s.pacman
}

pred FoodSupplyNeverIncreases(s, s' : State)
{
	s'.food in s.food
}

pred FoodIsEatenByPacman(s, s': State)
{
	s'.food = s.food - s.pacman
}

pred WallsDontMove(s, s' : State)
{
	s.walls = s'.walls
}

pred MovementIsOnlyToAdjacentPosition(s, s':State)
{
	let p = (s'.pacman), q = (s.pacman) | p->q in adjacent
	let p = (s'.blinky), q = (s.blinky) | p->q in adjacent
}

pred MovementIsPossibleOnlyWhilePlaying(s,s':State)
{
	s.status != Play implies s = s'
}

fact ValidBehaviour {
	all s: State, s': ord/next(s) {
		FoodSupplyNeverIncreases(s,s') and
		FoodIsEatenByPacman(s,s') and 
		MovementIsOnlyToAdjacentPosition(s,s') and
		WallsDontMove(s,s') and
		MovementIsPossibleOnlyWhilePlaying(s,s') 
	}
}

pred InitGame(s : State)
{
	s.walls = p01 + p11  and
	s.food = p00 + p02 + p10 + p12 + p20 +p22 and
	s.status = Play
}

fact initialState {
   InitGame(ord/first())
}

pred GameWon() {
	ord/last().status = Won
}

pred GameLost() {
	ord/last().status = Lost
}

pred GamePlay() {
	ord/last().status = Play
}

//run GamePlay for 1 State

//run GameLost for 8 State 

run GameWon for 8 State