-- allium: 3

-- allium: damage-and-health

------------------------------------------------------------
-- Rules
------------------------------------------------------------

rule DamageReducesHealth {
    when: Character.dealDamage(attacker, target, damage)
    requires: attacker.name != target.name
    requires: target.status = alive
    ensures: target.health.value = max(0, target.health.value - damage)
    ensures:
        if max(0, target.health.value - damage) = 0:
            target.status = dead
        else:
            target.status = alive
}

rule SelfDamageForbidden {
    when: Character.dealDamage(attacker, target, damage)
    requires: attacker.name = target.name
    ensures:
        target.health.value = target.health.value
        target.status = target.status
}

rule DeadCannotTakeDamage {
    when: Character.dealDamage(attacker, target, damage)
    requires: target.status = dead
    ensures:
        target.health.value = target.health.value
        target.status = dead
}

------------------------------------------------------------
-- Invariants
------------------------------------------------------------

invariant HealthNonNegative {
    for c in Characters:
        c.health.value >= 0
}

invariant DeathAtZeroHealth {
    for c in Characters:
        c.health.value = 0 implies c.status = dead
}