EspecificacaoD20.als

/*
As principais relações foram baseadas no esquema do banco de dados que desenvolvemos para aplicação.
Alguns detalhes foram considerados não relevantes para a espeficicação formal, apesar de fundamentais para a
lógica de negócios, como o fato de que Tipos e Generos são ENUMs específicos. Torná-los genéricos não prejudica a análise lógica!
Campos de dados como "nomes", "emails", etc, também não foram considerados. Somente as relações entre modelos significantes 
(Usuário, Conta, Jogo..) foram especificados.
*/

-------------------------------------------------------
----------------------------- A S S I N A T U R A S  |
-------------------------------------------------------

sig Perfil, Conta {}

sig Usuario {
	conta: one Conta,
	perfil: one Perfil,
	anuncios: set Anuncio
}

sig Tipo, Genero {}

sig Jogo {
	tipo: one Tipo,
	genero: one Genero
}

sig Anuncio {
	jogo: one Jogo
}

sig Aluguel {
	locador: one Usuario,
	locatario: one Usuario,
	jogoAnunciado: one Anuncio
}


----------------------------------------------
----------------------------- F A T O S |
----------------------------------------------


fact regrasDeUsuario {
	//  Toda Conta, Perfil e Anúncio de um Usuário deve pertencer somente a ele
	all c:Conta | one conta.c
	all p:Perfil | one perfil.p
	all an:Anuncio | one anuncios.an

	// Um Usuário só pode ser locador de um Aluguel por vez
	all u:Usuario | one locador.u
}

fact regrasDeAluguel {
	// Um Usuário não pode alugar de si mesmo
	all al:Aluguel | al.locador != al.locatario
	
	// O jogo anunciado deve estar entre os Anúncios do locador
	all al:Aluguel | al.jogoAnunciado in al.locador.anuncios
	
	// Dois Alugueis não pode ter o mesmo Anúncio envolvido
	all an:Anuncio | one jogoAnunciado.an
}

------------------------------------------------------------
----------------------------- P R E D I C A D O S |
------------------------------------------------------------

-------------- Predicados de Anúncio ------------
pred usuarioTemAnuncio[u:Usuario, a:Anuncio] {
	a in u.anuncios
}

pred usuarioNaoTemAnuncio[u:Usuario, a:Anuncio]{
	not (a in u.anuncios)
}

pred adicionarAnuncio[u, u':Usuario, a:Anuncio] {
	u'.anuncios = u.anuncios + a
}
pred removerAnuncio[u,u':Usuario, a:Anuncio] {
	u'.anuncios = u.anuncios - a
}

------------ Predicados de Aluguel -----------------
pred usuarioNaoAlugou[loc:Usuario, aluguel:Aluguel] {
	aluguel.locador != loc
}

pred usuarioAlugou[loc:Usuario, aluguel:Aluguel] {
	aluguel.locador = loc
}

pred realizarAluguel [loc:Usuario, anuncio:Anuncio, aluguel:Aluguel] {
	aluguel.locador = loc
	aluguel.locatario = anuncio.~anuncios
	aluguel.jogoAnunciado.jogo = anuncio.jogo
}

pred finalizarAluguel [aluguel:Aluguel] {
	#aluguel.locador = 0
}

// O predicado mais simples. Mostra uma instância das assinaturas sem nenhuma condição.
pred show {}

------------------------------------------
------------------------- A S S E R T S |
------------------------------------------

// Todo locataráo tem algum anúncio
assert locatariosTemAnuncios {
	all al:Aluguel | some al.locador.anuncios
}

// Verificação da operação de adição de anúncio
assert usuarioAdicionouAnuncio {
	all u, u':Usuario, a:Anuncio | usuarioNaoTemAnuncio[u, a] and adicionarAnuncio[u, u', a] => usuarioTemAnuncio[u', a]
}

// Verificação da operação de remoção de anúncio
assert usuarioRemoveuAnuncio {
	all u, u':Usuario, a:Anuncio | usuarioTemAnuncio[u, a] and removerAnuncio[u, u', a] => usuarioNaoTemAnuncio[u', a]
}

// Verificação da operação de aluguel de um jogo
assert usuarioAlugouJogo {
	all u:Usuario, an:Anuncio, al:Aluguel | usuarioNaoAlugou[u, al] and realizarAluguel[u, an, al] => usuarioAlugou[u, al]
}

// Verificação da operação de devolução de um jogo
assert usuarioDevolveuJogo {
	all u:Usuario, al:Aluguel | usuarioAlugou[u, al] and finalizarAluguel[al] => usuarioNaoAlugou[u, al]
}

------------------------------------------
--------------------------- C H E C K S |
------------------------------------------

check locatariosTemAnuncios for 20

check usuarioAdicionouAnuncio for 20
check usuarioRemoveuAnuncio for 20

check usuarioAlugouJogo for 20
check usuarioAlugouJogo for 20

------------------------------------------
---------------------------------- R U N |
------------------------------------------

run show for 20