-- The  Knight's Tour

-- A board with dimensions Width x Height
Width = 9
Height = 3


BoardCoords = {(i,j) | i <- {1..Width}, j <- {1..Height}}

-- As with the peg solitaire example, we use an enlarged board in 
-- declaring the possible move events:

Xcoords = {(-1)..Width+2}
Ycoords = {(-1)..Height+2}


-- visit.i.j  indicates that the knight has arrived at position (i,j)
channel visit: Xcoords.Ycoords

channel done



-- Each square on the board has either been visited or not

Visited(i,j) =  
	done -> Visited(i,j)
     []	visit?x:diff(Xcoords,{i})?y -> Visited(i,j)
     []	visit?x?y:diff(Ycoords,{j}) -> Visited(i,j)


JustVisited(i,j) =  
	done -> JustVisited(i,j)
     []	visit.i+2.j+1 -> Visited(i,j)
     []	visit.i+2.j-1 -> Visited(i,j)
     []	visit.i-2.j+1 -> Visited(i,j)
     []	visit.i-2.j-1 -> Visited(i,j)
     []	visit.i+1.j+2 -> Visited(i,j)
     []	visit.i+1.j-2 -> Visited(i,j)
     []	visit.i-1.j+2 -> Visited(i,j)
     []	visit.i-1.j-2 -> Visited(i,j)

NotVisited(i,j) =  
     	visit?x?y -> if (x,y) == (i,j)
                        then JustVisited(i,j)
                        else NotVisited(i,j)

-- The "real moves" are those where all three slots involved are
-- actually on the board:

RealMoves = union({done},{visit.i.j | (i,j) <- BoardCoords})

BadMoves = diff({|visit|},RealMoves)



Tour = ([|RealMoves|] (i,j):BoardCoords @ NotVisited(i,j)) [| BadMoves |] STOP

Tactic1 = visit.1?x -> visit.3?y -> visit.4?z -> Tactic1'

Tactic1' = visit?x:{1..Width}?y:{1..Height} -> Tactic1'
        [] done -> STOP

Tactic2 = visit?x?y -> visit.((x+1)%Width)+1.((y+2)%Height)+1 
                    -> visit.((x-1)%Width)+1.((y+1)%Height)+1 -> Tactic2

Tact1 = Tactic1 [| BadMoves|] STOP
Tact2 = Tactic2 [| BadMoves|] STOP

assert STOP [T= Tour \ diff(Events,{done})

assert STOP [T= (Tour [|RealMoves|] Tact1) \ diff(Events,{done})
assert STOP [T= (Tour [|RealMoves|] Tact2) \ diff(Events,{done})