-- allium: 3

-- allium: levels

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

rule LevelDiff {
    for attacker in Characters, target in Characters:
        diff = target.level - attacker.level
}

rule HighLevelTargetModifier {
    when: CharacterDealsDamage(attacker, target, baseDamage)
    requires: target.level - attacker.level >= 5
    ensures: actualDamage = floor(baseDamage * 0.5)
}

rule LowLevelTargetModifier {
    when: CharacterDealsDamage(attacker, target, baseDamage)
    requires: attacker.level - target.level >= 5
    ensures: actualDamage = floor(baseDamage * 1.5)
}

rule CloseLevelNoModifier {
    when: CharacterDealsDamage(attacker, target, baseDamage)
    requires: abs(target.level - attacker.level) < 5
    ensures: actualDamage = baseDamage
}

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

invariant DamageModifierComputationComplete {
    for a in Characters, t in Characters, d in NonNegativeIntegers:
        let diff = t.level - a.level
        let actualDamage =
            if diff >= 5 then floor(d * 0.5)
            else if diff <= -5 then floor(d * 1.5)
            else d
        a.dealDamage(t, d) implies t.health = old(t.health) - actualDamage
}