-- allium: 3

-- allium: changing-level

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

value Faction {
    name: String
}

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

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

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

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

enum Status {
    alive | dead
}

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

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

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

rule DamageIsAccumulated {
    when: Character.dealDamage(attacker, target, damage)
    requires: target.status = alive
    ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value) + damage.value
}

rule LevelUpFromDamage {
    when: Character.dealDamage(attacker, target, damage)
    requires: target.status = alive
    requires: old(target.totalDamageTaken.value) + damage.value >= 1000 * (target.level.value + 1) * (target.level.value + 2) / 2
    ensures: target.level.value = target.level.value + 1
    ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value) + damage.value
}

rule LevelUpFromFaction {
    when: Character.joinFaction(character, faction)
    requires: character.status = alive
    requires: old(character.factionsJoined.size) + 1 >= 3 * (character.level.value + 1)
    ensures: character.level.value = character.level.value + 1
    ensures: character.factionsJoined = old(character.factionsJoined) + {faction}
}

rule MaxLevelCappedOnDamage {
    when: Character.dealDamage(attacker, target, damage)
    requires: target.status = alive
    requires: target.level.value = 10
    ensures: target.level.value = 10
}

rule MaxLevelCappedOnFaction {
    when: Character.joinFaction(character, faction)
    requires: character.status = alive
    requires: character.level.value = 10
    ensures: character.level.value = 10
}

rule DeadCannotLevelUpFromDamage {
    when: Character.dealDamage(attacker, target, damage)
    requires: target.status = dead
    ensures: target.level.value = old(target.level.value)
    ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value)
}

rule DeadCannotLevelUpFromFaction {
    when: Character.joinFaction(character, faction)
    requires: character.status = dead
    ensures: character.level.value = old(character.level.value)
}

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

invariant LevelBounded {
    for c in Characters:
        c.level.value >= 1 and c.level.value <= 10
}

invariant DamageTotalNonNegative {
    for c in Characters:
        c.totalDamageTaken.value >= 0
}

invariant FactionsJoinedNonNegative {
    for c in Characters:
        c.factionsJoined.size >= 0
}