-- allium: 3

-- allium: factions

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

value Faction {
    name: String
}

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

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

enum Status {
    alive | dead
}

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

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

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

rule JoinFaction {
    when: Character.joinFaction(character, faction)
    requires: character.status = alive
    ensures: character.factions = old(character.factions) + {faction}
}

rule LeaveFaction {
    when: Character.leaveFaction(character, faction)
    requires: character.status = alive
    requires: faction in character.factions
    ensures: character.factions = old(character.factions) - {faction}
}

rule AllyDamageForbidden {
    when: Character.dealDamage(attacker, target, damage)
    requires: attacker.isAllyOf(target)
    ensures:
        target.health.value = old(target.health.value)
        target.status = old(target.status)
}

rule AllyHealAllowed {
    when: Character.healAlly(healer, ally, amount)
    requires: healer.status = alive
    requires: ally.status = alive
    requires: healer.isAllyOf(ally)
    ensures: ally.health.value = min(ally.health.value + amount, maxHealthForLevel(ally.level))
}

rule NonAllyHealForbidden {
    when: Character.healAlly(healer, ally, amount)
    requires: not healer.isAllyOf(ally)
    ensures:
        ally.health.value = old(ally.health.value)
        ally.status = old(ally.status)
}

rule DeadCannotJoinFaction {
    when: Character.joinFaction(character, faction)
    requires: character.status = dead
    ensures: character.factions = old(character.factions)
}

rule DeadCannotLeaveFaction {
    when: Character.leaveFaction(character, faction)
    requires: character.status = dead
    ensures: character.factions = old(character.factions)
}

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

invariant FactionsAlwaysValid {
    for c in Characters:
        for f in c.factions:
            f.name.length > 0
}

invariant SelfNotAlly {
    for c in Characters:
        not c.isAllyOf(c)
}