battle_simulator.pcsp

#define active 1; //trainer active
#define inactive 0; //trainer inactive
#define win 2; // trainer wins
#define lose -1; //trainer loses

var trainer[2] = [active, inactive]; //initial trainer states
var health[2] = [80, 79]; // pokemon's HP [Blastoise, Venusaur]
var attackStat[2] = [83, 82]; // pokemon's attack [Blastoise, Venusaur]
var defenceStat[2] = [100, 83]; // pokemon's defence [Blastoise, Venusaur]
var level[2] = [50, 50]; // pokemon's level [Blastoise, Venusaur]
var pokemon0Moves = [90, 90, 100, 80]; // Blastoise: Surf, Ice Beam, Earthquake, Gyro Ball
var pokemon1Moves = [60, 90, 85, 70]; // Venusaur: Magical Leaf, Sludge Bomb, Body Slam, Secret Power

rotate() = 
        [trainer[0] == active && trainer[1] == inactive]switch{trainer[0] = inactive; trainer[1] = active} -> move(1)
        []
        [trainer[1] == active && trainer[0] == inactive]switch{trainer[1] = inactive; trainer[0] = active} -> move(0);   

move(i) = 
        [i == 0]attackFoe.i -> attack(0)
        []
        [i == 1]attackFoe.i -> attack(1);

attack(i) = [i == 0]pokemon0attack -> pcase {
        [0.25]: damage(0, pokemon0Moves[0])
        [0.25]: damage(0, pokemon0Moves[1])
        [0.25]: damage(0, pokemon0Moves[2])
        [0.25]: damage(0, pokemon0Moves[3])
} [] [i == 1]pokemon1attack -> pcase {
        [0.25]: damage(1, pokemon1Moves[0])
        [0.25]: damage(1, pokemon1Moves[1])
        [0.25]: damage(1, pokemon1Moves[2])
        [0.25]: damage(1, pokemon1Moves[3])
};

damage(i, p) = [i == 0]damageFoe.i{health[1] = health[1] - (((((2*level[0])/5) + 2)*p*(attackStat[0]/defenceStat[1])/50) + 2)} -> end()
                []
                [i == 1]damageFoe.i{health[0] = health[0] - (((((2*level[1])/5) + 2)*p*(attackStat[1]/defenceStat[0])/50) + 2)} -> end();  

end() = [health[0] <= 0]trainer0win{trainer[1] = win; trainer[0] = lose} -> Stop
        []
        [health[1] <= 0]trainer1win{trainer[0] = win; trainer[1] = lose} -> Stop
        []
        [health[1] > 0 && health[0] > 0] rotate();

start() = 
	trainer0start{trainer[0] = active; trainer[1] = inactive} -> rotate()
	[]
	trainer1start{trainer[1] = active; trainer[0] = inactive} -> rotate();

simulate = start();

#define trainer0wins (trainer[0] == win && trainer[1] == lose);
#define trainer1wins (trainer[1] == win && trainer[0] == lose);
#define bothtrainerswin (trainer[0] == win && trainer[1] == win);
#define bothtrainerslose (trainer[0] == lose && trainer[1] == lose);

#assert simulate reaches trainer0wins;
#assert simulate reaches trainer1wins;
#assert simulate reaches bothtrainerswin;
#assert simulate reaches bothtrainerslose;