diff --git a/.pi/specs/story-4-magical-objects.allium b/.pi/specs/story-4-magical-objects.allium new file mode 100644 index 0000000..ed2cfbd --- /dev/null +++ b/.pi/specs/story-4-magical-objects.allium @@ -0,0 +1,174 @@ +-- 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/src/Character.ts b/src/Character.ts index c3b2a8c..812923c 100644 --- a/src/Character.ts +++ b/src/Character.ts @@ -10,6 +10,8 @@ import type { Status } from './Status.ts'; import { StatusAlive, StatusDead } from './Status.ts'; import { CharacterState } from './CharacterState.ts'; import type { Faction } from './Faction.ts'; +import type { MagicalWeapon } from './MagicalWeapon.ts'; +import type { HealingObject } from './HealingObject.ts'; export interface CharacterCtor { name: string; @@ -22,6 +24,13 @@ export interface CharacterCtorWithHealth { health: number; } +export interface CharacterCtorWithHealthAndStatus { + name: string; + level: Level; + health: number; + status: Status; +} + export class Character { #state: CharacterState; readonly #name: string; @@ -43,6 +52,17 @@ export class Character { return new Character(state); } + /** Create a character with specific health and status (for use by MagicalWeapon). */ + static createWithHealthAndStatus({ + name, + level, + health, + status, + }: CharacterCtorWithHealthAndStatus): Character { + const state = new CharacterState(name, Health.create(health), status, level, new Set()); + return new Character(state); + } + get name(): string { return this.#name; } @@ -108,4 +128,34 @@ export class Character { new CharacterState(this.name, newHealth, this.status, this.level, this.factions), ); } + + /** + * Use a Magical Weapon to deal damage to a target. + * Dead characters cannot use weapons. Only the owner can use a weapon. + * Returns updated weapon and target. + */ + useWeapon( + weapon: MagicalWeapon, + target: Character, + ): { weapon: MagicalWeapon; target: Character } { + // Dead characters cannot use weapons + if (this.status.kind === 'dead') return { weapon, target }; + // Only the owner can use the weapon + if (weapon.owner !== this) return { weapon, target }; + return weapon.use(target); + } + + /** + * Use a Healing Object to gain health. + * Dead characters cannot use healing objects. + * Returns updated object and character. + */ + useHealingObject( + object: HealingObject, + amount: number, + ): { object: HealingObject; character: Character } { + // Dead characters cannot use healing objects + if (this.status.kind === 'dead') return { object, character: this }; + return object.heal(this, amount); + } } diff --git a/src/HealingObject.ts b/src/HealingObject.ts new file mode 100644 index 0000000..66463d6 --- /dev/null +++ b/src/HealingObject.ts @@ -0,0 +1,84 @@ +/** + * Healing Object — a Magical Object that gives health to Characters. + * + * Invariants enforced at construction: + * - Health is non-negative + * - Health never exceeds maxHealth + */ + +import { Character } from './Character.ts'; + +export type ObjectStatus = { kind: 'alive' } | { kind: 'destroyed' }; + +export class HealingObject { + readonly #health: number; + readonly #maxHealth: number; + readonly #status: ObjectStatus; + + private constructor(health: number, maxHealth: number, status: ObjectStatus) { + this.#health = health; + this.#maxHealth = maxHealth; + this.#status = status; + } + + static create({ + maxHealth, + currentHealth, + }: { + maxHealth: number; + currentHealth: number; + }): HealingObject { + if (maxHealth < 0) throw new Error('MaxHealth cannot be negative'); + if (currentHealth < 0) throw new Error('CurrentHealth cannot be negative'); + if (currentHealth > maxHealth) throw new Error('CurrentHealth cannot exceed maxHealth'); + const status = + currentHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const }; + return new HealingObject(currentHealth, maxHealth, status); + } + + get health(): number { + return this.#health; + } + + get maxHealth(): number { + return this.#maxHealth; + } + + get status(): ObjectStatus { + return this.#status; + } + + /** Use this object to heal a character. Returns updated object and character. */ + heal(character: Character, amount: number): { object: HealingObject; character: Character } { + // Destroyed objects can't heal + if (this.#status.kind === 'destroyed') { + return { object: this, character }; + } + // Negative amount is invalid + if (amount < 0) throw new Error('Heal amount must be non-negative'); + // Calculate actual heal amount: min of requested, object remaining, character headroom + const objectRemaining = this.#health; + const characterMax = character.level.value >= 6 ? 1500 : 1000; + const characterHeadroom = characterMax - character.health.value; + const actualHeal = Math.min(amount, objectRemaining, characterHeadroom); + // If actualHeal is 0, nothing changes + if (actualHeal === 0) { + return { object: this, character }; + } + // Create updated object + const newObjectHealth = this.#health - actualHeal; + const newObjectStatus = + newObjectHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const }; + // Create updated character + const newCharacterHealth = character.health.value + actualHeal; + const newCharacter = Character.createWithHealth({ + name: character.name, + level: character.level, + health: newCharacterHealth, + }); + return { + object: new HealingObject(newObjectHealth, this.#maxHealth, newObjectStatus), + character: newCharacter, + }; + } +} diff --git a/src/MagicalWeapon.ts b/src/MagicalWeapon.ts new file mode 100644 index 0000000..c0a66b1 --- /dev/null +++ b/src/MagicalWeapon.ts @@ -0,0 +1,99 @@ +/** + * Magical Weapon — a Magical Object that deals fixed damage. + * + * Invariants enforced at construction: + * - Health is non-negative + * - Health never exceeds maxHealth + * - Damage is non-negative + */ +import { Character } from './Character.ts'; + +export type WeaponStatus = { kind: 'alive' } | { kind: 'destroyed' }; + +export class MagicalWeapon { + readonly #health: number; + readonly #maxHealth: number; + readonly #status: WeaponStatus; + readonly #damage: number; + readonly #owner: Character; + + private constructor( + health: number, + maxHealth: number, + status: WeaponStatus, + damage: number, + owner: Character, + ) { + this.#health = health; + this.#maxHealth = maxHealth; + this.#status = status; + this.#damage = damage; + this.#owner = owner; + } + + static create({ + maxHealth, + damage, + owner, + }: { + maxHealth: number; + damage: number; + 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(maxHealth, maxHealth, { kind: 'alive' }, damage, owner); + } + + get health(): number { + return this.#health; + } + + get maxHealth(): number { + return this.#maxHealth; + } + + get status(): WeaponStatus { + return this.#status; + } + + get damage(): number { + return this.#damage; + } + + get owner(): Character { + return this.#owner; + } + + /** Use this weapon to deal damage. Returns updated weapon and target. */ + use(target: Character): { weapon: MagicalWeapon; target: Character } { + // Destroyed weapons can't be used + if (this.#status.kind === 'destroyed') { + return { weapon: this, target }; + } + // Deal fixed damage + const newTargetHealth = Math.max(0, target.health.value - this.#damage); + const newTargetStatus = newTargetHealth === 0 ? { kind: 'dead' as const } : target.status; + const newTarget = Character.createWithHealthAndStatus({ + name: target.name, + level: target.level, + health: newTargetHealth, + status: newTargetStatus, + }); + // Reduce weapon health by 1 + const newWeaponHealth = this.#health - 1; + const newWeaponStatus = + newWeaponHealth === 0 ? { kind: 'destroyed' as const } : { kind: 'alive' as const }; + return { + weapon: new MagicalWeapon( + newWeaponHealth, + this.#maxHealth, + newWeaponStatus, + this.#damage, + this.#owner, + ), + + target: newTarget, + }; + } +} diff --git a/src/magical-objects.spec.ts b/src/magical-objects.spec.ts new file mode 100644 index 0000000..6a6fc36 --- /dev/null +++ b/src/magical-objects.spec.ts @@ -0,0 +1,360 @@ +import fc from 'fast-check'; +import { describe, it } from 'vitest'; +import { Character } from './Character.ts'; +import { Level } from './Level.ts'; +import { MagicalWeapon } from './MagicalWeapon.ts'; +import { HealingObject } from './HealingObject.ts'; + +describe('Magical Objects', () => { + describe('WeaponDealsDamage', () => { + it('property: weapon deals its fixed damage amount', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 10 }), + (damage, weaponHP, level) => { + const attacker = Character.create({ name: 'hero', level: Level.create(level) }); + const target = Character.create({ name: 'goblin', level: Level.create(level) }); + const weapon = MagicalWeapon.create({ + damage, + maxHealth: weaponHP, + owner: attacker, + }); + const result = attacker.useWeapon(weapon, target); + return result.target.health.value === Math.max(0, 1000 - damage); + }, + ), + ); + }); + + it('property: weapon health decreases by 1 after use', () => { + fc.assert( + fc.property( + fc.integer({ min: 2, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (weaponHP, damage) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker }); + const result = attacker.useWeapon(weapon, target); + return result.weapon.health === weaponHP - 1; + }, + ), + ); + }); + + it('property: weapon is destroyed when health reaches 0', () => { + fc.assert( + fc.property(fc.integer({ min: 1, max: 500 }), (damage) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: 1, owner: attacker }); + const result = attacker.useWeapon(weapon, target); + return result.weapon.status.kind === 'destroyed'; + }), + ); + }); + + it('property: weapon remains alive when health > 0 after use', () => { + fc.assert( + fc.property( + fc.integer({ min: 2, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (weaponHP, damage) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker }); + const result = attacker.useWeapon(weapon, target); + return result.weapon.status.kind === 'alive'; + }, + ), + ); + }); + }); + + describe('DeadCannotUseWeapon', () => { + it('property: dead character cannot use weapon — state unchanged', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (damage, weaponHP) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + 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 weaponHPBefore = weapon.health; + const targetHealthBefore = target.health.value; + const result = deadAttacker.useWeapon(weapon, target); + return ( + result.weapon.health === weaponHPBefore && + result.target.health.value === targetHealthBefore + ); + }, + ), + ); + }); + }); + + describe('NonOwnerCannotUseWeapon', () => { + it('property: non-owner cannot use weapon — state unchanged', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (damage, weaponHP) => { + const owner = Character.create({ name: 'owner', level: Level.create(1) }); + const thief = Character.create({ name: 'thief', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner }); + const weaponHPBefore = weapon.health; + const targetHealthBefore = target.health.value; + const result = thief.useWeapon(weapon, target); + return ( + result.weapon.health === weaponHPBefore && + result.target.health.value === targetHealthBefore + ); + }, + ), + ); + }); + }); + + describe('DestroyedWeaponCannotDealDamage', () => { + it('property: destroyed weapon cannot deal damage — state unchanged', () => { + fc.assert( + fc.property(fc.integer({ min: 1, max: 500 }), (damage) => { + const owner = Character.create({ name: 'owner', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: 1, owner }); + // Destroy the weapon first + const firstUse = owner.useWeapon(weapon, target); + const destroyedWeapon = firstUse.weapon; + const targetHealthBefore = firstUse.target.health.value; + // Try to use again on the destroyed weapon + const result = owner.useWeapon(destroyedWeapon, firstUse.target); + return result.weapon.health === 0 && result.target.health.value === targetHealthBefore; + }), + ); + }); + }); + + describe('HealingObjectHealsCharacter', () => { + it('property: healing object gives health up to its remaining health', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (objectHP, healAmount, characterHealth) => { + fc.pre(healAmount >= objectHP); + fc.pre(characterHealth + objectHP <= 1000); + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, healAmount); + return result.character.health.value === characterHealth + objectHP; + }, + ), + ); + }); + + it('property: healing object gives health up to character max when object has more', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 900, max: 999 }), + (objectHP, healAmount, characterHealth) => { + fc.pre(objectHP >= healAmount); + fc.pre(characterHealth + healAmount > 1000); + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, healAmount); + return result.character.health.value === 1000; + }, + ), + ); + }); + + it('property: healing object health decreases by actual healed amount', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 999 }), + (objectHP, healAmount, characterHealth) => { + fc.pre(characterHealth + healAmount <= 1000); + fc.pre(healAmount <= objectHP); + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, healAmount); + return result.object.health === objectHP - healAmount; + }, + ), + ); + }); + + it('property: healing object is destroyed when health reaches 0', () => { + fc.assert( + fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => { + // Character needs enough headroom to accept all object health + const characterHealth = Math.max(1, 1000 - objectHP); + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, objectHP); + return result.object.status.kind === 'destroyed'; + }), + ); + }); + + it('property: healing object remains alive when health > 0 after use', () => { + fc.assert( + fc.property( + fc.integer({ min: 2, max: 500 }), + fc.integer({ min: 1, max: 999 }), + (objectHP, characterHealth) => { + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, 1); + return result.object.status.kind === 'alive'; + }, + ), + ); + }); + }); + + describe('DeadCannotUseHealingObject', () => { + it('property: dead character cannot use healing object — state unchanged', () => { + fc.assert( + fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => { + const character = Character.create({ name: 'hero', level: Level.create(1) }); + 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 objectHPBefore = object.health; + const characterHealthBefore = deadCharacter.health.value; + const result = deadCharacter.useHealingObject(object, 100); + return ( + result.object.health === objectHPBefore && + result.character.health.value === characterHealthBefore + ); + }), + ); + }); + }); + + describe('DestroyedHealingObjectCannotHeal', () => { + it('property: destroyed healing object cannot heal — state unchanged', () => { + fc.assert( + fc.property(fc.integer({ min: 1, max: 500 }), (objectHP) => { + // Character needs headroom to drain the object + const characterHealth = Math.max(1, 1000 - objectHP); + const character = Character.createWithHealth({ + name: 'hero', + level: Level.create(1), + health: characterHealth, + }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + // Drain the object to 0 + const firstUse = character.useHealingObject(object, objectHP); + const destroyedObject = firstUse.object; + const healedCharacter = firstUse.character; + const characterHealthBefore = healedCharacter.health.value; + // Try to use again on the destroyed object + const result = healedCharacter.useHealingObject(destroyedObject, 100); + return ( + result.object.health === 0 && result.character.health.value === characterHealthBefore + ); + }), + ); + }); + }); + + describe('Invariants', () => { + it('property: weapon health never goes negative', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 10000 }), + (weaponHP, damage) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker }); + const result = attacker.useWeapon(weapon, target); + return result.weapon.health >= 0; + }, + ), + ); + }); + + it('property: healing object health never goes negative', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 10000 }), + (objectHP, healAmount) => { + const character = Character.create({ name: 'hero', level: Level.create(1) }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, healAmount); + return result.object.health >= 0; + }, + ), + ); + }); + + it('property: weapon health never exceeds maxHealth', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 500 }), + (weaponHP, damage) => { + const attacker = Character.create({ name: 'hero', level: Level.create(1) }); + const target = Character.create({ name: 'goblin', level: Level.create(1) }); + const weapon = MagicalWeapon.create({ damage, maxHealth: weaponHP, owner: attacker }); + const result = attacker.useWeapon(weapon, target); + return result.weapon.health <= weaponHP; + }, + ), + ); + }); + + it('property: healing object health never exceeds maxHealth', () => { + fc.assert( + fc.property( + fc.integer({ min: 1, max: 500 }), + fc.integer({ min: 1, max: 10000 }), + (objectHP, healAmount) => { + const character = Character.create({ name: 'hero', level: Level.create(1) }); + const object = HealingObject.create({ maxHealth: objectHP, currentHealth: objectHP }); + const result = character.useHealingObject(object, healAmount); + return result.object.health <= objectHP; + }, + ), + ); + }); + }); +}); diff --git a/transcripts/forgot-to-commit.html b/transcripts/forgot-to-commit.html new file mode 100644 index 0000000..e1572a8 --- /dev/null +++ b/transcripts/forgot-to-commit.html @@ -0,0 +1,13112 @@ + + + + + + Session Export + + + + + +
+ + +
+
+
+
+
+ +
+
+ + + + + + + + + + + + +