damas.smv

--
--			P1
--	  __1___2___3___4__
--	1 |-1 |_0_|-1_|_1_|  	/ \			 |
--	2 |_0_|-1_|_0_|-1_|		 | Descer 	\ / Subir
--	3 |-1_|_0_|-1_|_0_| 
--	4 |_3_|-1_|_0_|-1_| 
--			P2
--						
--			->	Direita (Sobe no Vetor)
--			<-	Esquerda (Desce no Vetor)
--
--	Significados dos Blocos: 
--  1 	-> P1.normal
--  2 	-> P1.dama
--  3 	-> P2.normal
--  4 	-> P2.Damas
--  -1	-> Espaço Inacessível (Espaços Brancos)
--  0	-> Espaço Vazio

MODULE main

	VAR
	    tabuleiro : array 1..4 of array 1..4 of {-1,0,1,2,3,4};
	    turno: boolean; --TRUE - Jogador1 | FALSE - Jogador2
	    num_pecas1: 0..4;
	    num_pecas2: 0..4;
	    linha: {1,2,3,4};
	    coluna:{1,2,3,4};
	    estado: {andando, parado, finalizado, comendo};

	DEFINE

		--1 CASA
		linhaCima :=case
					linha+1 < 4: linha + 1;
					TRUE: linha;
					esac;

		linhaBaixo :=case
					linha - 1 > 0: linha - 1;
					TRUE: linha;
					esac;

		diagDir :=	case
					coluna + 1 < 0: coluna + 1; 
					TRUE: coluna;
					esac;

		diagEsq :=	case
					coluna - 1 < 0: coluna - 1; 
					TRUE: coluna;
					esac;

		--2 CASA

		linhaCima2 := 	case
						linha+2 < 4: linha + 2;
						TRUE: linha;
						esac;

		linhaBaixo2 := 	case
						linha - 2 > 0: linha - 2;
						TRUE: linha;
						esac;

		diagDir2 :=	case
					coluna + 2 < 0: coluna + 2; 
					TRUE: coluna;
					esac;

		diagEsq2 :=	case
					coluna - 2 < 0: coluna - 2; 
					TRUE: coluna;
					esac;

		--3 CASA
		linhaCima3 := 	case
						linha+3 < 4: linha + 3;
						TRUE: linha;
						esac;

		linhaBaixo3 := 	case
						linha - 3 > 0: linha - 3;
						TRUE: linha;
						esac;

		diagDir3 :=	case
					coluna + 3 < 0: coluna + 3; 
					TRUE: coluna;
					esac;

		diagEsq3 :=	case
					coluna - 3 < 0: coluna - 3; 
					TRUE: coluna;
					esac;

		valido_andar := case
							num_pecas1 > 0 & turno = TRUE & tabuleiro[linha][coluna] = 1 & (tabuleiro[linhaCima][diagEsq] = 0 | tabuleiro[linhaCima][diagDir] = 0): TRUE;
							num_pecas2 > 0 & turno = FALSE & tabuleiro[linha][coluna] = 3 & (tabuleiro[linhaBaixo][diagEsq] = 0 | tabuleiro[linhaBaixo][diagDir] = 0): TRUE;
						TRUE: FALSE;
						esac;

		valido_comer := case
							num_pecas1 > 0 & turno = TRUE & tabuleiro[linha][coluna] = 1: case
								tabuleiro[linhaCima][diagDir] = 3 | tabuleiro[linhaCima][diagDir] = 4 & tabuleiro[linhaCima2][diagDir2] = 0: TRUE;
								tabuleiro[linhaCima][diagEsq] = 3 | tabuleiro[linhaCima][diagEsq] = 4 & tabuleiro[linhaCima2][diagEsq2] = 0: TRUE;
								TRUE: FALSE;
								esac;

							num_pecas2 > 0 & turno = FALSE & tabuleiro[linha][coluna] = 3: case 
								tabuleiro[linhaBaixo][diagDir] = 1 | tabuleiro[linhaBaixo][diagDir] = 2 & tabuleiro[linhaBaixo2][diagDir2] = 0: TRUE;
								tabuleiro[linhaBaixo][diagEsq] = 1 | tabuleiro[linhaBaixo][diagEsq] = 2 & tabuleiro[linhaBaixo2][diagEsq2] = 0: TRUE;
								TRUE: FALSE;
								esac;

						TRUE: FALSE;
						esac;

		casa_valida :=	case
						(turno = TRUE & (tabuleiro[linha][coluna] = 1 | tabuleiro[linha][coluna] = 2)) | 
						(turno = FALSE & (tabuleiro[linha][coluna] = 3 | tabuleiro[linha][coluna] = 4)): TRUE;
						TRUE: FALSE;
						esac;

		
	ASSIGN
		init(turno) := TRUE;
		init(num_pecas1) := 1;
		init(num_pecas2) := 1;
		init(estado) := andando;
			
			--INACESSÍVEIS
		init(tabuleiro[1][1]) := -1;
		init(tabuleiro[1][3]) := -1;
		
		init(tabuleiro[2][2]) := -1;
		init(tabuleiro[2][4]) := -1;

		init(tabuleiro[3][1]) := -1;
		init(tabuleiro[3][3]) := -1;
	
		init(tabuleiro[4][2]) := -1;
		init(tabuleiro[4][4]) := -1;
		init(linha) := 1;
		init(coluna) := 4;

		--P1
		--LINHA 1
		init(tabuleiro[1][2]) := 0;
		init(tabuleiro[1][4]) := 1;		

		--LINHA 2
		init(tabuleiro[2][1]) := 0;
		init(tabuleiro[2][3]) := 0;
		--FIMP1

		--P2 
		--LINHA 3
		init(tabuleiro[3][2]) := 0;
		init(tabuleiro[3][4]) := 0;		
		--LINHA 4
		init(tabuleiro[4][1]) := 3; 
		init(tabuleiro[4][3]) := 0;	
		--FIM P2	

	ASSIGN
		next(linha) := 	case
						estado = parado: {1,2,3,4};
						TRUE linha;
						esac;

		next(coluna) := case
						estado = parado: {1,2,3,4};
						TRUE: coluna;
						esac;

		--NUMERO DE PECAS

		next(num_pecas1) := case
							valido_comer :num_pecas1 -1;
							TRUE: num_pecas1;
							esac;

		next(num_pecas2) := case
							valido_comer :num_pecas2 -1;
							TRUE: num_pecas2;
							esac;
		--ESTADO POSSIVEIS
		--Só trocar do andando para o parado depois de achar uma casa valida
		--Só trocar do parado para o vez depois de ceder a vez;
		--Só finalizado quando Deus quer;
		--Andar depois do parado;

		next(estado) := 	case
								num_pecas1 = 0 | num_pecas2 = 0: finalizado;
								estado = parado & casa_valida = TRUE:	case
									valido_comer & valido_andar: comendo;
									valido_andar: andando;
									TRUE: parado; 
									esac;
								estado = andando | estado = comendo: parado;
							TRUE: estado;
							esac;

		--turnos
		next(turno) := 	case
							estado = parado: 
								case 
									turno = TRUE: FALSE;
									turno = FALSE: TRUE;
								TRUE: turno;
								esac;
							TRUE: turno;
							esac;
						
