-- allium: 3

-- allium: character-creation

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

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

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

type Status {
    alive | dead
}

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

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

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

rule CharacterCreation {
    when: Character.create(name, level)
    ensures: character.health.value = 1000
    ensures: character.status = alive
    ensures: character.level = level
    ensures: character.factions = empty
}

rule MaxLevel {
    for c in Characters:
        c.level.value <= 10
}

rule MinLevel {
    for c in Characters:
        c.level.value >= 1
}