De forma semelhante aos exemplos de jogo da velha e pokemons, você deve especificar um jogo onde as partes fazem jogadas aleatórias, mostrando que assim ambas as partes podem vencer; e então especificar uma versão desse jogo onde os personagens usam uma estratégia que garante que eles não percam.
As regras dessa batalha são inspiradas em jogo de RPG, porém um tanto exageradas para que possamos explorar algumas correspondências interessantes com problemas e soluções reais.
Ataques são a forma de dar dano em criaturas. O dano é determinado por um inteiro, e ao receber um ataque, uma criatura perde uma quantidade de pontos de vida (HP - Health Points) igual ao dano do ataque. Uma criatura morre quando seus pontos de vida chegam a zero.
Criaturas podem ser paralisadas. Criaturas paralisadas não podem fazer nada em seu turno.
Personagens da classe sacerdote tem habilidade de curar seus aliados, restaurando 10 pontos de vida de todos os aliados, incluindo ele mesmo. A cura não pode fazer com que a criatura fique com mais vida do que sua vida inicial. Considerando que os personagens começam com 20 pontos de vida, um personagem com 15 pontos de vida que recebe cura ficará com 20 pontos de vida.
Personagens da classe bardo tem habilidade de cantar para inspirar outras criaturas. O primeiro ataque feito após o bardo começar a cantar dá o triplo de dano, e o bardo imediatamente para de cantar. Até mesmo inimigos podem se inspirar no canto do bardo.
Personagens da classe necromante tem um ataque especial. Eles podem usar o próprio sangue para causar dano extra num inimigo, recebendo 10 de dano e causando 20 de dano em seu alvo. O dano causado no alvo pode ser afetado pelo canto do bardo.
Essa batalha tem várias criaturas lutando entre si, entre elas inimigos e personagens
Todos os inimigos são iguais. Inimigos tem 90 pontos de vida iniciais.
No primeiro turno, um inimigo inicia um ritual (somente um deles, se tiverem múltiplos inimigos). No terceiro turno desse inimigo após o ínicio do ritual (sem contar o turno de início do ritual), o inimigo finaliza o ritual e todos os personagens morrem. Evidentemente, o ritual não pode ser finalizado se o inimigo estiver morto.
Nos demais turnos, podem fazer as seguintes ações (uma ação por turno):
Os ataques de personagem causam 10 de dano e tem 20 pontos de vida iniciais, independente da classe. Eles podem executar uma das seguintes ações em seu turno:
No início da batalha, cada criatura roda um d20 (dado com 20 faces, de 1 até 20) para determinar sua iniciativa. Aqueles com maior iniciativa jogam primeiro, e os com menor iniciativa jogam por último. Se duas ou mais criaturas tiverem a mesma iniciativa, a ordem que elas jogam entre si não importa. Nesse caso, fica a critério de vocês qual o comportamento exato. Se uma criatura A tem iniciativa maior que a criatura B, A deve jogar antes de B. Após todas as criaturas jogarem uma vez, o ciclo reinicia seguindo as mesmas regras e a mesma iniciativa.
Primeiramente, escreva uma especificação descrevendo o que pode acontecer nesse jogo. Considere que exista um único inimigo, e um personagem de cada classe. Nessa versão, deve ser possível tanto que o inimigo quanto que algum dos jogadores morra.
Escreva duas invariantes:
Nenhuma delas deve ser verdadeira nessa versão.
Adicionalmente, se quiser conferir que seu ritual está funcionando como deveria, escreva uma invariante para “algum personagem sobrevive” (ou a equivalente “não é verdade que todos os personagens morrem”). Ela não deve ser verdadeira nessa versão.
Você pode usar simuladores ao invés de model checkers para testar as invariantes em todas as etapas deste trabalho. Idealmente, devíamos usar model checkers, mas o modelo deste trabalho tem estados demais e execuções muito longas para uso de model checkers. Usaremos model checkers nos exemplos reais de sistemas distribuídos que veremos na disciplina.
Agora, modifique a especificação (mas salve o arquivo! Você precisa entregar as duas) para que os personagens utilizem uma estratégia, ao escolher suas ações, de forma que a invariante “nenhum personagem morre” seja verdadeira.
Por último, modifique a especificação anterior (com estratégia) para que a batalha seja contra dois inimigos. Você pode escolher entregar um arquivo a mais com essa versão, ou simplesmente entregar com essa parte comentada, já que pode ser uma modificação de apenas uma linha.
Essa batalha é impossível, mesmo com as estratégias empregadas. Assim, a invariante “nenhum personagem morre” deve ser violada. Se os personagens estiverem sobrevivendo na sua versão, pode ser que alguma regra não esteja definida corretamente.