next(tabuleiro[1][2]) := case
	estado = andando & ((linhaCima=1 & diagDir=2)|(linhaBaixo=1 & diagDir=2)|(linhaCima=1 & diagEsq=2)|(linhaBaixo=1 & diagEsq=2)): case
		turno = TRUE   : 0;	
		turno = FALSE : 3;
		TRUE : tabuleiro[1][2];
	esac;
	
	estado = comendo & ((linhaCima2=1 & diagDir2=2)|(linhaBaixo2=1 & diagDir2=2)|(linhaCima2=1 & diagEsq2=2)|(linhaBaixo2=1 & diagEsq2=2)): case
		turno = TRUE : 0;
		turno = FALSE : 3;
		TRUE : tabuleiro[1][2];
	esac;
TRUE : tabuleiro[1][2];
esac;

next(tabuleiro[1][4]) := case
	estado = andando & ((linhaCima=1 & diagDir=4)|(linhaBaixo=1 & diagDir=4)|(linhaCima=1 & diagEsq=4)|(linhaBaixo=1 & diagEsq=4)): case	
		turno = TRUE : 0;
		turno = FALSE : 3;
		TRUE : tabuleiro[1][4];
	esac;
					
			
	estado = comendo & ((linhaCima2=1 & diagDir2=4)|(linhaBaixo2=1 & diagDir2=4)|(linhaCima2=1 & diagEsq2=4)|(linhaBaixo2=1 & diagEsq2=4)) : case
		turno = TRUE : 0;
		turno = FALSE : 3;
		TRUE : tabuleiro[1][4];
	esac;
TRUE : tabuleiro[1][4];
esac;
			
