3by3_nreturn_2robots.fcr

/* Process */

process play is
   states move
   var x1 : 0..4 := 1,
       y1 : 0..4 := 1,
       x2 : 0..4 := 2,
       y2 : 0..4 := 1,
       lx1 : 0..4 := 0,
       ly1 : 0..4 := 0,
       lx2 : 0..4 := 0,
       ly2 : 0..4 := 0,
      a : array 5 of array 5 of nat := [[1,1,1,1,1],
                                        [1,0,0,0,1],
                                        [1,0,0,0,1],
                                        [1,0,0,0,1],
                                        [1,1,1,1,1]]

   from move
      select
         on a[y1][x1-1]=0 and not (x1-1=x2 and y1=y2) and not (x1-1=lx1 and y1=ly1); lx1 := x1; ly1 :=y1; x1 := x1-1; to move
      [] on a[y1][x1+1]=0 and not (x1+1=x2 and y1=y2) and not (x1+1=lx1 and y1=ly1); lx1 := x1; ly1 :=y1; x1 := x1+1; to move
      [] on a[y1-1][x1]=0 and not (x1=x2 and y1-1=y2) and not (x1=lx1 and y1-1=ly1); lx1 := x1; ly1 :=y1; y1 := y1-1; to move
      [] on a[y1+1][x1]=0 and not (x1=x2 and y1+1=y2) and not (x1=lx1 and y1+1=ly1); lx1 := x1; ly1 :=y1; y1 := y1+1; to move
      [] on a[y2][x2-1]=0 and not (x2-1=x1 and y2=y1) and not (x2-1=lx2 and y2=ly2); lx2 := x2; ly2 :=y2; x2 := x2-1; to move
      [] on a[y2][x2+1]=0 and not (x2+1=x1 and y2=y1) and not (x2+1=lx2 and y2=ly2); lx2 := x2; ly2 :=y2; x2 := x2+1; to move
      [] on a[y2-1][x2]=0 and not (x2=x1 and y2-1=y1) and not (x2=lx2 and y2-1=ly2); lx2 := x2; ly2 :=y2; y2 := y2-1; to move
      [] on a[y2+1][x2]=0 and not (x2=x1 and y2+1=y1) and not (x2=lx2 and y2+1=ly2); lx2 := x2; ly2 :=y2; y2 := y2+1; to move
      end


/* Entry point */

play