-- allium: 3
-- allium: magical-objects

-- Scope: Magical Objects (Healing Objects and Weapons)
-- Includes: MagicalObject base, HealingObject, MagicalWeapon, Character interactions
-- Excludes:
--   - Magical Object to Magical Object interactions (not in story)
--   - Magical Object factions (they are neutral)
--   - Characters healing Magical Objects (forbidden by story)

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

entity MagicalObject {
    health: Health
    maxHealth: Health
    status: alive | destroyed

    is_alive: status = alive
    is_destroyed: status = destroyed

    transitions status {
        alive -> destroyed
        terminal: destroyed
    }
}

entity HealingObject : MagicalObject {
    -- Healing objects transfer health to characters
    -- They cannot deal damage
}

entity MagicalWeapon : MagicalObject {
    damage: Integer  -- fixed damage amount
    owner: Character  -- only the owner can use this weapon
    -- Weapons cannot give health to characters
}

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

rule HealingObjectHealsCharacter {
    when: CharacterUsesHealingObject(character, object, amount)

    requires: object.status = alive
    requires: character.status = alive
    requires: amount >= 0

    let objectRemaining = object.health
    let characterMax = Level.maxHealthForLevel(character.level)
    let characterHeadroom = characterMax - character.health
    let actualHeal = min(amount, objectRemaining, characterHeadroom)

    ensures:
        if actualHeal > 0:
            character.health = character.health + actualHeal
            object.health = object.health - actualHeal
            if object.health = 0:
                object.status = destroyed
            else:
                object.status = alive
        else:
            character.health = character.health
            object.health = object.health
}

rule HealingObjectDestroyedCannotHeal {
    when: CharacterUsesHealingObject(character, object, amount)

    requires: object.status = destroyed

    ensures:
        character.health = character.health
        object.health = object.health
}

rule DeadCannotUseHealingObject {
    when: CharacterUsesHealingObject(character, object, amount)

    requires: character.status = dead

    ensures:
        character.health = character.health
        object.health = object.health
}

rule HealingObjectZeroHealIsNoOp {
    when: CharacterUsesHealingObject(character, object, amount)

    requires: object.status = alive
    requires: character.status = alive
    requires: amount >= 0
    requires: min(amount, object.health, Level.maxHealthForLevel(character.level) - character.health) = 0

    ensures:
        character.health = character.health
        object.health = object.health
}

rule MagicalWeaponDealsDamage {
    when: CharacterUsesWeapon(owner, weapon, target)

    requires: weapon.status = alive
    requires: owner.status = alive
    requires: owner = weapon.owner

    ensures:
        target.health = max(0, target.health - weapon.damage)
        if target.health = 0:
            target.status = dead
        weapon.health = weapon.health - 1
        if weapon.health = 0:
            weapon.status = destroyed
        else:
            weapon.status = alive
}

rule DeadCannotUseWeapon {
    when: CharacterUsesWeapon(owner, weapon, target)

    requires: owner.status = dead

    ensures:
        target.health = target.health
        weapon.health = weapon.health
}

rule NonOwnerCannotUseWeapon {
    when: CharacterUsesWeapon(thief, weapon, target)

    requires: thief != weapon.owner

    ensures:
        target.health = target.health
        weapon.health = weapon.health
}

rule WeaponDestroyedCannotDealDamage {
    when: CharacterUsesWeapon(owner, weapon, target)

    requires: weapon.status = destroyed

    ensures:
        target.health = target.health
        weapon.health = weapon.health
}

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

invariant MagicalObjectHealthNonNegative {
    for m in MagicalObjects:
        m.health >= 0
}

invariant MagicalObjectHealthNeverExceedsMax {
    for m in MagicalObjects:
        m.health <= m.maxHealth
}

invariant MagicalObjectDestroyedAtZeroHealth {
    for m in MagicalObjects:
        m.health = 0 implies m.status = destroyed
}

invariant MagicalObjectAliveAtPositiveHealth {
    for m in MagicalObjects:
        m.health > 0 implies m.status = alive
}

invariant HealingObjectDoesNotDealDamage {
    for h in HealingObjects, t in Characters:
        not exists amount: CharacterUsesHealingObject(t, h, amount) implies t.health >= t.health
}

invariant MagicalWeaponCannotGiveHealth {
    for w in MagicalWeapons, c in Characters:
        not exists target: CharacterUsesWeapon(c, w, target) implies target.health <= target.health
}