**************************************************
* Especificación del Pacman en Maibaum's CDAL    *
**************************************************

En el resto del texto el símbolo // indica que luego sigue un comentario.

Sorts:
Levels
Agents
Actions
Heading
Loc


Constants:
         
Levels = { 0,1,2,3,4,5,6,7,8,9 }
	  
Agents = { 0,1,2,3,4,5,6 } U { pacman, gamemaster, player }
// Nueva entidad gamemaster, ejecuta acciones como BeginGame o GamerOver, esto es con el
// único motivo de poder distinguir el estado no-jugando del estado jugando y al revés. 
// Claramente estas acciones las podría ejecutar el pacman y no habría necesidad de agregar
// una entidad más, el problema con esto es que el rol del pacman se comienza a oscurecer
// y no sé sabe si la entidad pacman es una simple entidad dentro del juego, una entidad
// que representa al jugador o ambas cosas. En principio parecería que es mejor agregar
// una entidad adicional que se ocupe de "gobernar" el juego.

*********** PARECE RAZONABLE TENER UN GAMEMASTER *********************

Heading = { n, s, w, e }


Loc = ZxZ



Actions:
Mov // moverse en dirección del heading
NewHead // no determinístico
Eat
BeginGame < Levels >
GameOver
KeyLeft
KeyRight
KeyUp
KeyDown
BeginKey
EndKey


Predicates:

neighbor < Loc,  Loc , Levels> 
//V t1,t2,e neighbor(t1,t2,e) <-> abs(fst(t1)-fst(t2))+abs(snd(t1)-snd(t2)) = 1

legal_pos < Agent, Levels >
//este predicado evalua a TRUE si el agente recibido como parametro
//esta en una posición válida en el level también recibido como
//parametro. Por qué recibe el Level? porque una posición que es
//válida en el Level 1 puede dejar de serlo en el Level 2, el Level
//es quién determina si la posición es válida o no.

legal_mov < Agent , Levels>
//TRUE cuando el agente recibido como parametro puede moverse en
//dirección a su actual heading en el level recibido como parametro.

legal_mov_by_head < Agent , Levels, Heading>
// legal_mov_by_head(x,l,h) true si x puede moverse en dirección h en el level l


food < Loc >

alive < Agent >
// TURE si está vivo, sino FALSE.

not_together < Actions, Actions >
// TRUE si no se pueden ejecutar las dos acciones en paralelo.


player < Agent >
// TRUE si el agente es pacman, FALSE en caso contrario

playing // true si el juego comenzó y false en caso contrario


legalplace < Loc, Levels > 

walkable < Loc , Levels >

there_is_path < Loc, Loc, Levels >
// there_is_path(p1,p2,e) es true si existe un "camino" entre las
// dos posiciones p1 y p2 en el nivel e. Por camino entendemos una
// secuencia de posiciones t1, t2,....,tn tal que:
//
// 1)V(i<n) neighbor(ti,ti+1)
// 2)Vi walkable(ti,e) 

inMapBoundsX < Z , Levels> // true si la coordenada está dentro del tablero
inMapBoundsY < Z , Levels> 


ghost < Agent >


Functions:

LASTLEVEL < N >
level < N >
lives < N >
score < N >

getpos  < Agent , Loc  >
getHead < Agent , Heading >

headx < Heading , N >
heady < Heading , N >

foodCount < Levels , N >
getInitialPos < Agent, Levels , Loc >



.....
.....
.....



Vx ( getpos(x) <> getpos(gamemaster) <> getpos(player) )


[player, BeginKey] O(gamemaster, BeginGame(0) )
[player, EndKey]   O(gamemaster, GameOver )


Vc [ gamemaster, BeginGame(c) ]
level=0 ^ score=0 ^ lives=3 ^ playing
^ Va ( a <> gamemaster -> getpos(a)= getInitialPos(a,c) ^ alive(a) ^ legal_mov(a,c) )
^ Vw ( walkable(w,c) <-> food(w,c) )

// *****No entiendo la utlima formula, walkable es lo mismo que food? o lo 
// es en el contexto de begingame? y si es asi, porque?******************
//
// Lo que intenta especificar la fórmula Vw ( walkable(w,c) <-> food(w,c) ), es que luego
// de que el gamemaster ejecuta la acción BeginGame, todas las posiciones del mapa del actual
// nivel que son caminables deben tener comida. 

[ gamemaster, GameOver ] not playing 


Vt,e ( legal_place(t,e) <-> inMapBoundsX(fst(t),e) ^ inMapBoundsY(snd(t),e)
// *********** que mas define una legalplace? porque no hay 
// equivalencia? ************* 
// 
// El predicado legal_place evalua que la posición recibida como parametro esté
// dentro de los límites del mapa del nivel actual. Todos las posiciones que no
// evaluen a TRUE estan fuera del mapa del nivel como recibido como parametro. 


Vt,t',e legal_place(t,e) ^ legal_place(t',e) ^ walkable(t,e) ^ walkable(t',e) -> there_is_path(t,t',e)
// ******** el grafo de las locaciones walkables es totalmente 
// conexo?!!! ******************
//
// Sí, el grafo de los tiles caminables es conexo. La fórmula de arriba pretende capturar 
// esa idea: si las posiciones t y t' son válidas y ambas caminables, entonces existe un 
// camino entre ellas.


