// ----------------------------------------------------------------- // husbands.txt: the jealous husbands problem. // Concrete Abstractions: Puzzles and Games // (c) 2020, Wolfgang Schreiner, RISC, JKU Linz, Austria // ----------------------------------------------------------------- // the number of pairs val N:ℕ; // the entities to be transfered across the river (entry 0 is the boat) type Entity = ℕ[2⋅N]; val boat = 0; type Place = Bool; val left = ⊥; val right = ⊤; type Placement = Map[Entity,Place]; pred isWoman(e:Entity) ⇔ 1 ≤ e ∧ e ≤ N; pred isMan(e:Entity) ⇔ e > N; fun husbandOf(e:Entity):Entity requires isWoman(e); = e+N; fun other(p:Place):Place = ¬p; // ----------------------------------------------------------------- // the rules of the game // ----------------------------------------------------------------- // movement of e1 and e2 is safe pred safe(e1:Entity,e2:Entity) ⇔ (isWoman(e1) ∧ isMan(e2) ⇒ e2 = husbandOf(e1)) ∧ (isWoman(e2) ∧ isMan(e1) ⇒ e1 = husbandOf(e2)); // placement p is safe pred safe(p:Placement) ⇔ ∀e1:Entity with isWoman(e1) ∧ (∃e2:Entity. isMan(e2) ∧ p[e1] = p[e2]). p[e1] = p[husbandOf(e1)]; val L:ℕ; shared system River { var p:Placement ≔ Map[Entity,Place](left); var len:Nat[L] = 0; invariant ¬∀e:Entity. p[e] = right; action move1(e:Entity) with len < L ∧ e ≠ boat ∧ p[e] = p[boat] ∧ let q = other(p[boat]), p0 = p with [boat] = q with [e] = q in safe(p0); { val q = other(p[boat]); p[boat] ≔ q; p[e] ≔ q; len ≔ len+1; } action move2(e1:Entity,e2:Entity) with len < L ∧ e1 ≠ e2 ∧ e1 ≠ boat ∧ e2 ≠ boat ∧ p[e1] = p[boat] ∧ p[e2] = p[boat] ∧ let q = other(p[boat]), p0 = p with [boat] = q with [e1] = q with [e2] = q in safe(e1,e2) ∧ safe(p0); { val q = other(p[boat]); p[boat] ≔ q; p[e1] ≔ q; p[e2] ≔ q; len ≔ len+1; } } // ----------------------------------------------------------------- // end of file // -----------------------------------------------------------------