O SISTEMA OPERA

/* BIBLIOTECA

* Author: Italo

* Creation date: 05/10/2021

*/

MACHINE

BIBLIOTECA (USUARIO, LIVRO, ANAIS, REVISTAS)

VARIABLES

usuarios, livros, anais, revistas, emprestimo, limite

INVARIANT

livros : POW(LIVRO) &

usuarios : POW(USUARIO) &

anais : POW(ANAIS) &

revistas : POW(REVISTAS) &

limite : NAT1 &

emprestimo : livros +-> usuarios

INITIALISATION

livros, anais, revistas, usuarios, emprestimo, limite := {}, {}, {}, {}, {}, 3

SETS

AVISO = {SUCESSO, FALHA}

OPERATIONS

resp <-- inserirUsuario (novo_usuario) =

PRE

novo_usuario : USUARIO &

novo_usuario /: usuarios

THEN

CHOICE

usuarios := usuarios \/ {novo_usuario} ||

resp := SUCESSO

OR

resp := FALHA

END

END;

resp <-- removerUsuario (novo_usuario) =

PRE

novo_usuario : USUARIO &

novo_usuario : usuarios

THEN

CHOICE

usuarios := usuarios - {novo_usuario} ||

resp := SUCESSO

OR

resp := FALHA

END

END;

resp <-- inserirLivro (novo_livro) =

PRE

novo_livro : LIVRO & novo_livro /: livros

THEN

CHOICE

livros := livros \/ {novo_livro} ||

resp := SUCESSO