next(tabuleiro[2][1]) := case
	estado = andando & ((linhaCima=2 & diagDir=1)|(linhaBaixo=2 & diagDir=1)|(linhaCima=2 & diagEsq=1)|(linhaBaixo=2 & diagEsq=1)): case	
		turno = TRUE : {0,1};
		turno = FALSE : {3,0};
		TRUE : tabuleiro[2][1];
	esac;
					
	estado = comendo & ((linhaCima2=2 & diagDir2=1)|(linhaBaixo2=2 & diagDir2=1)|(linhaCima2=2 & diagEsq2=1)|(linhaBaixo2=2 & diagEsq2=1)): case
		turno = TRUE : 0;
		turno = FALSE : 3;
		TRUE : tabuleiro[2][1];	
	esac;
TRUE : tabuleiro[2][1];
esac;			
		
next(tabuleiro[2][3]) := case
	estado = andando & ((linhaCima=2 & diagDir=3)|(linhaBaixo=2 & diagDir=3)|(linhaCima=2 & diagEsq=3)|(linhaBaixo=2 & diagEsq=3)): case
		turno = TRUE : {0,1};	
		turno = FALSE : {0,3};
		TRUE : tabuleiro[2][3];
	esac;
	
	estado = comendo & ((linhaCima2=2 & diagDir2=3)|(linhaBaixo2=2 & diagDir2=3)|(linhaCima2=2 & diagEsq2=3)|(linhaBaixo2=2 & diagEsq2=3)) : case
		turno = TRUE : 0;
		turno = FALSE : 3;
		TRUE : tabuleiro[2][3];
	esac;
TRUE : tabuleiro[2][3];
esac;	

next(tabuleiro[3][2]) := case
	estado = andando & ((linhaCima=3 & diagDir=2)|(linhaBaixo=3 & diagDir=2)|(linhaCima=3 & diagEsq=2)|(linhaBaixo=3 & diagEsq=2)) : case
		turno = TRUE : {0,1};
		turno = FALSE : {0,3};
		TRUE : tabuleiro[3][2];
	esac;
	
	estado = comendo & ((linhaCima2=3 & diagDir2=2)|(linhaBaixo2=3 & diagDir2=2)|(linhaCima2=3 & diagEsq2=2)|(linhaBaixo2=3 & diagEsq2=2)) : case
		turno = TRUE : 1;
		turno = FALSE : 0;
		TRUE : tabuleiro[3][2];
	esac;
TRUE : tabuleiro[3][2];
esac;

next(tabuleiro[3][4]) := case
	estado = andando & ((linhaCima=3 & diagDir=4)|(linhaBaixo=3 & diagDir=4)|(linhaCima=3 & diagEsq=4)|(linhaBaixo=3 & diagEsq=4)): case
		turno = TRUE : {0,1};
		turno = FALSE : {0,3};
		TRUE : tabuleiro[3][4];
	esac;
	
	estado = comendo & ((linhaCima2=3 & diagDir2=4)|(linhaBaixo2=3 & diagDir2=4)|(linhaCima2=3 & diagEsq2=4)|(linhaBaixo2=3 & diagEsq2=4)): case
		turno = TRUE : 1;
		turno = FALSE : 0;
		TRUE : tabuleiro[3][4];
	esac;
TRUE : tabuleiro[3][4];
esac;	

next(tabuleiro[4][1]) := case
	estado = andando & ((linhaCima=4 & diagDir=1)|(linhaBaixo=4 & diagDir=1)|(linhaCima=4 & diagEsq=1)|(linhaBaixo=4 & diagEsq=1)): case	
		turno = TRUE : 1;
		turno = FALSE : {3,0};
		TRUE : tabuleiro[4][1];
	esac;
	
	estado = comendo & ((linhaCima2=4 & diagDir2=1)|(linhaBaixo2=4 & diagDir2=1)|(linhaCima2=4 & diagEsq2=1)|(linhaBaixo2=4 & diagEsq2=1)): case
		turno = FALSE : 0;
		TRUE : tabuleiro[4][1];
	esac;
TRUE : tabuleiro[4][1];
esac;	
		
next(tabuleiro[4][3]) := case
	estado = andando & ((linhaCima=4 & diagDir=3)|(linhaBaixo=4 & diagDir=3)|(linhaCima=4 & diagEsq=3)|(linhaBaixo=4 & diagEsq=3)): case	
		turno = TRUE : 1;
		turno = FALSE : 0;
		TRUE : tabuleiro[4][3];
	esac;
			
	estado = comendo & ((linhaCima2=4 & diagDir2=3)|(linhaBaixo2=4 & diagDir2=3)|(linhaCima2=4 & diagEsq2=3)|(linhaBaixo2=4 & diagEsq2=3)): case
		turno = TRUE : 1;
		turno = FALSE : 0;
		TRUE : tabuleiro[4][3];
	esac;
TRUE : tabuleiro[4][3];
esac;								
		
					

SPEC
	EF(estado = andando)