Identifique em quais estruturas de Kripke a seguir tem não-determinismo e justifique sua resposta.

1. 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.

2. 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.

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.

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.

1. Fórmula: \(X(b)\)
   • [ ] \([b], [b], [a]\)
   • [ ] \([a], [b], [a]\)
   • [ ] \([a], [a], [b]\)
2. Fórmula: \(a -> b\)
   • [ ] \([a], [a], [a]\)
   • [ ] \([a], [b], [a]\)
   • [ ] \([a, b], [a], [a]\)
   • [ ] \([b], [a], [a]\)
3. Fórmula: \(F(a)\)
   • [ ] \([a], [a], [a]\)
   • [ ] \([b], [a], [b]\)

Explique a diferença entre LTL (Lógica Temporal Linear) e CTL (Lógica de árvore computacional - Computational Tree Logic).

Assinale as fórmulas abaixo com [V] (verdadeiro) se a propriedade pode ser espressa com uma invariante ou [F] (falso) caso seja preciso uma fórmua temporal. 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

Leia a contextualização e responda:

Estou vendendo peças de computador e contrato uma transportadora para fazer as entregas. Essas peças são frágeis, e podem quebrar se não forem transportadas de maneira adequada. A caixa não pode ser virada (a mesma face deve permanecer para cima durante todo o transporte), e não pode se mover no baú do caminhão. Para ter certeza de que a transportadora está fazendo seu serviço corretamente, instalei câmeras internas nos baús dos caminhões que me enviam fotos a cada 5 minutos. Agora, só preciso analisar essas fotos e determinar se a transportadora cumpre os requisitos.

Considerando uma execução dada pela sequência de fotos enviadas, escreva propriedades de segurança e vivacidade que digam sobre a qualidade do serviço da transportadora. Informe o tipo (invariante/temporal e segurança/vivacidade) de cada propriedade. Liste também que tipo de suposições estão sendo feitas para viabilizar essa análise.

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.

1. 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.

2. 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

3. 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.

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

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:

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 = 10

Next ==
  \/ /\ x < 20
     /\ x % 2 = 0
     /\ x' = x + 3
  \/ /\ x > 5
     /\ x' = x - 1

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

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

Agora escreva a propriedade em Quint ou em TLA+ para:

1. “Não é possível estar na aula e no shopping ao mesmo tempo”. Considere que existam duas variáveis de estado do tipo bool: na_aula e no_shopping.
2. “Sempre uso óculos para dirigir”. Considere que existam duas variáveis de estado do tipo bool: estou_dirigindo e estou_de_oculos.
3. “Em algum momento vou terminar de pagar as parcelas do meu apartamento”. Considere que exista uma variável de estado do tipo int para o número restante de parcelas: parcelas_restantes.
4. “Todos os códigos em C++ serão migrados para Rust”. Considere que exista uma variável codigos do tipo int -> { codigo: str, linguagem: str } sendo a chave (domínio) um identificador único daquele código e o campo linguagem pode conter "c++", "haskell" ou "rust".