Vamos corrigir juntos usando a REPL.

x’ = x + 1 na REPL

>>> var x: int

>>> x' = 0
true
>>> x
0
>>> action step = x' = x + 1

>>> step
true
>>> step
true
>>> x
2

Sempre podemos definir operadores, valores e ações dentro do próprio corpo de outra definição. Semelhante ao let do Haskell.

• Para isso, basta escrever a(s) definição(ões) seguidas por fim da expressão final a ser retornada.
  
  • Sem separar com vírgula!
    

pure def f(x) = {
  pure def quadrado(y) = y * y
  pure def dobro(y) = 2 * y
  quadrado(x) + dobro(x)
}

As chaves {} são opcionais, e você pode usar elas quando quiser pra deixar mais claro o escopo, por exemplo:

val foo = pure def f(x) = 2 * x { f(5) }

Ações são expressões booleanas que podem incluir o operador primed (').

Contudo, não podemos usar os operadores booleanos normais sobre essa expressão. Quint não permite isso para evitar possíveis confusões. Por exemplo, as seguintes operações não são permitidas:

• not(x' = 1)
  
• x' = 1 or x' = 2
  
• x' > 1 and x' < 2
  
• Set(1, 2, 3).exists(i ==> x' = i)
  

Os equivalentes em TLA+ são permitidos. Em Quint, somos forçados a escrever as ações de um jeito específico, de uma forma que elas não possam ser confundidas com não-ações.

• Em vez de and, usamos all
  

    action incrementa_x_e_y = all {
      x' = x + 1,
      y' = y + 1,
    }
  

• Em vez de or, usamos any
  

    action incrementa_ou_decrementa_x = any {
      x' = x + 1,
      x' = x - 1,
    }
  

• Em vez de exists, usamos nondet e oneOf
  

    action x_recebe_algum_valor = {
      nondet valor = Set(1, 2, 3).oneOf()
      x' = valor
    }
  

• Importante: O oneOf só pode ser usado nesse cenário (dentro de uma ação, em uma definição do tipo nondet, sem operações adicionais sobre ele).
  

  • A syntaxe em Quint é dessa forma para deixar o não-determinismo explícito, mas na lógica (TLA), isso ainda é um exists.
    
  • Por exemplo, não é possível usar o oneOf na implementação de uma função, i.e. para encontrar o máximo em um conjunto.
    

• O if não tem uma versão especial pra ações. Usamos ele normalmente.
  

    action incrementa_x_se_par = {
      if (x % 2 == 0) {
        x' = x + 1
      } else {
        x' = x
      }
    }
  

Todas as ações em Quint devem ser devidamente balanceadas, e uma variável nunca pode ser atualizada mais de uma vez em uma mesma ação.

Isso significa que:

• Todas as ações em um any devem atualizar as mesmas variáveis
  

• Em um if, os blocos then e else devem atualizar as mesmas variáveis
  

• Em um all, as variáveis atualizadas por cada ação não podem se repetir
  

Essas restrições valem pra TLA+ também, mas em TLA+ isso só será detectado na hora de rodar o model checker. Em Quint, vocês vão ver sublinhados vermelhos no editor.

Os exemplos a seguir não são permitidos no Quint. PS: Para vê-los no editor, você precisa declarar as variáveis (var x: int e var y: int).

action any_desbalanceado = any {
  x' = 1,
  y' = 2,
}

action if_desbalanceado = {
  if (x > 0) {
    x' = 1
  } else {
    y' = 2
  }
}

Os exemplos a seguir não são permitidos no Quint.

action all_multiplas_atualizacoes = all {
  x' = 1,
  x' = 2,
}

action a1 = x' = 1
action a2 = x' = 2
action all_multiplas_atualizacoes = all { a1, a2 }

Percebam como nas últimas aulas conversamos sobre coisas um tanto diferentes:

• Aula passada, definimos
  
  • operadores com def e pure def
    
  • valores com val e pure val
    
• Nessa aula, usaremos ações com action
  

Primeiramente, temos a diferença entre val e def

• val (ou pure val): Valores, onde não há nenhum parâmetro.
  
• def (ou pure def): Operadores, onde há pelo menos um parâmetro.
  

Esses são os modos das definições. Eles definem o tanto de acesso que as definições tem às variáveis.

• pure def e pure val: Nenhum acesso. Como funções puras, onde o mesmo input vai sempre gerar o mesmo output.
  
• def e val: Leitura.
  
• action: Escrita e Leitura.
  

Além destes, temos alguns modos adicionais:

• nondet: Para declarações com não determinismo (que usam oneOf).
  
• temporal: Para fórmulas temporais.
  
• run: Para execuções mais específicas, permitindo operadores que ajudam a definir o passo a passo esperado.
  

• Você tem dois jarros:
  
  1. um grande, com capacidade de 5 litros
     
  2. um pequeno, com capacidade de 3 litros
     
• Você tem uma torneira de água com capacidade infinita
  
• Você pode descartar água a qualquer momento
  
• É possível, com precisão, ter uma medida de 4 litros de água?
  

Tente escrever as ações abaixo, definindo os valores para grande e pequeno em cada uma delas. Nenhuma dessas ações precisa de parâmetros.

  action enche_grande
  action enche_pequeno
  action esvazia_grande
  action esvazia_pequeno
  action grande_pro_pequeno
  action pequeno_pro_grande

quint -r jarros.qnt::jarros

Comece com init, e verifique os valores de grande e pequeno. Depois, tente invocar as outras ações, lembrando que o objetivo é chegar em um estado onde um dos jarros tem 4 litros.

Agora, vamos usar o model checker para encontrar a solução. Para isso, vamos definir:

• step, a ação de próximo estado. A cada passo, podemos tomar qualquer uma das ações definidas.
  
• inv, nossa invariante. Nesse caso, esperamos que a invariante seja quebrada, para obter nossa solução como contraexemplo.
  

  action step = any {
    enche_grande,
    enche_pequeno,
    esvazia_grande,
    esvazia_pequeno,
    grande_pro_pequeno,
    pequeno_pro_grande,
  }

  val inv = grande != 4

• Representação de uma execução finita.
  
  • Pode ser uma execução concreta, ou
    
  • Pode ter não determinismo, representando mais de uma execução
    
• Descreve como reproduzir uma ou mais execuções, se possível
  

Essa é uma feature exclusiva do Quint, e não há uma representação equivalente em TLA+.

• Em TLA+, só podemos usar o estado em si para determinar cada passo a ser dado.
  
• Em Quint, as runs permitem definir isso externamente, sem necessidade de manipular o estado.
  

O propósito de runs está relacionado a testes, e não tem função alguma para o model checker.

  run solution =
    init
      .then(enche_grande)
      .then(grande_pro_pequeno)
      .then(esvazia_pequeno)
      .then(grande_pro_pequeno)
      .then(enche_grande)
      .then(grande_pro_pequeno)
      .expect(grande == 4)

Adicionando o expect no final, essa run também funciona como um teste