Se você está conseguindo executar (simular) sua especificação, mas não entende porque algo está se comportando de determinada maneira, pode ser útil usar o operador auxiliar q::debug. Por exemplo, considere a função:

pure def f(x) = (x + 1) * 2

Se tivermos dúvida se nossa soma está correta, podemos envolve-la em uma chamada de q::debug, onde o primeiro argumento é uma string qualquer e o segundo a expressão a ser avaliada. O resultado de q::debug é exatamente igual à expressão em si, mas ele tem um efeito colateral que resulta na impressão daquele valor precedido pela string fornecida:

>>> pure def f(x) = q::debug("resultado soma: ", x + 1) * 2
>>> f(1)
> resultado soma:  2
4

Isso é o mais próximo que temos de printf para debugar :). Você também pode tentar usar a flag --verbosity=5 para ver em mais detalhes o que está sendo executado.

De forma semelhante, temos o operator Print em TLA+, definido no módulo TLC

EXTENDS TLC

Usado da mesma forma:

otherTeam(team) == Print("otherTeam: ", IF team = "A" THEN "B" ELSE "A")

No VSCode, no painel do TLC teremos uma seção “Output” mostrando:

"otherTeam: " "A" (6)
"otherTeam: " "B" (2)
"otherTeam: " "A" (4)
"otherTeam: " "B" (4)
"otherTeam: " "A" (2)
...

E se, no mesmo turno, um pokemon puder dar dois ataques em vez de somente um?

Lembrem-se que não podemos atualizar uma variável duas vezes na mesma ação (transição).

Temos duas opções:

1. Usar duas ações e só atualizar next_team na segunda
   
2. Usar uma unica ação, onde só atualizamos pokemons com o resultado do segundo ataque.
   

A opção (2) é geralmente mais interessante, já que ela funciona melhor se, por exemplo, quisermos adicionar um terceiro ataque.

[Exemplo completo no moodle]

type AttackDescription = { attacker: Pokemon, receiver: Pokemon, attack: str, damage: int }
var last_attack: Option[List[AttackDescription]]

pure def tackle(attacker: Pokemon, receiver: Pokemon): (Pokemon, AttackDescription) = {
  (receiver.damage(10), { attacker: attacker, receiver: receiver, attack: "Tackle", damage: 10 })
}

pure def elemental_attack(attacker: Pokemon, receiver: Pokemon): (Pokemon, AttackDescription) = {
  val base_damage = 10
  val actual_damage = match damage_modifier(attacker, receiver) {
    | SuperEffective => base_damage * 2
    | NotVeryEffective => base_damage / 2
    | Normal => base_damage
  }
  (receiver.damage(actual_damage), { attacker: attacker, receiver: receiver, attack: "Elemental", damage: actual_damage })
}

pure def attack(attacker: Pokemon, receiver: Pokemon): (Pokemon, AttackDescription) = {
  if (damage_modifier(attacker, receiver) == SuperEffective) {
    attacker.elemental_attack(receiver)
  } else {
    attacker.tackle(receiver)
  }
}

action double_attack(attacker: Pokemon, receiver: Pokemon): bool = {
  all {
    attacker != receiver,
    attacker.hp > 0,
    receiver.hp > 0,
    val first_attack_result = attacker.attack(receiver)
    val second_attack_result = attacker.attack(first_attack_result._1)
    val double_attack_description = [first_attack_result._2, second_attack_result._2]
    all {
      pokemons' = pokemons.set(receiver.team, second_attack_result._1),
      last_attack' = Some(double_attack_description)
    }
  }
}

E se precisássemos registrar o modificador de dano de ataques elementais na nossa especificação de pokemons?

• O problema aqui é que ataques do tipo tackle não tem modificador. Esse dado só existe para ataques elementais.
  

• Poderíamos colocar um valor qualquer no campo modifier quando o ataque é do tipo tackle, e lembrar que esse campo é irrelevante quando o tipo do ataque é tackle.
  

A alternativa mais elegante é usar um tipo soma para, no mesmo campo, termos tipos diferentes para um ataque elemental (aqui, um record com o modificador e o dano) e um tackle (aqui, um inteiro para o dano).

type Attack =
  | ElementalAttack({ modifier: DamageModifier, damage: int })
  | Tackle(int)
type AttackDescription = { attacker: Pokemon, receiver: Pokemon, attack: Attack }

Se quisermos deixar nossa especificação de pokemons mais completa, podemos adicionar outras ações que um pokemon pode tomar no seu turno, além de atacar. Vamos pensar somente nos tipos aqui.

type AttackDescription = ElementalAttack({ modifier: DamageModifier, damage: int }) | Tackle(int)
type Status = Attack | Defense | SpecialDefense | SpecialAttack | Speed | Accuracy | Evasiveness
type Condition = Poison | Burn | Freeze | Paralize | Sleep
type TurnDescription =
   | Attack({ attacker: Pokemon, receiver: Pokemon, attack: AttackDescription })
   | Heal({ pokemon: Pokemon, healed_amount: int })
   | Buff({ pokemon: Pokemon, status: Status })
   | Debuff({ caster: Pokemon, receiver: Pokemon, status: Status })
   | ApplyCondition({ caster: Pokemon, receiver: Pokemon, condition: Condition })
   | RemoveCondition({ pokemon: Pokemon, condition: Condition })

