Exercícios para a prova
Estruturas de Kripke
Questão 1
Identifique em quais estruturas de Kripke a seguir tem não-determinismo e justifique sua resposta.
Semáforos. Considere o conjunto de estados inicial \(I = \{vermelho\}\)
[Resposta]
Determinístico (não há não-determinismo), porque existe somente um estado inicial e, para cada um dos três estados, há apenas uma possível transição.
Chaleira. Considere o conjunto de estados inicial \(I = \{temperatura\_ambiente\}\)
[Resposta]
Não-determinístico (há não-determinismo), porque, para os estados “esquentando” e “esfriando”, há mais de uma transição possível.
Questão 2
Defina uma estrutura de Kripke para um sistema de caixa da água com as seguintes características:
- A caixa da água contém uma bóia que impede que ela transborde, ou seja, a bóia interrompe o enchimento quando a caixa está completamente cheia.
- A caixa não enche enquanto está sendo usada, ou seja, ela não pode estar enchendo e esvaziando ao mesmo tempo.
- Se a caixa está vazia, ela não pode ser esvaziada.
- O sistema inicia com a caixa vazia
PS: Tente usar o mínimo de estados e transições necessários para representar esse sistema.
[Resposta]
- \(S = \{vazia, enchendo, cheia, esvaziando\}\)
- \(\rightarrow = \{vazia \rightarrow enchendo, enchendo \rightarrow esvaziando, enchendo \rightarrow cheia, cheia \rightarrow esvaziando, esvaziando \rightarrow enchendo, enchendo \rightarrow vazia\}\)
- \(I = \{vazia\}\)
Lógica temporal
Questão 3
Dada uma fórmula temporal e uma execução, indique se a fórmula é verdadeira ou falsa para a execução. Ou seja, responda verdadeiro se a execução satisfaz a fórmula e falso caso não satisfaça. Considere que \(a\) e \(b\) são proposições.
- Fórmula: \(X(b)\)
[ ]\([b], [b], [a]\)[ ]\([a], [b], [a]\)[ ]\([a], [a], [b]\)
- Fórmula: \(a -> b\)
[ ]\([a], [a], [a]\)[ ]\([a], [b], [a]\)[ ]\([a, b], [a], [a]\)[ ]\([b], [a], [a]\)
- Fórmula: \(F(a)\)
[ ]\([a], [a], [a]\)[ ]\([b], [a], [b]\)
[Resposta]
- Fórmula: \(X(b)\)
- [V] \([b], [b], [a]\)
- [V] \([a], [b], [a]\)
- [F] \([a], [a], [b]\)
- Fórmula: \(a -> b\)
- [F] \([a], [a], [a]\)
- [F] \([a], [b], [a]\)
- [V] \([a, b], [a], [a]\)
- [V] \([b], [a], [a]\)
- Fórmula: \(F(a)\)
- [V] \([a], [a], [a]\)
- [V] \([b], [a], [b]\)
Questão 4
Explique a diferença entre LTL (Lógica Temporal Linear) e CTL (Lógica de árvore computacional - Computational Tree Logic).
[Resposta]
A representação de árvore da CTL permite que usemos quantificações existenciais com nossas fórmulas temporais: existe alguma execução onde eventualmente X. Já na LTL, todas as fórmulas são implicitamente universalmente quantificadas, e isso não é possível. Essa diferença faz com que existam fórmulas na LTL que não podem ser espressadas em CTL e fórmulas na CTL que não podem ser espressadas na LTL.
Propriedades
Questão 5
Assinale as fórmulas abaixo com [I] - Invariante ou [V] - Vivacidade (Propriedade de Vivacidade ou Liveness Property). Lembre-se que não importa se a fórmula é verdadeira ou falsa.
[ ]Para cada compra no cartão de crédito, vem uma cobrança na fatura ao final do mês.[ ]Nunca vou para a academia sem meus fones de ouvido[ ]Em algum momento vou terminar de pagar as parcelas do meu apartamento[ ]Sempre uso óculos para dirigir[ ]Não é possível estar na aula e no shopping ao mesmo tempo[ ]Todos os códigos em C++ serão migrados para Rust
[Resposta]
- [V] Para cada compra no cartão de crédito, vem uma cobrança na fatura ao final do mês.
- [I] Nunca vou para a academia sem meus fones de ouvido
- [V] Em algum momento vou terminar de pagar as parcelas do meu apartamento
- [I] Sempre uso óculos para dirigir
- [I] Não é possível estar na aula e no shopping ao mesmo tempo
- [V] Todos os códigos em C++ serão migrados para Rust
Assumptions
Questão 6
Alice e Bob estavam combinando de se encontrar e Alice mandou a seguinte mensagem para Bob: “Encontre-me as 15h na cafeteria Café Quentinho”. Ao fazer essa comunicação, Alice estava supondo algumas coisas. Descreva qual suposição de Alice estava errada para cada um dos cenários a seguir.
Bob não apareceu. A bateria do celular dele acabou antes que visse a mensagem de Alice. Responda: Alice assumiu que …
[Resposta]
Alice assumiu que Bob havia recebido a mensagem dela.
Bob foi em outro Café Quentinho - acontece que havia outra cafeteria com esse nome em outro bairro. Responda: Alice assumiu que …
[Resposta]
Alice assumiu que havia apenas uma “Café Quentinho” na cidade
Quando Alice chegou, o Bob já estava lá por uma hora. Ele havia esquecido de ajustar seu relógio no fim do horário de verão. Responda: Alice assumiu que …
[Resposta]
Alice assumiu que o relógio de Bob estava no mesmo horário que o dela.
Perguntas gerais
Questão 7
Suponha que temos um modelo e uma propriedade que é violada numa execução de 5 passos. Considere que estamos usando um simulador aleatório com até 10.000 amostras e 10 passos, e um model checker com até 10 passos. Assinale com verdadeiro ou falso e justifque sua resposta.
[ ]O simulador irá encontar um contraexemplo para propriedades[ ]O model checker encontrará um contraexemplo de 5 passos[ ]O model checker demorará mais tempo que o simulador para responder[ ]O simulador demorará mais tempo que o model checker para responder[ ]O model checker poderá finalizar a execução sem encontrar o contraexemplo[ ]O simulador pode encontrar um contraexemplo de 9 passos
[Resposta]
- [F] O simulador irá encontar um contraexemplo para propriedades
- [V] O model checker encontrará um contraexemplo de 5 passos
- [F] O model checker demorará mais tempo que o simulador para responder
- [F] O simulador demorará mais tempo que o model checker para responder
- [F] O model checker poderá finalizar a execução sem encontrar o contraexemplo
- [V] O simulador pode encontrar um contraexemplo de 9 passos
TLA+ e Quint
Questão 8
Dada uma especificação simples, escreva uma breve descrição do que ela faz. Observe o seguinte exemplo: Quint:
var x: int action init = x' = 0 action step = x' = if (x < 10) x + 1 else x
TLA+:
VARIABLE x Init == x = 0 Next == x' = IF (x < 10) THEN x + 1 ELSE x
Poderíamos descrever como: Um modelo onde x começa em zero e é incrementado até chegar a 10, com incrementos de tamanho 1. Ao chegar a 10, x permanece com o mesmo valor pra sempre
Agora, responda com uma descrição para cada especificação abaixo:
Especificação A
Quint:
var x: int action init = x' = 0 action step = any { all { x < 5, x' = x + 1 }, all { x > -5, x' = x - 1 } }
TLA+
VARIABLE x Init == x = 0 Next == \/ /\ x < 5 /\ x' = x + 1 \/ /\ x > -5 /\ x' = x - 1
[Resposta]
Um modelo onde x começa em zero e pode ser incrementado em 1 caso seja menor que 5, ou decrementado em 1 caso seja maior que -5. Ou seja, a cada passo x terá seu valor modificado (mais um ou menos um) e permanecerá sempre entre -5 e 5.
Especificação B
Quint:
var x: int action init = x' = 1 action step = { nondet v = 1.to(10).oneOf() all { x != v, x' = v } }
TLA+:
VARIABLE x Init == x = 1 Next == \E v \in 1..10: /\ x /= v /\ x' = v
[Resposta]
Um modelo onde x começa em 1 e a cada passo recebe um novo valor, diferente do atual, entre 1 e 10.
Questão 9
Considere o modelo a seguir:
Quint:
var x: int action init = x' = 10 action step = any { all { x < 20, x % 2 = 0, x' = x + 3 }, all { x > 5, x' = x - 1 } }
TLA+:
VARIABLE x Init == x = 1 Next == \E v \in 1..10: /\ x /= v /\ x' = v
Para cada execução a seguir, assinale verdadeiro se o modelo permite a execução e falso caso contrário. Quando responder falso, justifique sua resposta.
[ ]x: 7, x: 6, x: 9, x: 8[ ]x: 10, x: 13, x: 12, x: 11, x: 10[ ]x: 10, x: 9, x: 8, x: 11[ ]x: 10, x: 9, x: 12, x: 15
[Resposta]
- [F]
x: 7, x: 6, x: 9, x: 8- x não pode ser 7 no estado inicial. Deve ser 10.
- [V]
x: 10, x: 13, x: 12, x: 11, x: 10 - [V]
x: 10, x: 9, x: 8, x: 11 - [F]
x: 10, x: 9, x: 12, x: 15- não podemos somar 3 ao 9 para chegar em 12, porque uma das pré-condições para somar 3 é que x seja divisível por 2, e 9 não é.
Questão 10
O operador primed (') permite que escrevamos predicados sobre o próximo estado. Assinale verdadeiro se o operador primed está sendo usado corretamente, ou falso se o uso resultará em um erro. Caso responder falso, justifique sua resposta. Considere que x e y são variáveis. As respostas para Quint ou TLA+ são as mesmas, responda apenas uma delas.
Quint:
[ ]all { x' = 1, x' = 2 }[ ]any { x' = 1, x' = 2 }[ ]all { x' = 1, y' = 2 }[ ]any { x' = 1, y' = 2 }
TLA+:
[ ]x' = 1 /\ x' = 2[ ]x' = 1 \/ x' = 2[ ]x' = 1 /\ y' = 2[ ]x' = 1 \/ y' = 2
[Resposta]
Quint:
- [F]
all { x' = 1, x' = 2 }- x é atualizado duas vezes na mesma ação
- [V]
any { x' = 1, x' = 2 } - [V]
all { x' = 1, y' = 2 } - [F]
any { x' = 1, y' = 2 }- atualização desbalanceada: em uma das ramificações apenas x é atualizado, e em outra apenas y
TLA+:
- [F]
x' = 1 /\ x' = 2- x é atualizado duas vezes na mesma ação
- [V]
x' = 1 \/ x' = 2 - [V]
x' = 1 /\ y' = 2 - [F]
x' = 1 \/ y' = 2- atualização desbalanceada: em uma das ramificações apenas x é atualizado, e em outra apenas y