add example tests for damage

This commit is contained in:
Willem van den Ende 2026-06-14 20:52:31 +01:00
parent 1c9d4ad66b
commit 692bd7305b
14 changed files with 26269 additions and 4016 deletions

120
src/changing-level.allium Normal file
View File

@ -0,0 +1,120 @@
-- allium: 3
-- allium: changing-level
------------------------------------------------------------
-- Value Types
------------------------------------------------------------
value Faction {
name: String
}
value Health {
value: Integer
requires: value >= 0
}
value Level {
value: Integer
requires: value >= 1 and value <= 10
}
value Damage {
value: Integer
requires: value >= 0
}
------------------------------------------------------------
-- Enumerations
------------------------------------------------------------
enum Status {
alive | dead
}
------------------------------------------------------------
-- Entities
------------------------------------------------------------
entity Character {
name: String
health: Health
status: Status
level: Level
factions: Set<Faction>
totalDamageTaken: Damage
factionsJoined: Set<Faction>
}
------------------------------------------------------------
-- Rules
------------------------------------------------------------
rule DamageIsAccumulated {
when: Character.dealDamage(attacker, target, damage)
requires: target.status = alive
ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value) + damage.value
}
rule LevelUpFromDamage {
when: Character.dealDamage(attacker, target, damage)
requires: target.status = alive
requires: old(target.totalDamageTaken.value) + damage.value >= 1000 * (target.level.value + 1) * (target.level.value + 2) / 2
ensures: target.level.value = target.level.value + 1
ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value) + damage.value
}
rule LevelUpFromFaction {
when: Character.joinFaction(character, faction)
requires: character.status = alive
requires: old(character.factionsJoined.size) + 1 >= 3 * (character.level.value + 1)
ensures: character.level.value = character.level.value + 1
ensures: character.factionsJoined = old(character.factionsJoined) + {faction}
}
rule MaxLevelCappedOnDamage {
when: Character.dealDamage(attacker, target, damage)
requires: target.status = alive
requires: target.level.value = 10
ensures: target.level.value = 10
}
rule MaxLevelCappedOnFaction {
when: Character.joinFaction(character, faction)
requires: character.status = alive
requires: character.level.value = 10
ensures: character.level.value = 10
}
rule DeadCannotLevelUpFromDamage {
when: Character.dealDamage(attacker, target, damage)
requires: target.status = dead
ensures: target.level.value = old(target.level.value)
ensures: target.totalDamageTaken.value = old(target.totalDamageTaken.value)
}
rule DeadCannotLevelUpFromFaction {
when: Character.joinFaction(character, faction)
requires: character.status = dead
ensures: character.level.value = old(character.level.value)
}
------------------------------------------------------------
-- Invariants
------------------------------------------------------------
invariant LevelBounded {
for c in Characters:
c.level.value >= 1 and c.level.value <= 10
}
invariant DamageTotalNonNegative {
for c in Characters:
c.totalDamageTaken.value >= 0
}
invariant FactionsJoinedNonNegative {
for c in Characters:
c.factionsJoined.size >= 0
}

126
src/changing-level.spec.ts Normal file
View File

