Willem van den Ende
f6605bbbfd
- Add .pi/specs/story-3-factions.allium with formal spec for faction rules - Add src/factions.spec.ts with 26 fast-check properties covering: - joinFaction / leaveFaction (add, remove, idempotent, dead no-op) - isAllyOf (shared factions, symmetry, self-not-ally) - dealDamage blocks ally damage - healAlly (allies only, capped, dead no-op) - Implement Character methods: joinFaction, leaveFaction, isAllyOf, healAlly - Modify dealDamage to check ally status before applying damage
98 lines
2.6 KiB
Plaintext
98 lines
2.6 KiB
Plaintext
-- allium: 3
|
|
|
|
-- allium: factions
|
|
|
|
------------------------------------------------------------
|
|
-- Value Types
|
|
------------------------------------------------------------
|
|
|
|
type Faction {
|
|
name: String
|
|
requires: trimmed(name).length > 0
|
|
}
|
|
|
|
------------------------------------------------------------
|
|
-- Entities
|
|
------------------------------------------------------------
|
|
|
|
entity Character {
|
|
name: String
|
|
health: Health
|
|
status: alive | dead
|
|
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.trim().length > 0
|
|
}
|
|
|
|
invariant AllyRelationIsSymmetric {
|
|
for a in Characters, b in Characters:
|
|
a.isAllyOf(b) implies b.isAllyOf(a)
|
|
}
|
|
|
|
invariant SelfNotAlly {
|
|
for c in Characters:
|
|
not c.isAllyOf(c)
|
|
}
|