// ----------------------------------------------------------------- // frogs.txt: toads and frogs // Concrete Abstractions: Puzzles and Games // (c) 2020, Wolfgang Schreiner, RISC, JKU Linz, Austria // ----------------------------------------------------------------- // toads, spaces, and frogs val T = 3; val S = 2; val F = 3; val N = T+S+F; axiom notZero ⇔ N > 0; type Player = ℕ[2]; val none = 0; val toad = 1; val frog = 2; type Strip = Array[N,Player]; type Pos = ℕ[N-1]; // ----------------------------------------------------------------- // the puzzle // ----------------------------------------------------------------- pred goal(s:Strip) ⇔ (∀i:Pos with i < F. s[i] = frog) ∧ (∀i:Pos with i < T. s[F+S+i] = toad); val L:ℕ; shared system ToadsAndFrogsPuzzle { var s:Strip = Array[N,Player](none); var len:ℕ[L] = 0; // invariant ¬goal(s); invariant goal(s) ⇒ printtrace in ⊤; init() { for var i:ℕ[T] := 0; i < T; i ≔ i+1 do invariant 0 ≤ i ∧ i ≤ T; decreases T-i; s[i] = toad; for var i:ℕ[F] := 0; i < F; i ≔ i+1 do invariant 0 ≤ i ∧ i ≤ F; decreases F-i; s[i+T+S] = frog; } action toadMove(i:Pos) with len < L ∧ s[i] = toad ∧ i+1 < N ∧ s[i+1] = none; { s[i+1] ≔ s[i]; s[i] ≔ none; len ≔ len+1; } action toadHop(i:Pos) with len < L ∧ s[i] = toad ∧ i+2 < N ∧ s[i+1] = frog ∧ s[i+2] = none; { s[i+2] ≔ s[i]; s[i] ≔ none; len ≔ len+1; } action frogMove(i:Pos) with len < L ∧ s[i] = frog ∧ i-1 ≥ 0 ∧ s[i-1] = none; { s[i-1] ≔ s[i]; s[i] ≔ none; len ≔ len+1; } action frogHop(i:Pos) with len < L ∧ s[i] = frog ∧ i-2 ≥ 0 ∧ s[i-1] = toad ∧ s[i-2] = none; { s[i-2] ≔ s[i]; s[i] ≔ none; len ≔ len+1; } } // ----------------------------------------------------------------- // the game // ----------------------------------------------------------------- fun dir(p:Player):ℤ[-1,1] requires p ≠ none; = if p = toad then 1 else -1; fun other(p:Player):Player requires p ≠ none; = 3-p; pred admissible(s:Strip,p:Player,i:Pos) requires p ≠ none; ⇔ s[i] = p ∧ let d = dir(p) in (let i0 = i+d in 0 ≤ i0 ∧ i0 < N ∧ s[i0] = none) ∨ (let i0 = i+d, i1 = i0+d in 0 ≤ i1 ∧ i1 < N ∧ s[i0] = other(p) ∧ s[i1] = none); fun step(s:Strip,p:Player,i:Pos):Strip = let d = dir(p) in if s[i+d] = none then s with [i+d] = p with [i] = none else s with [i+2⋅d] = p with [i] = none; pred win(s:Strip,p:Player,i:Pos) requires p ≠ none; ⇔ admissible(s,p,i) ∧ let s0 = step(s,p,i), p0 = other(p) in ¬∃i0:Pos. win(s0,p0,i0); pred winnable(s:Strip,p:Player) requires p ≠ none; ⇔ ∃i:Pos. win(s,p,i); shared system ToadsAndFrogsGame { var s:Strip = Array[N,Player](none); var p:Player = toad; invariant p = toad ∨ p = frog; // invariant ∃i:Pos. admissible(s,p,i); invariant (¬∃i:Pos. admissible(s,p,i)) ⇒ printtrace in ⊤; init() { for var i:ℕ[T] := 0; i < T; i ≔ i+1 do invariant 0 ≤ i ∧ i ≤ T ∧ p = old_p; decreases T-i; s[i] = toad; for var i:ℕ[F] := 0; i < F; i ≔ i+1 do invariant 0 ≤ i ∧ i ≤ F ∧ p = old_p; decreases F-i; s[i+T+S] = frog; print winnable(s,p); } action step(i:Pos) with if winnable(s,p) then win(s,p,i) else admissible(s,p,i); { s ≔ step(s,p,i); p ≔ other(p); } } // ----------------------------------------------------------------- // end of file // -----------------------------------------------------------------