@ -0,0 +1,126 @@
import fc from 'fast-check';
import { describe, it, expect } from 'vitest';
import { Character } from './characters/Character.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
import { Faction } from './factions/Faction.ts';
describe('ChangingLevel', () => {
describe('MaxLevelCappedOnDamage (example)', () => {
it('L10 takes 99999 damage → stays L10', () => {
const attacker = Character.create({ name: 'dragons', level: Level.create(1) });
const target = Character.create({ name: 'hero', level: Level.create(10) });
const result = attacker.dealDamage(target, Damage.create(99999));
expect(result.level.value).toBe(10);
});
});
describe('MaxLevelCappedOnFaction (example)', () => {
it('L10 joins 100 factions → stays L10', () => {
const hero = Character.create({ name: 'hero', level: Level.create(10) });
let char = hero;
for (let i = 0; i < 100; i++) {
char = char.joinFaction(Faction.create(`faction-${i}`));
}
expect(char.level.value).toBe(10);
});
});
describe('DeadCannotLevelUpFromDamage (example)', () => {
it('dead char takes 1000 damage → stays same level', () => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const target = Character.create({ name: 'hero', level: Level.create(1) });
const dead = attacker.dealDamage(target, Damage.create(10000));
const result = attacker.dealDamage(dead, Damage.create(1000));
expect(result.level.value).toBe(1);
});
});
describe('DeadCannotLevelUpFromFaction (example)', () => {
it('dead char joins 5 factions → stays same level', () => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const target = Character.create({ name: 'hero', level: Level.create(1) });
const dead = attacker.dealDamage(target, Damage.create(10000));
let char = dead;
for (let i = 0; i < 5; i++) {
char = char.joinFaction(Faction.create(`faction-${i}`));
}
expect(char.level.value).toBe(1);
});
});
describe('LevelUpFromDamage (property)', () => {
it('property: cumulative damage triggers level-up at threshold', () => {
fc.assert(
fc.property(
fc.integer({ min: 1, max: 9 }),
fc.integer({ min: 1, max: 10000 }),
fc.integer({ min: 1, max: 10000 }),
(level, dmg1, dmg2) => {
const currentLevel = Level.create(level);
const targetLevel = Level.create(level + 1);
const threshold = 1000 * (level + 1) * (level + 2) / 2;
const total = dmg1 + dmg2;
// If total damage meets threshold, level should increase
if (total >= threshold) {
const attacker = Character.create({ name: 'a', level: Level.create(1) });
const target = Character.create({ name: 't', level: currentLevel });
const afterFirst = attacker.dealDamage(target, Damage.create(dmg1));
const afterSecond = attacker.dealDamage(afterFirst, Damage.create(dmg2));
return afterSecond.level.value === Math.min(10, level + 1);
}
return true; // skip non-applicable cases
},
),
);
});
});
describe('LevelUpFromFaction (property)', () => {
it('property: faction count triggers level-up at threshold', () => {
fc.assert(
fc.property(
fc.integer({ min: 1, max: 9 }),
fc.integer({ min: 1, max: 100 }),
fc.integer({ min: 1, max: 100 }),
(level, join1, join2) => {
const threshold = 3 * (level + 1);
const total = join1 + join2;
if (total >= threshold) {
const hero = Character.create({ name: 'hero', level: Level.create(level) });
let char = hero;
for (let i = 0; i < total; i++) {
char = char.joinFaction(Faction.create(`faction-${i}`));
}
return char.level.value === Math.min(10, level + 1);
}
return true; // skip non-applicable cases
},
),
);
});
});
describe('DamageAccumulation (property)', () => {
it('property: totalDamageTaken accumulates across multiple damage events', () => {
fc.assert(
fc.property(
fc.array(fc.integer({ min: 1, max: 5000 }), { minLength: 2, maxLength: 10 }),
(damageEvents) => {
const expectedTotal = damageEvents.reduce((sum, d) => sum + d, 0);
const attacker = Character.create({ name: 'a', level: Level.create(1) });
const target = Character.create({ name: 't', level: Level.create(1) });
let current = target;
for (const dmg of damageEvents) {
current = attacker.dealDamage(current, Damage.create(dmg));
}
return current.totalDamageTaken.value === expectedTotal;
},
),
);
});
});
});

View File

