45 lines
1.1 KiB
Plaintext
45 lines
1.1 KiB
Plaintext
-- 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, _)
|
|
}
|