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 caçador tem habilidade de cegar um monstro. Ataques de um monstro cego causam 0 de dano. A cegueira dura um turno, de forma que o monstro deixa de estar cego ao terminar seu turno.
Personagens da classe druida tem habilidade de se transformar em urso. Ao se transformar em urso, o druida passa a, temporariamente, ter 60 pontos de vida. Se o urso morrer, o druida volta a ter a quantidade de pontos de vida que tinha antes de se transformar. A transformação selvagem dura até o início do próximo turno do druida, onde ele pode escolher se transformar novamente ou fazer outra ação.
Monstros tem medo de animais: A ameaça (threat) que um urso causa nos monstros é maior, de forma que monstros sempre atacam o urso se ele estiver presente.
Personagens da classe mago tem habilidade de criar uma ilusão de uma ovelha com 1 ponto de vida. A ilusão não pode atacar, mas pode ser atacada. A ilusão dura até o início do próximo turno do mago, onde ele pode escolher recriar a ilusão ou fazer outra ação.
Monstros tem medo de animais: A ameaça (threat) que uma ilusão causa nos monstros é a mesma do urso, de forma que os montros vão sempre preferir atacar ovelhas e ursos se esses estiverem presentes.
Essa batalha tem várias criaturas lutando entre si, entre elas monstros e personagens
Todos os monstros são iguais. Monstros tem 100 pontos de vida iniciais, e podem fazer as seguintes ações em seus turnos (uma ação por turno)
Os ataques de monstro sempre dão 20 de dano, exceto se esse for o primeiro turno de toda a batalha (ninguém jogou ainda), onde o ataque é mais fraco (ele ainda está carregando todo o seu poder). No primeiro turno, um monstro dá apenas 10 de dano.
Um monstro pode paralizar um personagem. Essa paralisia é permanente, e só é removida quando outro personagem usa sua ação para remover a paralisia de um jogador específico.
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 monstro, e um personagem de cada classe. Nessa versão, deve ser possível tanto que o monstro quanto que algum dos jogadores morra.
Escreva duas invariantes:
Nenhuma delas 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 monstros. 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.