-- solitaire.csp

-- version for FDR2

-- Bill Roscoe

-- This file implements the system  described in Section 15.1

-- SETTING UP THE BOARD

-- As described in the text, we use a notation for describing boards that
-- looks like physical boards

datatype Pictel = X | P | E | S 

-- Here are four, of which the first is the standard:
-- X is a non-slot,
-- E is an empty one
-- P or S is a full one
-- S is a "sticky" peg as described in the text.

-- We could pick a variety of boards to try and solve.  The first one
-- here is the standard one

Board1 = <<X,X,P,P,P,X,X>,
          <X,X,P,P,P,X,X>,
          <S,S,P,P,P,P,P>,
          <P,P,P,E,P,P,P>,
          <S,S,P,P,P,P,P>,
          <X,X,S,P,S,X,X>,
          <X,X,S,P,S,X,X>>

-- Of the following, some are soluble and some are not.  Unlike the first
-- one I have not set which pegs should be "sticky" for tactic 2.  Where
-- necessary you could experiment with this and other tactics yourself.

Board2 = <<X,X,X,S,X,X,X>,
          <X,X,S,S,S,X,X>,
          <X,P,P,P,P,P,X>,
          <P,P,P,E,P,P,P>,
          <X,S,P,P,P,P,X>,
          <X,X,P,P,P,X,X>,
          <X,X,X,P,X,X,X>>

Board3 = <<X,X,P,P,P,X,X>,
          <X,P,P,P,P,P,X>,
          <P,P,P,P,P,P,P>,
          <P,P,P,E,P,P,P>,
          <P,P,P,P,P,P,P>,
          <X,P,P,P,P,P,X>,
          <X,X,P,P,P,X,X>>

Board4 = <<X,X,X,S,S,S,X,X,X>,
          <X,X,X,S,S,S,X,X,X>,
          <S,S,S,P,P,P,P,P,P>,
          <S,S,P,P,E,P,P,P,P>,
          <S,S,S,P,P,P,P,P,P>,
          <X,X,X,P,P,P,X,X,X>,
          <X,X,X,P,P,P,X,X,X>>

Board5 = <<X,X,P,P,P,X,X>,
          <P,P,P,P,P,P,P>,
          <P,P,P,E,P,P,P>,
          <P,P,P,P,P,P,P>,
          <X,X,P,P,P,X,X>>


-- The following sets up which board the rest of the script uses.  
-- I strongly recommend you
-- only investigate most of the other examples above using appropriate tactics
-- to limit the state coverage.

Board = Board1

-- Having made our choice of board, we can map it to a system of processes
-- The following manipulations are designed to make the above notation
-- easy to access

Height = #Board
Width = #(head(Board))

nth(n,xs) = if n==0 then head(xs) 
                    else nth(n-1,tail(xs))

init(i,j) = nth(j,nth(Height-1-i,Board))

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

-- As discussed in the book, we use an enlarged board in declaring the
-- possible move events:

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

channel up,down,left,right:Ycoords.Xcoords
channel done

-- SLOT PROCESSES

Full(i,j,target) = (target==P) & done -> Full(i,j,target)
                  [] up.i+2.j -> Empty(i,j,target)
                  [] down.i-2.j -> Empty(i,j,target)
                  [] right.i.j+2 -> Empty(i,j,target)
                  [] left.i.j-2 -> Empty(i,j,target)
                  [] up.i+1.j -> Empty(i,j,target)
                  [] down.i-1.j -> Empty(i,j,target)
                  [] right.i.j+1 -> Empty(i,j,target)
                  [] left.i.j-1 -> Empty(i,j,target)

Empty(i,j,target) = (target==E) & done -> Empty(i,j,target)
                  [] up.i.j -> Full(i,j,target)
                  [] down.i.j -> Full(i,j,target)
                  [] right.i.j -> Full(i,j,target)
                  [] left.i.j -> Full(i,j,target)

Slot(i,j) = if init(i,j) == E then Empty(i,j,P)
                              else Full(i,j,E)

-- Each slot process has to co-operate in each move event
-- that it can participate in.

Alpha(i,j) = Union({{done},
                    {up.i+k.j    | k <-{0,1,2}},
                    {down.i-k.j  | k <-{0,1,2}},
                    {left.i.j-k  | k <-{0,1,2}},
                    {right.i.j+k | k <-{0,1,2}}})

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

JumpTos = {up.i.j, down.i.j, left.i.j, right.i.j | (i,j) <- BoardCoords}

JumpOvers = {up.i+1.j, down.i-1.j, left.i.j-1, 
             right.i.j+1 | (i,j) <- BoardCoords}

JumpFroms = {up.i+2.j, down.i-2.j, left.i.j-2, 
             right.i.j+2 | (i,j) <- BoardCoords}

RealMoves = inter(JumpTos,inter(JumpOvers,JumpFroms))

-- so we can calculate which moves the processes perform that are
-- not allowed.


OffBoardMoves = diff({|up,down,left,right|},RealMoves)

-- The CSP description of the puzzle is just the following process,
-- which can perform just the sequences of moves that are legal for the
-- puzzle and can communicate done just when the puzzle has been solved.

Puzzle = (|| (i,j):BoardCoords @ [Alpha(i,j)] Slot(i,j)) [|OffBoardMoves|] STOP

assert STOP [T= Puzzle \ {|up,down,left,right|}

-- But, at least for the standard board, there are too many states in
-- this system for the check to complete on ordinary computers.
-- So we can cut the state-space by seeing if there are solutions
-- obeying some additional rules.  The following says that moves in the
-- four directions rotate strictly:

Tactic1 = left?x -> Tactic1' 
Tactic1' = up?x -> Tactic1'' 
Tactic1'' = right?x -> Tactic1''' 
Tactic1''' = down?x -> Tactic1 

PuzzleWithTactic1 = Puzzle [|RealMoves|] (Tactic1 [|OffBoardMoves|] STOP)

-- For the standard board this fails, meaning there is no such solution.

assert STOP [T= PuzzleWithTactic1 \ {|up,down,left,right|}

-- For tactic 2 we adopt the "sticky" peg approach described in the text
-- and prevent pegs labelled S from moving until there are a given
-- number left.

NoDelays = card({(i,j) | (i,j) <- BoardCoords, init(i,j) == P})

Delaymoves = diff(Union({Alpha(i,j) | (i,j) <- BoardCoords, init(i,j)==S}),
                  {done})

Nodelaymoves = diff(RealMoves,Delaymoves)

Tactic2(n) = if n==0 then []x:RealMoves @ x -> Tactic2(0)
                     else []x:Nodelaymoves @ x -> Tactic2(n-1)

-- The higher the following number the more states are found and
-- the more likely you are to find a solution if there is one.

NonStickyAllowance = 4

Puzzle2 = Puzzle [|RealMoves|] Tactic2(NoDelays-NonStickyAllowance)

assert STOP [T= Puzzle2 \ {|up,down,left,right|}

-- Clearly the tactics can be varied or combined.