@ -6,6 +6,7 @@
*/
import { Health } from '../value-objects/Health.ts';
import { Level } from '../value-objects/Level.ts';
import type { Damage } from '../value-objects/Damage.ts';
import type { Status } from '../value-objects/Status.ts';
import { StatusAlive, StatusDead } from '../value-objects/Status.ts';
import type { CharacterState } from './CharacterState.ts';
@ -176,24 +177,22 @@ export class Character {
* Deal damage to another character. Returns a new Character with updated state.
* Does not mutate the attacker or the original target reference.
*/
dealDamage(target: Character, damage: number): Character {
dealDamage(target: Character, damage: Damage): Character {
// Self-damage is forbidden — use reference equality, not name
if (this === target) return target;
// Allies cannot deal damage to each other
if (this.isAllyOf(target)) return target;
// Dead characters cannot take damage
if (target.status.kind === 'dead') return target;
// Negative damage is invalid
if (damage < 0) throw new Error(`Damage must be non-negative, got ${damage}`);
// Level-based damage modifier
const levelDiff = this.level.diff(target.level); // = this.level - target.level
let actualDamage = damage;
let actualDamage = damage.value;
if (levelDiff <= -5) {
// Target is ≥5 levels above → damage reduced by 50%
actualDamage = Math.floor(damage * 0.5);
actualDamage = Math.floor(damage.value * 0.5);
} else if (levelDiff >= 5) {
// Target is ≥5 levels below → damage increased by 50%
actualDamage = Math.floor(damage * 1.5);
actualDamage = Math.floor(damage.value * 1.5);
}
// Reduce health by the (possibly modified) damage amount
const newHealth = target.health.sub(actualDamage);

View File

@ -8,6 +8,7 @@ import type { Health } from '../value-objects/Health.ts';
import type { Level } from '../value-objects/Level.ts';
import type { Status } from '../value-objects/Status.ts';
import type { Faction } from '../factions/Faction.ts';
import type { Damage } from '../value-objects/Damage.ts';
export type CharacterState = {
readonly name: string;
@ -15,4 +16,6 @@ export type CharacterState = {
readonly status: Status;
readonly level: Level;
readonly factions: ReadonlySet<Faction>;
readonly totalDamageTaken: Damage;
readonly factionsJoined: ReadonlySet<Faction>;
};

View File

@ -2,6 +2,7 @@ import fc from 'fast-check';
import { describe, it } from 'vitest';
import { Character } from './characters/Character.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
describe('DamageAndHealth', () => {
describe('DamageReducesHealth', () => {
@ -18,7 +19,7 @@ describe('DamageAndHealth', () => {
health,
});
const expected = Math.max(0, health - damage);
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value === expected;
},
),
@ -39,7 +40,7 @@ describe('DamageAndHealth', () => {
level: Level.create(1),
health,
});
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value >= 0;
},
),
@ -60,7 +61,7 @@ describe('DamageAndHealth', () => {
level: Level.create(1),
health,
});
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
const expected = Math.max(0, health - damage);
if (expected === 0) {
return result.status.kind === 'dead';
@ -82,7 +83,7 @@ describe('DamageAndHealth', () => {
const c = Character.createWithHealth({ name: 'hero', level: Level.create(1), health });
const healthBefore = c.health.value;
const statusBefore = c.status.kind;
const result = c.dealDamage(c, damage);
const result = c.dealDamage(c, Damage.create(damage));
// Should return the same reference
return (
result === c &&
@ -102,11 +103,11 @@ describe('DamageAndHealth', () => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const target = Character.create({ name: 'target', level: Level.create(1) });
// Kill the target first — capture the returned (dead) character
const deadTarget = attacker.dealDamage(target, 10000);
const deadTarget = attacker.dealDamage(target, Damage.create(10000));
const healthBefore = deadTarget.health.value;
const statusBefore = deadTarget.status.kind;
// Then try to deal more damage to the dead character
const result = attacker.dealDamage(deadTarget, damage);
const result = attacker.dealDamage(deadTarget, Damage.create(damage));
return (
result === deadTarget &&
result.health.value === healthBefore &&
@ -118,14 +119,12 @@ describe('DamageAndHealth', () => {
});
describe('NegativeDamageForbidden', () => {
it('property: negative damage throws an error', () => {
it('property: negative damage throws an error via Damage.create', () => {
fc.assert(
fc.property(fc.integer({ min: -10000, max: -1 }), (negativeDamage) => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const target = Character.create({ name: 'target', level: Level.create(1) });
let threw = false;
try {
attacker.dealDamage(target, negativeDamage);
Damage.create(negativeDamage);
} catch {
threw = true;
}

View File

@ -3,6 +3,7 @@ import { describe, it } from 'vitest';
import { Character } from './characters/Character.ts';
import { Faction } from './factions/Faction.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
describe('Factions', () => {
const hero = () => Character.create({ name: 'hero', level: Level.create(1) });
@ -189,7 +190,7 @@ describe('Factions', () => {
(factionName) => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const hero = Character.create({ name: 'hero', level: Level.create(1) });
const deadHero = attacker.dealDamage(hero, 10000);
const deadHero = attacker.dealDamage(hero, Damage.create(10000));
const f = Faction.create(factionName);
const result = deadHero.joinFaction(f);
return result === deadHero && result.factions.size === 0;
@ -209,7 +210,7 @@ describe('Factions', () => {
const hero = Character.create({ name: 'hero', level: Level.create(1) });
const f = Faction.create(factionName);
const withFaction = hero.joinFaction(f);
const deadHero = attacker.dealDamage(withFaction, 10000);
const deadHero = attacker.dealDamage(withFaction, Damage.create(10000));
const result = deadHero.leaveFaction(f);
return result === deadHero && result.factions.has(f);
},
@ -302,7 +303,7 @@ describe('Factions', () => {
const target = ally().joinFaction(faction);
const healthBefore = target.health.value;
const statusBefore = target.status.kind;
const result = attacker.dealDamage(target, 500);
const result = attacker.dealDamage(target, Damage.create(500));
return result.health.value === healthBefore && result.status.kind === statusBefore;
}),
);
@ -314,7 +315,7 @@ describe('Factions', () => {
const faction = Faction.create('guard');
const attacker = hero().joinFaction(faction);
const target = ally().joinFaction(faction);
const result = attacker.dealDamage(target, 500);
const result = attacker.dealDamage(target, Damage.create(500));
return result === target;
}),
);
@ -326,7 +327,7 @@ describe('Factions', () => {
const attacker = hero();
const target = enemy();
const healthBefore = target.health.value;
const result = attacker.dealDamage(target, 100);
const result = attacker.dealDamage(target, Damage.create(100));
return result.health.value === healthBefore - 100;
}),
);
@ -414,7 +415,7 @@ describe('Factions', () => {
const target = ally().joinFaction(faction);
// Kill the target with a non-ally attacker
const killer = enemy();
const deadTarget = killer.dealDamage(target, 10000);
const deadTarget = killer.dealDamage(target, Damage.create(10000));
const healthBefore = deadTarget.health.value;
const statusBefore = deadTarget.status.kind;
const result = healer.healAlly(deadTarget, 500);

View File

@ -2,6 +2,7 @@ import fc from 'fast-check';
import { describe, it } from 'vitest';
import { Character } from './characters/Character.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
describe('Healing', () => {
describe('SelfHealIncreasesHealth', () => {
@ -88,7 +89,7 @@ describe('Healing', () => {
const attacker = Character.create({ name: 'attacker', level: Level.create(1) });
const hero = Character.create({ name: 'hero', level: Level.create(1) });
// Kill the hero first using a different attacker
const deadHero = attacker.dealDamage(hero, 10000);
const deadHero = attacker.dealDamage(hero, Damage.create(10000));
const healthBefore = deadHero.health.value;
const statusBefore = deadHero.status.kind;
// Try to heal the dead character

View File

@ -2,6 +2,7 @@ import fc from 'fast-check';
import { describe, it } from 'vitest';
import { Character } from './characters/Character.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
describe('Levels', () => {
describe('CloseLevelNoModifier', () => {
@ -21,7 +22,7 @@ describe('Levels', () => {
level: Level.create(targetLevel),
health: 1000,
});
const result = attacker.dealDamage(target, baseDamage);
const result = attacker.dealDamage(target, Damage.create(baseDamage));
return result.health.value === Math.max(0, 1000 - baseDamage);
},
),
@ -47,7 +48,7 @@ describe('Levels', () => {
health: 1000,
});
const expectedDamage = Math.floor(baseDamage * 0.5);
const result = attacker.dealDamage(target, baseDamage);
const result = attacker.dealDamage(target, Damage.create(baseDamage));
return result.health.value === Math.max(0, 1000 - expectedDamage);
},
),
@ -66,7 +67,7 @@ describe('Levels', () => {
health: 1000,
});
const expectedDamage = Math.floor(oddDamage * 0.5);
const result = attacker.dealDamage(target, oddDamage);
const result = attacker.dealDamage(target, Damage.create(oddDamage));
return result.health.value === Math.max(0, 1000 - expectedDamage);
}),
);
@ -91,7 +92,7 @@ describe('Levels', () => {
health: 1000,
});
const expectedDamage = Math.floor(baseDamage * 1.5);
const result = attacker.dealDamage(target, baseDamage);
const result = attacker.dealDamage(target, Damage.create(baseDamage));
return result.health.value === Math.max(0, 1000 - expectedDamage);
},
),
@ -111,7 +112,7 @@ describe('Levels', () => {
health: 1000,
});
const expectedDamage = Math.floor(damage * 0.5);
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value === Math.max(0, 1000 - expectedDamage);
}),
);
@ -128,7 +129,7 @@ describe('Levels', () => {
health: 1000,
});
const expectedDamage = Math.floor(damage * 1.5);
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value === Math.max(0, 1000 - expectedDamage);
}),
);
@ -144,7 +145,7 @@ describe('Levels', () => {
level: Level.create(5),
health: 1000,
});
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value === Math.max(0, 1000 - damage);
}),
);
@ -160,7 +161,7 @@ describe('Levels', () => {
level: Level.create(1),
health: 1000,
});
const result = attacker.dealDamage(target, damage);
const result = attacker.dealDamage(target, Damage.create(damage));
return result.health.value === Math.max(0, 1000 - damage);
}),
);

View File

@ -2,6 +2,7 @@ import fc from 'fast-check';
import { describe, it } from 'vitest';
import { Character } from './characters/Character.ts';
import { Level } from './value-objects/Level.ts';
import { Damage } from './value-objects/Damage.ts';
import { MagicalWeapon } from './magical-objects/MagicalWeapon.ts';
import { HealingObject } from './magical-objects/HealingObject.ts';
@ -85,7 +86,7 @@ describe('Magical Objects', () => {
const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker });
// Kill the attacker using a separate killer
const killer = Character.create({ name: 'boss', level: Level.create(1) });
const deadAttacker = killer.dealDamage(attacker, 10000);
const deadAttacker = killer.dealDamage(attacker, Damage.create(10000));
const weaponHPBefore = weapon.health.value;
const targetHealthBefore = target.health.value;
const result = deadAttacker.useWeapon(weapon, target);
@ -256,7 +257,7 @@ describe('Magical Objects', () => {
const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP });
// Kill the character using a separate killer
const killer = Character.create({ name: 'boss', level: Level.create(1) });
const deadCharacter = killer.dealDamage(character, 10000);
const deadCharacter = killer.dealDamage(character, Damage.create(10000));
const objectHPBefore = object.health.value;
const characterHealthBefore = deadCharacter.health.value;
const result = deadCharacter.useHealingObject(object, 100);

View File

@ -7,18 +7,19 @@
*/
import { Character } from '../characters/Character.ts';
import { Health } from '../value-objects/Health.ts';
import { Damage } from '../value-objects/Damage.ts';
import { MagicalObject } from './MagicalObject.ts';
import type { DamageDealer } from './magical-object-types.ts';
export class MagicalWeapon extends MagicalObject implements DamageDealer {
readonly #damage: number;
readonly #damage: Damage;
readonly #owner: Character;
private constructor(
health: Health,
maxHealth: Health,
status: { readonly kind: 'alive' } | { readonly kind: 'destroyed' },
damage: number,
damage: Damage,
owner: Character,
) {
super(health, maxHealth, status);
@ -36,17 +37,16 @@ export class MagicalWeapon extends MagicalObject implements DamageDealer {
owner: Character;
}): MagicalWeapon {
if (maxHealth < 0) throw new Error('MaxHealth cannot be negative');
if (damage < 0) throw new Error('Damage cannot be negative');
return new MagicalWeapon(
Health.create(maxHealth),
Health.create(maxHealth),
{ kind: 'alive' },
damage,
Damage.create(damage),
owner,
);
}
get damage(): number {
get damage(): Damage {
return this.#damage;
}
@ -61,7 +61,7 @@ export class MagicalWeapon extends MagicalObject implements DamageDealer {
return { weapon: this, target };
}
// Deal fixed damage
const newTargetHealth = Math.max(0, target.health.value - this.#damage);
const newTargetHealth = Math.max(0, target.health.value - this.#damage.value);
const newTargetStatus = newTargetHealth === 0 ? { kind: 'dead' as const } : target.status;
const newTarget = Character.createWithHealthAndStatus({
name: target.name,

View File

@ -0,0 +1,26 @@
/**
* Damage value object non-negative, immutable.
*
* Invariant enforced at construction: n >= 0
*/
export class Damage {
readonly #value: number;
private constructor(n: number) {
this.#value = n;
}
static create(n: number): Damage {
if (n < 0) throw new Error(`Damage must be non-negative, got ${n}`);
return new Damage(n);
}
get value(): number {
return this.#value;
}
/** Add another damage amount — cumulative damage is still a Damage. */
add(other: Damage): Damage {
return Damage.create(this.#value + other.value);
}
}

View File

@ -31,4 +31,12 @@ export class Level {
diff(target: Level): number {
return this.value - target.value;
}
/** Damage threshold to reach the given level.
* Level 12: 1000, Level 23: 3000, Level 34: 6000, etc.
* Formula: 1000 * N * (N+1) / 2
*/
static damageThresholdForLevel(level: number): number {
return 1000 * level * (level + 1) / 2;
}
}

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long