Please enable JavaScript.
Coggle requires JavaScript to display documents.
Refinamento de Não Determinismo - Coggle Diagram
Refinamento de Não Determinismo
Não determinismo pode ser usado na inicialização ou nas operações.
Refinar não determinismo
Ref1
Definir a escolha não determinística, fornecendo uma determinística.
x :: NATURAL :arrow_right: xx := 0
Ref2
No refinamento a máquina pode continuar não determinística, o objetivo é que ela se torne, no mínimo, menos não determinística.
xx :: NATURAL :arrow_right: CHOICE xx := 0 OR xx := 1 END;
Ref3
Também pode ser um algoritmo.
xx :: NATURAL :arrow_right: IF yy = 0 THEN xx : (xx /= yy) [...] END;
Exemplos
Exemplo #1
Registrar um conjunto de números que forma usados.
Op1
Adicionar um determinado número não usado.
Op2
Consultar se um determinado número foi usado.
Op3
Adicionar qualquer número não usado.
Refinamento
Remove o não determinismo da Op3 transformando-a em uma operação que adiciona o menor número ainda não usado.
Conceitos
O estado resultante da execução de uma operação em um refinamento devem coincidir com algum dos estados resultantes na máquina abstrata.
Exemplo #2
Registra um conjunto de valores com capacidade limitada.
Op1
Adicionar um dado elemento.
Op2
Remover qualquer elemento.
Conceitos
As transições de estado no refinamento corresponde a alguma transição de estado da máquina abstrata.
Refinamento
Remove o não determinismo da Op2 transformando-a para remover o último elemento.
Exemplo #3
Armazena o conjunto de livros que foram lidos.
Op1
Retorna um novo livro e o adiciona no conjunto de livros lidos.
Refinamento #1
Mapear os livros não lidos em uma sequência.
Transformar Op1 para sempre retornar o primeiro livro da sequência.
Possui não determinismo na inicialização.
Refinamento #2
Mapear todos os livros em um array.
Armazenar a quantidade de livros lidos.
Transformar Op1 para sempre retornar o livro que está na posição da quantidade de livros lidos.
Completamente determinística.
Conceitos
Transitividade de Refinamento
Se R2 refina R1 e R1 refina R, então R2 refina R.
Pré-condições são implícitas nos refinamentos.
Exemplo #4
Jukebox
Op1
Comprar créditos.
Op2
Adiciona uma música na fila.
Consome ou não um crédito.
Op3
Escolhe uma música da fila para ser tocada.
Op4
Remove um crédito, caso tenha disponível.
Ou remove uma música da fila, caso a fila não seja vazia.
Refinamento
Mapeia a fila de músicas em uma sequência.
Cria uma constante que representa a quantidade de músicas que devem ser tocadas consumindo crédito até que seja possível tocar uma música sem consumir créditos.
Refina Op2 para tornar possível a escolha de não consumir apenas quando a quantidade de músicas tocadas gastando crédito for alcançada.
Refina Op3 para tocar sempre a primeira música da fila.
Refina Op4 para se a fila não for vazia, remover a primeira música ou se tiver crédito, remover um crédito.
Menos não determinística que a máquina original.