Va,e ( getInitialPos(a,e) = p -> legal_place (p,e) ^ walkable(p,e) )


Va ( alive(a) ^ legal_mov(a) -> getpos(a) = (x,y) -> [a, Mov]
	getpos(a) = ( x + headx(gethead(a)) , y + heady (gethead(a)) )


headx w = -1
headx e =  1
headx _ =  0
heady n = -1
heady s =  1
heady _ =  0


playing ^ legal_mov(pacman, level) -> [ pacman, Mov]  food(getpos(pacman),level) -> O(pacman, Eat)


playing ^ food(getpos(pacman),level) ^ score=h ^ foodCount(level)=y -> [pacman, Eat] 
	not food(getpos(pacman),level) ^ score=h+1 ^ foodCount(level)=y-1


level <> LASTLEVEL ^ foodCount(level)=0 -> O(gamemaster,BeginGame(level+1) )

level = LASTLEVEL ^ foodCount(level)=0 -> O(gamemaster, GameOver)


Vx ( getpos(x) = getpos(pacman) ^ ghost(x) ^ alive(x) ^ lives=n ^ lives>1 -> lives = n-1 )
// Si un fantasma choca con el pacman y el pacman tiene más de una vida le quitamos una vida.


Vx ( getpos(x) = getpos(pacman) ^ ghost(x) ^ alive(x) ^ lives=1 -> O(gamemaster,GameOver)
// Si un fantasma choca con el pacman y el pacman tiene solo una vida terminamos el juego.


/// ########### GHOSTS' BEHAVIOR ##############

Vx ( ghost(x) ^ playing ^ alive(x) ^ not legal_mov(x, level) -> O(x,NewHead) // Esta obligado a cambiar de heading

Vx ( ghost(x) ^ playing ^ alive(x) ^ not legal_mov(x, level) -> [x,NewHead] legal_mov(x,level) )
// *********** me parece que sobra "notlegal_mov" en
// el antecedente *******************
//
// Creo que no está demás, ya que la idea con esta fórmula era que un GHOST cambie
// de Heading cuando ya no puede moverse en dirección al Heading actual, o
// sea cuando llega al límite de un corredor.

Vx ( ghost(x) ^ playing ^ alive(x) ^ legal_mov(x, level) -> O(x,Mov) )
// ************* porque en vez de O(x,Mov) no podria ir O(x, Mov+NewHead;Mov) ??
// quedaria mas no detereministico y divertido**********
//
// Podría ser, pero esto le daría permiso a los ghosts para cambiar de heading
// casi en cualquier instante, y ése no era el comportamiento que esperabamos 
// de ellos. 




// *********las 4 formulas que siguen dicen que los ghosts siempre miran al pcman, 
// esto es asi? *****
//
// No, las 4 fórmulas de abajo afirman que cuando un Ghost está en la intersección de dos
// caminos o túneles puede cambiar de heading si el pacman va por el tunel en el que no está
// el Ghost. Es cómo para que los Ghost persigan al pacman. 


Vx ( ghost(x) ^ playing ^ alive(x) ^ getpos(x) = ( x1, y2 ) ^ getpos(pacman) = ( x2, y2 )
	^ x1=x2 ^ y1 > y2 ^ legal_mov_by_head(x,level, n) -> getHead(x)= n )

Vx ( ghost(x) ^ playing ^ alive(x) ^ getpos(x) = ( x1, y2 ) ^ getpos(pacman) = ( x2, y2 )
	^ x1=x2 ^ y1 < y2 ^ legal_mov_by_head(x,level, s) -> getHead(x)= s )

Vx ( ghost(x) ^ playing ^ alive(x) ^ getpos(x) = ( x1, y2 ) ^ getpos(pacman) = ( x2, y2 )
	^ y1=y2 ^ x1 > y2 ^ legal_mov_by_head(x,level, w) -> getHead(x)= w )

Vx ( ghost(x) ^ playing ^ alive(x) ^ getpos(x) = ( x1, y2 ) ^ getpos(pacman) = ( x2, y2 )
	^ y1=y2 ^ x1 < y2 ^ legal_mov_by_head(x,level, e) -> getHead(x)= e )

/// ########### GHOSTS' BEHAVIOR ##############


playing ^ legal_mov_by_head(pacman,level,w) -> [player, KeyLeft]  getHead(pacman) = w
// el pacman cambia de heading si hay un legal_mov en esa dirección
playing ^ legal_mov_by_head(pacman,level,e) -> [player, KeyRight] getHead(pacman) = e
playing ^ legal_mov_by_head(pacman,level,n) -> [player, KeyUp] getHead(pacman)    = n
playing ^ legal_mov_by_head(pacman,level,s) -> [player, KeyDown] getHead(pacman)  = s

playing ^ legal_mov(pacman, level) -> O(pacman,Mov) )