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. [desafio] “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".

Considere um simples jogo de maior dado com dois jogadores, em que cada um rola um dado de 6 faces. Se o dado do jogador 1 for maior do que o do jogador 2, o jogador 1 vence e o jogador 2 perde - e vice versa. Se os dados são iguais, eles jogam novamente até desempatar. Responda às seguintes questões:

type Status =
  Pendente | Venceu(int)

var dado1: int
var dado2: int
var status: Status

action init = {
  nondet d1 = 1.to(6).oneOf()
  nondet d2 = 1.to(6).oneOf()
  all {
    dado1' = d1,
    dado2' = d2,
    status' = (???)
  }
}

action step = {
  if (status == Pendente) {
    init
  } else {
    all {
      dado1' = dado1,
      dado2' = dado2,
      status' = status,
    }
  }
}

EXTENDS Integers, FiniteSets
VARIABLES dado1, dado2, status

Init ==
  \E d1 \in 1..6:
     \E d2 \in 1..6:
       /\ dado1 = d1
       /\ dado2 = d2
       /\ status = (???)

Next ==
  IF (status = "pendente") THEN
    \E d1 \in 1..6:
       \E d2 \in 1..6:
         /\ dado1' = d1
         /\ dado2' = d2
         /\ status' = (???)
  ELSE
    /\ dado1' = dado1
    /\ dado2' = dado2
    /\ status' = status

1. Escreva a expressão que deveria estar em (???). PS: Em TLA+, ele aparece duas vezes, mas a expressão em ambos os casos é a mesma.

   [Resposta]

   Quint: if (d1 > d2) Venceu(1) else if (d2 > d1) Venceu(2) else Pendente ou TLA+: IF d1 > d1 THEN "1 venceu" ELSE IF d2 > d1 THEN "2 venceu" ELSE "pendente"

2. Escreva uma invariante para “O jogador 1 não perde”. Essa invariante é satisfeita nesse modelo? Justifique.

   [Resposta]

   dado1 >= dado2 ou status != Venceu(2) (Quint) / status # "2 venceu" (TLA+)

3. Escreva outras duas invariantes quaisquer sobre as variáveis desse modelo. Uma delas deve ser satisfeita nesse modelo, e outra não. Indique qual é satisfeita e qual não é.

   [Resposta]

   Satisfeita: dado1 + dado2 < 20 Insatisfeita: dado1 > 2

4. Escreva uma propriedade temporal de vivacidade para esse jogo. Ela deve ser satisfeita. Considere que razoabilidade já foi devidamente assumida.

   [Resposta]

   eventually(dado1 != dado2) / <>(dado1 # dado2)

5. Esse modelo se classifica como uma estrutura de Kripke? Justifique.

   [Resposta]

   Sim, pois cada estado tem ao menos uma possível transição (a relação de transição é total).

Observe as epecificações a seguir e responda às perguntas.

var x: int

action init = {
  nondet v = Set(1, 5).oneOf()
  x' = v
}

action step = any {
  all {
    x == 5,
    x' = 4,
  },
  all {
    x < 3,
    x' = 2,
  },
  all {
    x < 5,
    x' = x,
  }
}

VARIABLE x

Init == x \in {1, 5}

Next ==
  \/ /\ x = 5
     /\ x' = 4
  \/ /\ x < 3
     /\ x' = 2
  \/ /\ x < 5
     /\ x' = x

1. Defina uma estrutura de Kripke para esse modelo. Todos os estados da estrutura devem ser alcançáveis.

   [Resposta]

   (S, ->, I) tal que:

   S = {1, 2, 4, 5}

   -> = {1 -> 1, 1 -> 2, 2 -> 2, 4 -> 4, 5 -> 4}

   I = {1, 5}

2. Essa estrutura de Kripke é determinística ou não-determinística? Justifique sua resposta para cada estado/regra.

   [Resposta]

   Não-determinística, pois \(Post(1) = \{1, 2\}\) e \(|I| = 2\)

3. Essa estrutura de Kripke é finita? Justifique sua resposta.

   [Resposta]

   Finita, porque o número de estados é finito.

4. Quais são os estados terminais dessa estrutura de Kripke?

   [Resposta]

   2 e 4

5. Qual a pré-condição da ação de próximo estado (step em Quint ou Next em TLA+)?

   [Resposta]

   x <= 5

6. Modifique o modelo (Quint ou TLA+) para que haja transições do estado onde x é 2 para todos os estados da estrutura de Kripke.

   [Resposta]

   Quint:

      action step = any {
        ...,
        all {
          x == 2,
          nondet v = Set(1, 2, 4, 5).oneOf()
          x' = v
        }
      }
   

   TLA+:

      Next ==
        \/ ...
        \/ /\ x == 2
           /\ \E v \in {1, 2, 4, 5} : x' = v