#define TABLE 254
#define HAND 255
#define EMPTY 253

/*
  Initial:	Goal:
  3 5		3
  0 4		5
  2 1 6 7 	4
		7
		2
		0
		6
		1
*/

byte on0=2, on1=TABLE, on2=TABLE, on3=0, on4=1, on5=4, on6=TABLE, on7=TABLE;
byte clear0=0, clear1=0, clear2=0, clear3=1, clear4=0, clear5=1, clear6=1, clear7=1;
bit done=0;
byte holding = EMPTY;

#define PRICK_FROM_TABLE()\
::  atomic {clear0==1 && on0==TABLE;on0 = HAND;clear0 = 0;holding = 0;}  goto fullhand;\
::  atomic {clear1==1 && on1==TABLE;on1 = HAND;clear1 = 0;holding = 1;}  goto fullhand;\
::  atomic {clear2==1 && on2==TABLE;on2 = HAND;clear2 = 0;holding = 2;}  goto fullhand;\
::  atomic {clear3==1 && on3==TABLE;on3 = HAND;clear3 = 0;holding = 3;}  goto fullhand;\
::  atomic {clear4==1 && on4==TABLE;on4 = HAND;clear4 = 0;holding = 4;}  goto fullhand;\
::  atomic {clear5==1 && on5==TABLE;on5 = HAND;clear5 = 0;holding = 5;}  goto fullhand;\
::  atomic {clear6==1 && on6==TABLE;on6 = HAND;clear6 = 0;holding = 6;}  goto fullhand;\
::  atomic {clear7==1 && on7==TABLE;on7 = HAND;clear7 = 0;holding = 7;}  goto fullhand;

#define PICK_FROM_BLOCK(CLEAR, ON, ID)\
:: atomic\
{\
  CLEAR==1 && ON!=TABLE;\
  if\
  ::ON==0; clear0=1;\
  ::ON==1; clear1=1;\
  ::ON==2; clear2=1;\
  ::ON==3; clear3=1;\
  ::ON==4; clear4=1;\
  ::ON==5; clear5=1;\
  ::ON==6; clear6=1;\
  ::ON==7; clear7=1;\
  fi;\
  ON=HAND;\
  CLEAR=0;\
  holding=ID;\
} goto fullhand;

#define PUT_ON_BLOCK(CLEAR, ID)\
:: atomic\
{\
  CLEAR==1;\
  CLEAR=0;\
  if\
  ::holding==0; clear0=1; on0=ID;\
  ::holding==1; clear1=1; on1=ID;\
  ::holding==2; clear2=1; on2=ID;\
  ::holding==3; clear3=1; on3=ID;\
  ::holding==4; clear4=1; on4=ID;\
  ::holding==5; clear5=1; on5=ID;\
  ::holding==6; clear6=1; on6=ID;\
  ::holding==7; clear7=1; on7=ID;\
  fi;\
  holding=EMPTY;\
} goto emptyhand;

#define PUT_ON_TABLE()\
:: atomic\
{\
  if\
  ::holding==0; clear0 = 1; on0 = TABLE; holding = EMPTY;\
  ::holding==1; clear1 = 1; on1 = TABLE; holding = EMPTY;\
  ::holding==2; clear2 = 1; on2 = TABLE; holding = EMPTY;\
  ::holding==3; clear3 = 1; on3 = TABLE; holding = EMPTY;\
  ::holding==4; clear4 = 1; on4 = TABLE; holding = EMPTY;\
  ::holding==5; clear5 = 1; on5 = TABLE; holding = EMPTY;\
  ::holding==6; clear6 = 1; on6 = TABLE; holding = EMPTY;\
  ::holding==7; clear7 = 1; on7 = TABLE; holding = EMPTY;\
  fi;\
} goto emptyhand;


active proctype Hand()
{
  emptyhand: if
    :: on3==5 && on5==4 && on4==7 && on7==2 && on2==0 && on0==6 && on6==1; done=1; goto out; 
    PRICK_FROM_TABLE()
    PICK_FROM_BLOCK(clear0, on0, 0)
    PICK_FROM_BLOCK(clear1, on1, 1)
    PICK_FROM_BLOCK(clear2, on2, 2)
    PICK_FROM_BLOCK(clear3, on3, 3)
    PICK_FROM_BLOCK(clear4, on4, 4)
    PICK_FROM_BLOCK(clear5, on5, 5)
    PICK_FROM_BLOCK(clear6, on6, 6)
    PICK_FROM_BLOCK(clear7, on7, 7)
  fi;

  fullhand: if
    PUT_ON_BLOCK(clear0, 0)
    PUT_ON_BLOCK(clear1, 1)
    PUT_ON_BLOCK(clear2, 2)
    PUT_ON_BLOCK(clear3, 3)
    PUT_ON_BLOCK(clear4, 4)
    PUT_ON_BLOCK(clear5, 5)
    PUT_ON_BLOCK(clear6, 6)
    PUT_ON_BLOCK(clear7, 7)
    PUT_ON_TABLE()
  fi;
out: skip;
}

never
{
again:
  if
    ::true; goto again;
    ::done;
  fi;
}