/* adapted from: http://anna.fi.muni.cz/models/cgi/model_info.cgi?name=sokoban#pmnote 0 = free 1 = wall 2 = box person is represented by x,y */ /* Process */ process play is states move, done var x : 0..9 := 1, y : 0..5 := 1, a : array 6 of array 10 of nat := [[1,1,1,1,1,1,1,1,1,1], [1,0,0,0,1,0,0,0,0,1], [1,0,2,0,2,0,0,0,0,1], [1,0,2,2,2,1,1,0,0,1], [1,0,0,0,0,1,1,1,1,1], [1,1,1,1,1,1,1,1,1,1]] from move select on a[1][8] = 2 and a[2][7] = 2 and a[2][8] = 2 and a[3][7] = 2 and a[3][8] = 2; to done /* moves */ [] on a[y][x-1]=0; x := x-1; to move [] on a[y][x+1]=0; x := x+1; to move [] on a[y-1][x]=0; y := y-1; to move [] on a[y+1][x]=0; y := y+1; to move /* pushes */ [] on a[y][x-1]=2 and a[y][x-2]=0; a[y][x-2]:=2; a[y][x-1]:=0; x:=x-1; to move [] on a[y][x+1]=2 and a[y][x+2]=0; a[y][x+2]:=2; a[y][x+1]:=0; x:=x+1; to move [] on a[y-1][x]=2 and a[y-2][x]=0; a[y-2][x]:=2; a[y-1][x]:=0; y:=y-1; to move [] on a[y+1][x]=2 and a[y+2][x]=0; a[y+2][x]:=2; a[y+1][x]:=0; y:=y+1; to move end /* Entry point */ play /* Properties */ property impossible is ltl ([] not (play/state done)) assert impossible