1.1 Erro no Set(1.to(20))

O próprio operador to já constrói um conjunto, assim você está fazendo um conjunto de conjuntos. O certo é 1.to(20).

1.2 Erros do tipo "Name _ not found" sendo que o nome está definido logo acima

Cuidado com o escopo dos nomes. A vírgula (,) separa escopos no Quint. Veja o exemplo:

action Foo == all {
  val a = 1,
  val b = a, // Erro aqui, "a" não está no escopo e não será encontrado
  variavel' = a + b // Erro: nem "a" nem "b" serão encontrados
}

Para corrigir, basta remover as vírgulas:

action Foo == all {
  val a = 1
  val b = a
  variavel' = a + b
}

Vamos ver um caso com mais de uma atualização de variável:

action Foo == all {
  val a = 1
  val b = 2
  variavel' = a + b,
  val c = 3
  outra' = c,
}

A divisão de escopo fica assim:

action Foo == all {
  // --- escopo 1 ----------
  val a = 1
  val b = 2
  variavel' = a + b,
  // --- fim escopo 1 ------
  // --- escopo 2 ----------
  val c = 3
  outra' = c,
  // --- fim escopo 2 ------
}

Se precisarmos de a, b e c pra ambas atualizações, basta usar um all dentro do escopo delas:

action Foo == {
  val a = 1
  val b = 2
  val c = 3
  all {
    variavel' = a + b + c,
    outra' = a * b * c,
  }
}

3.1 Erro ao remover o blind após o ataque (nesse semestre, se aplica ao ataque especial do necromante)

Lembre-se que não é possível atualizar a mesma variável mais de uma vez na mesma ação/transição. É necessário que as duas modificações (aplicação do dano de ataque e remoção do blind) sejam feitos na mesma atualização da variável de estado. É possível encadear os setBy (Quint) ou EXCEPT (TLA+) para isso:
Quint:

creatures.setBy(<dar dano no alvo>).setBy(<remover blind do atacante>)

TLA+:

[creatures EXCEPT ![alvo] = dano(@), ![atacante] = remocao(@)]

De forma mais geral, precisamos compor as duas atualizações, salvando o resultado da primeira em algum valor temporário e usando esse valor como base para computar o resultado da segunda, que então pode ser salvo na variável de estado (creatures, no exemplo acima).

3.2 Como fazer pra rodar um dado por criatura?

Não é possível, nesse caso, escrever algo do tipo "para cada criatura, rode um dado".

• O Apalache tem uma extensão para TLA+ que possibilitaria isso (Gen)
  • Não conheço nada semelhante no TLC.
    
  • Ainda não temos um equivalente no Quint, mas isso está em discussão e deve ser implementado logo.
    

Para o trabalho, podem fazer da forma repetitiva e declarar um valor para cada dado de cada criatura.