Biblioteca em CSP Disciplina: Especificação de Sistemas Distribuídos - ESD Professor: Alexandre Mota Semestre: 2014.1 Alunos: Alex Candido - aacs Jacinto Filipe - jfsr Agenda ● ● ● ● ● ● ● ● ● ● ● Introdução & Objetivo Ilustração Textual do Projeto Ilustração Visual do Projeto Principais Constantes Principais Tipos Principais Canais Principais Processos Composição do Sistema Não Determinismo (intencional) Refinamento do Não Determinismo Dificuldades Enfrentadas Introdução & Objetivo ● O objetivo deste trabalho é tentar modelar um sistema do mundo real que torne possível a aplicação prática de alguns dos conceitos vistos em sala de aula. ● O sistema escolhido foi o de uma Biblioteca, tendo em vista que esse sistema é constituído de entidades comunicantes que permitem aplicar os conceitos de concorrência e paralelismo. Ilustração Textual (p.1) ● O Usuário ao chegar na biblioteca irá procurar e pegar o livro desejado, tendo assim uma lista de livros escolhidos, que por sua vez não pode ser maior que o tamanho máximo da lista de livros. ● Após ter escolhido os livros, o Usuário pode decidir em Realizar o Empréstimo se dirigindo para o balcão, onde irá interagir com o Bibliotecário, e assim Finalizar o Empréstimo por meio de uma Autenticação, que é composta pela Validação do Usuário através da verificação do seu CPF e Senha. ● O Bibliotecário inicia a sessão e passa a aguardar pelo usuário até que o mesmo decida Realizar um Empréstimo e ele passa a atender o usuário, a ler as informações dos livros contidos no balcão usando o scanner até Finalizar o Empréstimo e então ele passar a Esperar pela Autenticação do Usuário, gerando com isso um Comprovante em caso de sucesso. Ilustração Textual (p.2) ● O Computador, por sua vez tem interação direta com o Bibliotecário, uma vez que após ter o Acervo Carregado no sistema, o Computador está sem Bibliotecário. Após ocorrer uma interação entre o Bibliotecário e um Computador iniciando uma sessão, o Computador torna-se disponível podendo Realizar um Empréstimo ou ter sua sessão encerrada, ficando o Computador sem Bibliotecário. ● Caso o Bibliotecário seja acionado Realizar um Empréstimo, o Computador entra em Utilização e irá continuar nesse estado enquanto o Bibliotecário lê as informações dos livros usando o scanner até Finalizar o Empréstimo e assim o Computador passa a esperar pela Autenticação do Usuário. ● Como mencionado anteriormente, tal validação acontece através da verificação do seu CPF e Senha. Em caso positivo, uma Resposta positiva é exibida e um comprovante será gerado, tornando o Computador disponível novamente, caso contrário, uma Resposta negativa é exibida e o Computador permanece esperando pela Autenticação. Ilustração Textual (p.3) ● O Servidor da Biblioteca é a entidade responsável por Enviar o Acervo para a Biblioteca, isso só acontece após o mesmo estar ligado, ficando Disponível. ● Uma vez que o Servidor da Biblioteca está disponível, o mesmo pode ser Desligado, pode Carregar o Acervo e por fim, Registro de Empréstimos do Computador, que nada mais é do que o somatório dos registros de empréstimos da Biblioteca mais a quantidade de empréstimo contida no comprovante. Ilustração Visual 1 (Usuário) Ilustração Visual 2 (Bibliotecário) Ilustração Visual 3 (Computador) Ilustração Visual 4 (Servidor bibl.) Principais Constantes ● ● ● ● ● ● ● ● tamanhoMaximoDoAcervo = 2 tamanhoMaximoDoComprovante = 2 tamanhoMaximoDoRegistoDeEmprestimos = 2 tamanhoMaximoDaListaDeLivros = 2 qtdBibliotecarios = 2 qtdComputadores = 2 qtdUsuarios = 2 qtdBibliotecas = 1 Principais Tipos ● ● ● ● ● ● ● ● ● ● datatype Resposta = usuarioInexistente | usuarioEncontrado Livro = {1..1} Bibliotecario = {1..qtdBibliotecarios} Computador = {1..qtdComputadores} Usuario = {1..qtdUsuarios} Biblioteca = {1..qtdBibliotecas} Acervo = union({<livro>| livro <- Livro},{<>}) Comprovante = union({<livro>| livro <- Livro},{<>}) Cpf = { getCpf(usuario) | usuario <- Usuario } Senha = { getSenha(cpf) | cpf <- Cpf } Principais Canais ● ● ● ● ● ● ● ● ● ● ● ● ● channel RealizarEmprestimo, FinalizarEmprestimo: Bibliotecario channel PegarLivro : Livro channel Balcao : Bibliotecario.Livro channel DigitarCpf, VerificacaoCpf : Bibliotecario.Cpf channel DigitaSenha, VerificacaoSenha : Bibliotecario.Cpf.Senha channel ValidarUsuario : Bibliotecario.Resposta channel Scanner : Bibliotecario.Livro channel Impressora : Bibliotecario.Comprovante channel IniciarSessao, EncerrarSessao : Bibliotecario channel LigarServidorDaBiblioteca, DesligarServidorDaBiblioteca : Biblioteca channel CarregarRegistrosDeEmprestimoDoComputador : Comprovante channel CarregarAcervo : Biblioteca.Acervo channel EnviarAcervoParaBiblioteca : Acervo Principais Processos ● ● ● ● ● ● ● ● ● ● ● ● ● ● ● USUARIO USUARIO_NO_BALCAO USUARIO_SE_AUTENTICANDO BIBLIOTECARIO BIBLIOTECARIO_AGUARDANDO_USUARIO BIBLIOTECARIO_EM_ATENDIMENTO BIBLIOTECARIO_ESPERANDO_AUTENTICACAO COMPUTADOR COMPUTADOR_SEM_BIBLIOTECARIO COMPUTADOR_DISPONIVEL COMPUTADOR_EM_UTILIZACAO COMPUTADOR_ESPERANDO_AUTENTICACAO SERVIDOR_DA_BIBLIOTECA SERVIDOR_DA_BIBLIOTECA_DISPONIVEL BD_USUARIOS_BIBLIOTECA Composição do Sistema Canais_Bibliotecario_Computador = {|IniciarSessao, EncerrarSessao,Scanner, RealizarEmprestimo, FinalizarEmprestimo, VerificacaoCpf, VerificacaoSenha, ValidarUsuario, Impressora|} Canais_Biblioteca_Servidor = {|CarregarAcervo|} Canais_Sistema_Usuario = {|RealizarEmprestimo,FinalizarEmprestimo,Balcao,DigitarCpf,DigitaSenha,ValidarUsuario|} Canais_Computador_BD = {|VerificacaoCpf,VerificacaoSenha,ValidarUsuario|} BIBLIOTECARIOS = ||| b:{1..qtdBibliotecarios}@ (BIBLIOTECARIO(b)) CONJUNTO_COMPUTADOR_BD(biblioteca) = (COMPUTADOR(biblioteca) [|Canais_Computador_BD|] BD_USUARIOS_BIBLIOTECA) CONJUNTO_BIBLIOTECARIO_COMPUTADOR(biblioteca) = (BIBLIOTECARIOS [|Canais_Bibliotecario_Computador|] CONJUNTO_COMPUTADOR_BD(biblioteca)) BIBLIOTECA(biblioteca) = (CONJUNTO_BIBLIOTECARIO_COMPUTADOR(biblioteca)[|Canais_Biblioteca_Servidor|] SERVIDOR_DA_BIBLIOTECA(biblioteca)) BIBLIOTECAS = ||| b:{1..qtdBibliotecas}@ (BIBLIOTECA(b)) USUARIOS = ||| u:{1..qtdUsuarios}@ (USUARIO(u,<1>)) SISTEMA = BIBLIOTECAS [|Canais_Sistema_Usuario|] USUARIOS Não Determinismo (intencional) ● A utilização intencional do operador de Escolha Interna possibilita a simulação se um usuário existe ou não no banco de dados dos usuários da biblioteca. BD_USUARIOS_BIBLIOTECA = VerificacaoCpf?bibliotecario?cpf -> VerificacaoSenha.bibliotecario.cpf.getSenha(cpf) -> ( ValidarUsuario.bibliotecario!usuarioEncontrado -> BD_USUARIOS_BIBLIOTECA |~| ValidarUsuario.bibliotecario!usuarioInexistente -> BD_USUARIOS_BIBLIOTECA ) Refinamento do Processo ● A utilização do operador de Escolha Externa, possibilita a remoção do comportamento Não Determínistico do processo. BD_USUARIOS_BIBLIOTECA = VerificacaoCpf?bibliotecario?cpf -> VerificacaoSenha.bibliotecario.cpf.getSenha(cpf) -> ( ValidarUsuario.bibliotecario!usuarioEncontrado -> BD_USUARIOS_BIBLIOTECA [] ValidarUsuario.bibliotecario!usuarioInexistente -> BD_USUARIOS_BIBLIOTECA ) Dificuldades Enfrentadas ● Encontrar um projeto/tema o qual fossemos capazes de elaborar dentro do prazo e grau de complexidade compatível com o nível de conhecimento da dupla. ● Realizar o mapeamento das entidades do mundo real para o virtual. ● Falta de experiência com modelagens em geral, e principalmente com a linguagem CSP. ● Entender e conseguir separar as estruturas/entidades. ● Pensar de maneira concorrente e paralela, além de compreender como as estruturas se comunicam. ● Compreender e reconhecer na prática os principais conceitos abordados durante a disciplina, como: Deadlock, Não Determinismo e Livelock.