-- allium: 3

-- allium: magical-objects

------------------------------------------------------------
-- External Entities
------------------------------------------------------------

external entity Character {
    name: String
    health: Health
    status: alive | dead
    level: Level
    factions: Set<Faction>
}

external entity Health {
    value: Integer
}

external entity Level {
    value: Integer
}

external entity Faction {
    name: String
}

------------------------------------------------------------
-- Entities and Variants
------------------------------------------------------------

entity MagicalWeapon {
    health: Health
    maxHealth: Integer
    status: alive | destroyed
    damage: Integer
    owner: Character
}

entity HealingObject {
    health: Health
    maxHealth: Integer
    status: alive | destroyed
}

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

rule WeaponDealsDamage {
    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
    requires: weapon.status = alive
    requires: attacker = weapon.owner
    requires: attacker.status = alive
    ensures: target.health.value = max(0, target.health.value - weapon.damage)
    ensures: weapon.health.value = weapon.health.value - 1
    ensures:
        if weapon.health.value - 1 = 0:
            weapon.status = destroyed
        else:
            weapon.status = alive
    ensures:
        if max(0, target.health.value - weapon.damage) = 0:
            target.status = dead
        else:
            target.status = alive
}

rule DeadCannotUseWeapon {
    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
    requires: attacker.status = dead
    ensures:
        target.health.value = target.health.value
        weapon.health.value = weapon.health.value
        weapon.status = weapon.status
        target.status = target.status
}

rule NonOwnerCannotUseWeapon {
    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
    requires: attacker != weapon.owner
    ensures:
        target.health.value = target.health.value
        weapon.health.value = weapon.health.value
        weapon.status = weapon.status
        target.status = target.status
}

rule DestroyedWeaponCannotDealDamage {
    when: MagicalWeapon.dealsDamage(weapon, target, attacker)
    requires: weapon.status = destroyed
    ensures:
        target.health.value = target.health.value
        weapon.health.value = weapon.health.value
        weapon.status = weapon.status
        target.status = target.status
}

rule HealingObjectHealsCharacter {
    when: HealingObject.healsCharacter(object, character, amount)
    requires: object.status = alive
    requires: character.status = alive
    ensures: healAmount = min(amount, object.maxHealth - object.health.value)
    ensures: character.health.value = character.health.value + healAmount
    ensures: object.health.value = object.health.value - healAmount
    ensures:
        if object.health.value - healAmount = 0:
            object.status = destroyed
        else:
            object.status = alive
}

rule DeadCannotUseHealingObject {
    when: HealingObject.healsCharacter(object, character, amount)
    requires: character.status = dead
    ensures:
        character.health.value = character.health.value
        object.health.value = object.health.value
        object.status = object.status
}

rule DestroyedHealingObjectCannotHeal {
    when: HealingObject.healsCharacter(object, character, amount)
    requires: object.status = destroyed
    ensures:
        character.health.value = character.health.value
        object.health.value = object.health.value
        object.status = object.status
}

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

invariant WeaponHealthNeverNegative {
    for w in MagicalWeapons:
        w.health.value >= 0
}

invariant WeaponDestroyedAtZeroHealth {
    for w in MagicalWeapons:
        w.health.value = 0 implies w.status = destroyed
}

invariant WeaponMaxHealthNeverExceeded {
    for w in MagicalWeapons:
        w.health.value <= w.maxHealth
}

invariant HealingObjectHealthNeverNegative {
    for h in HealingObjects:
        h.health.value >= 0
}

invariant HealingObjectDestroyedAtZeroHealth {
    for h in HealingObjects:
        h.health.value = 0 implies h.status = destroyed
}

invariant HealingObjectMaxHealthNeverExceeded {
    for h in HealingObjects:
        h.health.value <= h.maxHealth
}

invariant HealingObjectCannotDealDamage {
    for h in HealingObjects:
        not h.dealsDamage(_, _)
}

invariant WeaponCannotHeal {
    for w in MagicalWeapons:
        not w.healsCharacter(_, _)
}