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

/*
  Initial:	Goal:
  1		3
  2		2
  0		0
  3		1
*/

byte on0=3, on1=2, on2=0, on3=TABLE;
byte clear0=0, clear1=1, clear2=0, clear3=0;
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;

#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;\
  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;\
  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;\
  fi;\
} goto emptyhand;


active proctype Hand()
{
  emptyhand: if
    :: on3==2 && on2==0 && on0==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)
  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_TABLE()
  fi;
out: skip;
}

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

