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

------------------------------------------------------------
-- Value Types
------------------------------------------------------------

value Health {
    value: Integer
    requires: value >= 0
}

value Faction {
    name: String
}

value Level {
    value: Integer
    requires: value >= 1 and value <= 10
}

------------------------------------------------------------
-- Enumerations
------------------------------------------------------------

enum Status {
    alive | destroyed
}

------------------------------------------------------------
-- Entities
------------------------------------------------------------

entity Character {
    name: String
    health: Health
    status: Status
    level: Level
    factions: Set<Faction>
}

entity MagicalObject {
    health: Health
    maxHealth: Integer
    status: Status
}

entity HealingObject {
    health: Health
    maxHealth: Integer
    status: Status
}

entity MagicalWeapon {
    health: Health
    maxHealth: Integer
    status: Status
    damage: Integer
    owner: Character
}

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

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

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

    ensures:
        character.health.value = character.health.value + min(amount, object.health.value, Level.maxHealthForLevel(character.level) - character.health.value)
        object.health.value = object.health.value - min(amount, object.health.value, Level.maxHealthForLevel(character.level) - character.health.value)
        if object.health.value = 0:
            object.status = destroyed
        else:
            object.status = alive
}

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

    requires: object.status = destroyed

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

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

    requires: character.status = dead

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

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

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

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

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

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

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

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

    requires: owner.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: CharacterUsesWeapon(thief, weapon, target)

    requires: thief != weapon.owner

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

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

    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
}

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

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

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

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

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