Em TLA+ (usando TLC), não temos tipos, então é possível usar records com diferentes campos em cada estado.
Por exemplo:

lastAttack' =[ attacker |-> p1, receiver |-> p2, attack |-> "elemental", modifier |-> "super effective", damage |-> 20]
lastAttack' = [ action |-> "buff", pokemon |-> p, status |-> "speed" ]

O nosso controle de turnos na especificação dos pokemons e do jogo da velha funciona muito bem para 2 jogadores, mas não é muito útil com mais do que isso.

action init = {
  // ...
  next_team' = if (team_A_pokemon.speed >= team_B_pokemon.speed) "A" else "B",
}

action step = {
  // ...
  next_team' = other_team(next_team),
}

Para não precisar salvar muita informação extra no estado (variáveis), uma alternativa legal é ter um contador de rounds e, a cada turno, computar quem é o jogador da vez naquele round.

var round: int

action init = all {
  pokemons' = ...,
  round' = 0,
}

action step = {
  val attackers_by_initiative = pokemons.values().toList((p1, p2) => intCompare(p2.speed, p1.speed))
  val attacker = attackers_by_initiative[round % pokemons.keys().size()]
  val receiver = pokemons.values().filter(p => attacker != p).oneOf()
  all {
    attack(attacker, receiver),
    round' = round + 1,
  }
}

val attackers_by_initiative = pokemons.values().toList((p1, p2) => intCompare(p2.speed, p1.speed))

• toList: Converte um conjunto (set) para uma lista. Precisa de um operador que indique como ordenar os elementos desse set, para que não tenhamos comportamento arbitrário.
  

• intCompare: Operador auxiliar para comparação de inteiros
  

    pure def intCompare(a: int, b:int): Ordering = {
      if (a < b)
        { LT }
      else if (a > b)
        { GT }
      else
        { EQ }
    }
  

• Para que a ordem seja descendente de acordo com a velocidade, basta inverter a ordem dos argumentos (intCompare(p2.speed, p1.speed)).
  

Para converter um conjunto em uma sequência com uma dada ordenação em TLA+, podemos usar o operador SetToSortSeq do módulo SequencesExt:

EXTENDS SequencesExt

SetToSortSeq({ [ speed |-> 10 ], [ speed |-> 20 ] }, LAMBDA r1, r2 : r1.speed > r2.speed)

Supondo que queremos aplicar 1 de dano em todos os pokemons.

Em Quint:

pokemons.transformValues(p => p.damage(1))

Em TLA+

[ team \in DOMAIN pokemons |-> damage(pokemons[team], 1) ]

A versão em Quint equivalente a essa expressão em TLA+ seria:

pokemons.keys().mapBy(team => pokemons.get(team).damage(1))

Mapas mapeiam um conjunto de chaves para seus valores.

• Na especificação dos pokemons, escolhemos indexar pokemons pelo seu time ("A" ou "B").
  

  • Ou seja, nossas chaves são times (strings), e nossos valores são pokemons.
    
  • Em Quint, o tipo do mapa é str -> Pokemon
    

• Isso foi possível porque temos apenas um pokemon por time. Se tivéssemos mais de um pokemon por time, teríamos que escolher outra chave. Por exemplo, o nome do pokemon.
  

  • Mapas são equivalentes a funções. Uma chave só pode mapear um único valor
    
  • Nesse caso, usamos time ao invés de nome por isso facilitar o acesso ao “pokemon adversário” (pokemons.get(other_team(next_team)))
    

Como indicado no enunciado do trabalho, devemos usar simuladores. Para usar o TLC no seu modo de simulação:

1. Instale a extensão do TLA+ no VSCode.
   
2. Aperte F1 e escolha: TLA+: Check model with TLC
   
   • Você deve ver um prompt para inserir opções adicionais para o TLC.
     

PS: Aconselho sempre usar a flag -deadlock para desativar checks de deadlock, já que essa não é uma preocupação para nossos sistemas de batalha.

Opções para simular até encontrar um erro, com no máximo 10 mil tentativas (semelhante ao quint run):

-deadlock -simulate num=10000

Se a propriedade for satisfeita, nenhum trace será exibido. Então, se você quiser ver um trace qualquer, use:

-deadlock -simulate file=out,num=1

Assim, o TLC irá criar um arquivo out_0_0 com um trace do modelo.

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

O operador oneOf() só pode ser usado nessa forma!

• Como parte de uma ação (action)
  
• Em uma definição do tipo nondet
  
• Sem mais operadores aplicados acima dele
  
  • (i.e. nondet valor = Set(1, 2, 3).oneOf() + 1)
    

Por que isso é importante?

• Quint obedece a lógica temporal das ações e pode ser traduzido para TLA+
  
• Se usamos oneOf() fora desse padrão, temos potencialmente definições fora da lógica, que não podem ser traduzidas para TLA+
  
• Lembrando que a versão em TLA+ para isso é o existe, cujo corpo é sempre booleano.
  

Atenção: isso significa que não é possível definir “role um d20 para cada criatura”. Vocês vão precisar definir um valor nondet para cada uma das criaturas:

action init = all {
  nondet d20_mago = // ...
  nondet d20_druida = // ...
  // ...
}