-- allium: 3

-- allium: healing

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

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

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

rule SelfHealIncreasesHealth {
    when: CharacterHealsSelf(character, amount)
    requires: character.status = alive
    ensures: character.health = min(character.health + amount, maxHealthForLevel(character.level))
}

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

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

invariant HealthNeverExceedsLevelCap {
    for c in Characters:
        c.health <= maxHealthForLevel(c.level)
}

invariant DeadCannotHeal {
    for c in Characters:
        c.status = dead implies not CharacterHealsSelf(c, _)
}