From 31984bbd9d3b0b8616a3c740a0dd5b438626e9e9 Mon Sep 17 00:00:00 2001 From: Willem van den Ende Date: Mon, 15 Jun 2026 08:16:12 +0100 Subject: [PATCH] Consolidate all .allium specs into specs/ - Move .pi/specs/ files into specs/ (healing, factions, merged magical-objects) - Move src/*.allium files into specs/ (levels, changing-level) - Delete .pi/specs/ directory - Document specs/ convention in AGENTS.md --- .pi/specs/story-4-magical-objects.allium | 174 ------------------ AGENTS.md | 2 +- {src => specs}/changing-level.allium | 0 .../factions.allium | 0 .../healing.allium | 0 {src => specs}/levels.allium | 0 specs/magical-objects.allium | 6 + 7 files changed, 7 insertions(+), 175 deletions(-) delete mode 100644 .pi/specs/story-4-magical-objects.allium rename {src => specs}/changing-level.allium (100%) rename .pi/specs/story-3-factions.allium => specs/factions.allium (100%) rename .pi/specs/story-3-healing.allium => specs/healing.allium (100%) rename {src => specs}/levels.allium (100%) diff --git a/.pi/specs/story-4-magical-objects.allium b/.pi/specs/story-4-magical-objects.allium deleted file mode 100644 index ed2cfbd..0000000 --- a/.pi/specs/story-4-magical-objects.allium +++ /dev/null @@ -1,174 +0,0 @@ --- allium: 3 - --- allium: magical-objects - ------------------------------------------------------------- --- External Entities ------------------------------------------------------------- - -external entity Character { - name: String - health: Health - status: alive | dead - level: Level - factions: Set -} - -external entity Health { - value: Integer -} - -external entity Level { - value: Integer -} - -external entity Faction { - name: String -} - ------------------------------------------------------------- --- Entities and Variants ------------------------------------------------------------- - -entity MagicalWeapon { - health: Health - maxHealth: Integer - status: alive | destroyed - damage: Integer - owner: Character -} - -entity HealingObject { - health: Health - maxHealth: Integer - status: alive | destroyed -} - ------------------------------------------------------------- --- Rules ------------------------------------------------------------- - -rule WeaponDealsDamage { - when: MagicalWeapon.dealsDamage(weapon, target, attacker) - requires: weapon.status = alive - requires: attacker = weapon.owner - requires: attacker.status = alive - ensures: target.health.value = max(0, target.health.value - weapon.damage) - ensures: weapon.health.value = weapon.health.value - 1 - ensures: - if weapon.health.value - 1 = 0: - weapon.status = destroyed - else: - weapon.status = alive - ensures: - if max(0, target.health.value - weapon.damage) = 0: - target.status = dead - else: - target.status = alive -} - -rule DeadCannotUseWeapon { - when: MagicalWeapon.dealsDamage(weapon, target, attacker) - requires: attacker.status = dead - ensures: - target.health.value = target.health.value - weapon.health.value = weapon.health.value - weapon.status = weapon.status - target.status = target.status -} - -rule NonOwnerCannotUseWeapon { - when: MagicalWeapon.dealsDamage(weapon, target, attacker) - requires: attacker != weapon.owner - ensures: - target.health.value = target.health.value - weapon.health.value = weapon.health.value - weapon.status = weapon.status - target.status = target.status -} - -rule DestroyedWeaponCannotDealDamage { - when: MagicalWeapon.dealsDamage(weapon, target, attacker) - requires: weapon.status = destroyed - ensures: - target.health.value = target.health.value - weapon.health.value = weapon.health.value - weapon.status = weapon.status - target.status = target.status -} - -rule HealingObjectHealsCharacter { - when: HealingObject.healsCharacter(object, character, amount) - requires: object.status = alive - requires: character.status = alive - ensures: healAmount = min(amount, object.maxHealth - object.health.value) - ensures: character.health.value = character.health.value + healAmount - ensures: object.health.value = object.health.value - healAmount - ensures: - if object.health.value - healAmount = 0: - object.status = destroyed - else: - object.status = alive -} - -rule DeadCannotUseHealingObject { - when: HealingObject.healsCharacter(object, character, amount) - requires: character.status = dead - ensures: - character.health.value = character.health.value - object.health.value = object.health.value - object.status = object.status -} - -rule DestroyedHealingObjectCannotHeal { - when: HealingObject.healsCharacter(object, character, amount) - requires: object.status = destroyed - ensures: - character.health.value = character.health.value - object.health.value = object.health.value - object.status = object.status -} - ------------------------------------------------------------- --- Invariants ------------------------------------------------------------- - -invariant WeaponHealthNeverNegative { - for w in MagicalWeapons: - w.health.value >= 0 -} - -invariant WeaponDestroyedAtZeroHealth { - for w in MagicalWeapons: - w.health.value = 0 implies w.status = destroyed -} - -invariant WeaponMaxHealthNeverExceeded { - for w in MagicalWeapons: - w.health.value <= w.maxHealth -} - -invariant HealingObjectHealthNeverNegative { - for h in HealingObjects: - h.health.value >= 0 -} - -invariant HealingObjectDestroyedAtZeroHealth { - for h in HealingObjects: - h.health.value = 0 implies h.status = destroyed -} - -invariant HealingObjectMaxHealthNeverExceeded { - for h in HealingObjects: - h.health.value <= h.maxHealth -} - -invariant HealingObjectCannotDealDamage { - for h in HealingObjects: - not h.dealsDamage(_, _) -} - -invariant WeaponCannotHeal { - for w in MagicalWeapons: - not w.healsCharacter(_, _) -} diff --git a/AGENTS.md b/AGENTS.md index ffcda55..666709d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -16,7 +16,7 @@ An implementation of the RPG Combat rules engine. There are six user stories des This project combines three practices: -1. **Allium** (`.allium` specs) — formal behavioural specifications that capture _what_ the system does +1. **Allium** (`.allium` specs) — formal behavioural specifications that capture _what_ the system does. All specs live in [specs/](specs/) — one file per story/domain area. 2. **fast-check** — property-based testing that verifies those properties hold across thousands of random inputs 3. **"I can't believe it's not Haskell"** — TypeScript with ADTs, value objects, and immutability diff --git a/src/changing-level.allium b/specs/changing-level.allium similarity index 100% rename from src/changing-level.allium rename to specs/changing-level.allium diff --git a/.pi/specs/story-3-factions.allium b/specs/factions.allium similarity index 100% rename from .pi/specs/story-3-factions.allium rename to specs/factions.allium diff --git a/.pi/specs/story-3-healing.allium b/specs/healing.allium similarity index 100% rename from .pi/specs/story-3-healing.allium rename to specs/healing.allium diff --git a/src/levels.allium b/specs/levels.allium similarity index 100% rename from src/levels.allium rename to specs/levels.allium diff --git a/specs/magical-objects.allium b/specs/magical-objects.allium index f756db3..f0227a9 100644 --- a/specs/magical-objects.allium +++ b/specs/magical-objects.allium @@ -136,6 +136,8 @@ rule DeadCannotUseWeapon { ensures: target.health.value = target.health.value weapon.health.value = weapon.health.value + weapon.status = weapon.status + target.status = target.status } rule NonOwnerCannotUseWeapon { @@ -146,6 +148,8 @@ rule NonOwnerCannotUseWeapon { ensures: target.health.value = target.health.value weapon.health.value = weapon.health.value + weapon.status = weapon.status + target.status = target.status } rule WeaponDestroyedCannotDealDamage { @@ -156,6 +160,8 @@ rule WeaponDestroyedCannotDealDamage { ensures: target.health.value = target.health.value weapon.health.value = weapon.health.value + weapon.status = weapon.status + target.status = target.status } ------------------------------------------------------------