add new benchmark MMG for Bristlecone
authorjzhou <jzhou>
Tue, 2 Sep 2008 03:57:29 +0000 (03:57 +0000)
committerjzhou <jzhou>
Tue, 2 Sep 2008 03:57:29 +0000 (03:57 +0000)
12 files changed:
Robust/src/Benchmarks/MMG/Java/Ghost.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Java/MMG.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Java/Map.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Java/Pacman.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Nor/Ghost.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Nor/MMG.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Nor/Map.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Nor/Pacman.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Tag/Ghost.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Tag/MMG.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Tag/Map.java [new file with mode: 0755]
Robust/src/Benchmarks/MMG/Tag/Pacman.java [new file with mode: 0755]

diff --git a/Robust/src/Benchmarks/MMG/Java/Ghost.java b/Robust/src/Benchmarks/MMG/Java/Ghost.java
new file mode 100755 (executable)
index 0000000..8d1b169
--- /dev/null
@@ -0,0 +1,324 @@
+public class Ghost {\r
+    public int x;\r
+    public int y;\r
+    public int index;\r
+    public int target;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Ghost(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.index = -1;\r
+       this.target = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int pacman) {\r
+       this.target = pacman;\r
+    }\r
+    \r
+    // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    public void tryMove() {\r
+       //System.printString("step 1\n");\r
+       //System.printString("target: " + this.target + "\n");\r
+       \r
+       // Don't let the ghost go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.map.pacMenX[this.target];\r
+       //System.printString("aaa\n");\r
+       int targety = this.map.pacMenY[this.target];\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       if(targetx == -1) {\r
+           //System.printString("a\n");\r
+           // already kicked off, choose another target\r
+           int i = 0;\r
+           boolean found = false;\r
+           while((!found) && (i < map.pacMenX.length)) {\r
+               if(this.map.pacMenX[i] != -1) {\r
+                   this.target = i;\r
+                   targetx = this.map.pacMenX[i];\r
+                   targety = this.map.pacMenY[i];\r
+                   this.map.targets[i] = this.target;\r
+                   found = true;\r
+               }\r
+               i++;\r
+           }\r
+           //System.printString("b\n");\r
+           if(i == this.map.pacMenX.length) {\r
+               //System.printString("c\n");\r
+               // no more pacmen to chase\r
+               this.dx = 0;\r
+               this.dy = 0;\r
+               this.direction = 0;\r
+               return;\r
+           }\r
+           //System.printString("d\n");\r
+       }\r
+       getDestination (this.map.pacmen[this.target].direction, targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Java/MMG.java b/Robust/src/Benchmarks/MMG/Java/MMG.java
new file mode 100755 (executable)
index 0000000..170039c
--- /dev/null
@@ -0,0 +1,81 @@
+public class MMG {\r
+    public MMG() {}\r
+    \r
+    public static void main(String[] args) {\r
+       MMG mmg = new MMG();\r
+       \r
+       //System.printString("Startup\n");\r
+       int nrofpacs = 4;\r
+       int nrofghosts = 8;\r
+       Map map = new Map(nrofpacs, nrofghosts);\r
+       \r
+       // Initiate the map\r
+       map.init();\r
+           \r
+       int i = 0;\r
+       // create ghosts\r
+       for(i = 0; i < map.nrofghosts; i++) {\r
+           Ghost ghost = new Ghost(7, 7, map);\r
+           ghost.setTarget(i%map.nrofpacs);\r
+           ghost.index = i;\r
+           map.placeGhost(ghost);\r
+           map.targets[i] = ghost.target;\r
+           map.ghosts[i] = ghost;\r
+       }\r
+       // create pacmen\r
+       int tx = 14;\r
+       int ty = 14;\r
+       for(i = 0; i < map.nrofpacs; i++) {\r
+           Pacman pacman = new Pacman(5, 7, map);\r
+           pacman.setTarget(tx*(i/2), ty*(i%2));\r
+           pacman.index = i;\r
+           map.placePacman(pacman);\r
+           map.desX[i] = tx*(i/2);\r
+           map.desY[i] = ty*(i%2);\r
+           map.pacmen[i] = pacman;\r
+           //System.printString("destination: " + map.desX[i] + "," + map.desY[i] + "\n");\r
+       }\r
+\r
+       map.ghostcount = 0;\r
+       map.paccount = 0;\r
+       \r
+       while(map.nrofpacs > 0) {\r
+           // try to move ghost\r
+           for(i = 0; i < map.nrofghosts; i++) {\r
+               map.ghosts[i].tryMove();\r
+           }\r
+           // try to move pacmen\r
+           for(i = 0; i < map.nrofpacs; i++) {\r
+               map.pacmen[i].tryMove();\r
+           }\r
+           \r
+           // update ghosts\r
+           for(i = 0; i < map.nrofghosts; i++) {\r
+               map.ghosts[i].doMove();\r
+               map.placeGhost(map.ghosts[i]);\r
+           }\r
+           /*for(i = 0; i < map.nrofghosts; i++) {\r
+               System.printString("(" + map.ghostsX[i] + "," + map.ghostsY[i] + ") ");\r
+           }\r
+           System.printString("\n");*/\r
+           // update pacmen\r
+           for(i = 0; i < map.nrofpacs; i++) {\r
+               map.pacmen[i].doMove();\r
+               map.placePacman(map.pacmen[i]);\r
+               //System.printString("Pacman " + map.pacmen[i].index + ": (" + map.pacMenX[map.pacmen[i].index] + "," + map.pacMenY[map.pacmen[i].index] + ")\n");\r
+               boolean death = map.check(map.pacmen[i]);\r
+               /*if(death) {\r
+                   System.printString("Pacman " + map.pacmen[i].index + " caught!\n");\r
+               }*/\r
+           }\r
+           map.nrofpacs -= map.deathcount;\r
+           //System.printString(map.nrofpacs + " pacmen left. \n");\r
+           \r
+           // reset for next run\r
+           map.paccount = 0;\r
+           map.deathcount = 0;\r
+       }\r
+       \r
+       System.printString("Finish\n");\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Java/Map.java b/Robust/src/Benchmarks/MMG/Java/Map.java
new file mode 100755 (executable)
index 0000000..b82e07e
--- /dev/null
@@ -0,0 +1,122 @@
+public class Map {    \r
+    public int[] map;\r
+    public int[] pacMenX;\r
+    public int[] pacMenY;\r
+    public int[] ghostsX;\r
+    public int[] ghostsY;\r
+    public int[] targets;\r
+    public int[] desX;\r
+    public int[] desY;\r
+    public Ghost[] ghosts;\r
+    public Pacman[] pacmen;\r
+    \r
+    public int nrofghosts;\r
+    public int nrofpacs;\r
+    private int nrofblocks;\r
+    //public boolean toupdate;\r
+    public int ghostcount;\r
+    public int paccount;\r
+    public int deathcount;\r
+    \r
+    public Random r;\r
+    \r
+    public Map(int nrofpacs, int nrofghosts) {\r
+       //System.printString("step 1\n");\r
+       this.nrofblocks = 15;\r
+       this.map = new int[this.nrofblocks*this.nrofblocks];\r
+       this.nrofpacs = nrofpacs;\r
+       this.nrofghosts = nrofghosts;\r
+       this.pacMenX = new int[this.nrofpacs];\r
+       this.pacMenY = new int[this.nrofpacs];\r
+       this.ghostsX = new int[this.nrofghosts];\r
+       this.ghostsY = new int[this.nrofghosts];\r
+       this.targets = new int[this.nrofghosts];\r
+       this.desX = new int[this.nrofpacs];\r
+       this.desY = new int[this.nrofpacs];\r
+       this.ghosts = new Ghost[this.nrofghosts];\r
+       this.pacmen = new Pacman[this.nrofpacs];\r
+       //this.toupdate = false;\r
+       this.ghostcount = 0;\r
+       this.paccount = 0;\r
+       this.deathcount = 0;\r
+       this.r = new Random();\r
+       \r
+       //System.printString("step 2\n");\r
+       for(int i = 0; i < this.nrofpacs; i++) {\r
+           this.pacMenX[i] = this.pacMenY[i] = -1;\r
+           this.desX[i] = this.desY[i] = -1;\r
+           this.pacmen[i] = null;\r
+       }\r
+       //System.printString("step 3\n");\r
+       for(int i = 0; i < this.nrofghosts; i++) {\r
+           this.ghostsX[i] = this.ghostsY[i] = -1;\r
+           this.targets[i] = -1;\r
+           this.ghosts[i] = null;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    public void init() {\r
+       int i = 0;\r
+       this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=15;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=6;this.map[i++]=1;this.map[i++]=10;this.map[i++]=4;this.map[i++]=3;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=6;this.map[i++]=5;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=5;this.map[i++]=3;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=12;this.map[i++]=5;this.map[i++]=9;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=12;\r
+       this.map[i++]=6;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=3;\r
+       this.map[i++]=4;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=10;this.map[i++]=10;this.map[i++]=10;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=1;\r
+       this.map[i++]=12;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=10;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=9;\r
+       this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=2;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=8;this.map[i++]=4;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=1;this.map[i++]=8;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=2;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;this.map[i++]=13;this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12; // 15*15    \r
+    } \r
+\r
+    public void placePacman(Pacman t) {\r
+       this.pacMenX[t.index] = t.x;\r
+       this.pacMenY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 16;\r
+       this.paccount++;\r
+    }\r
+    \r
+    public void placeGhost(Ghost t) {\r
+       this.ghostsX[t.index] = t.x;\r
+       this.ghostsY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 32;\r
+       this.ghostcount++;\r
+    }\r
+    \r
+    public boolean check(Pacman t) {\r
+       boolean death = false;\r
+       int i = 0;\r
+       while((!death) && (i < this.nrofghosts)) {\r
+           if((t.x == this.ghostsX[i]) && (t.y == this.ghostsY[i])) {\r
+               death = true;\r
+           }\r
+           i++;\r
+       }\r
+       if((!death) && (t.x == t.tx) && (t.y == t.ty)) {\r
+           // reach the destination\r
+           //System.printString("Hit destination!\n");\r
+           death = true;\r
+       }\r
+       if(death) {\r
+           // pacman caught by ghost\r
+           // set pacman as death\r
+           t.death = true;\r
+           // kick it out\r
+           //this.map[t.y * this.nrofblocks + t.x - 1] -= 16;\r
+           this.deathcount++;\r
+           this.pacMenX[t.index] = -1;\r
+           this.pacMenY[t.index] = -1;\r
+       }\r
+       return death;\r
+    }\r
+    \r
+    public boolean isfinish() {\r
+       return nrofpacs == 0;\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Java/Pacman.java b/Robust/src/Benchmarks/MMG/Java/Pacman.java
new file mode 100755 (executable)
index 0000000..1ab4003
--- /dev/null
@@ -0,0 +1,301 @@
+public class Pacman {\r
+    public int x;\r
+    public int y;\r
+    public boolean death;\r
+    public int index;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    public int tx;\r
+    public int ty;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Pacman(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.death = false;\r
+       this.index = -1;\r
+       this.tx = this.ty = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int x, int y) {\r
+       this.tx = x;\r
+       this.ty = y;\r
+    }\r
+    \r
+    public void tryMove() {\r
+       // decide dx & dy\r
+       \r
+       // Don't let the pacman go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.tx;\r
+       //System.printString("aaa\n");\r
+       int targety = this.ty;\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       getDestination (this.direction, targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       //System.printString("dx: " + this.dx + ", dy: " + this.dy + "\n");\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Nor/Ghost.java b/Robust/src/Benchmarks/MMG/Nor/Ghost.java
new file mode 100755 (executable)
index 0000000..31a85d4
--- /dev/null
@@ -0,0 +1,327 @@
+public class Ghost {\r
+    flag move;\r
+    flag update;\r
+\r
+    public int x;\r
+    public int y;\r
+    public int index;\r
+    public int target;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Ghost(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.index = -1;\r
+       this.target = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int pacman) {\r
+       this.target = pacman;\r
+    }\r
+    \r
+    // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    public void tryMove() {\r
+       //System.printString("step 1\n");\r
+       //System.printString("target: " + this.target + "\n");\r
+       \r
+       // Don't let the ghost go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.map.pacMenX[this.target];\r
+       //System.printString("aaa\n");\r
+       int targety = this.map.pacMenY[this.target];\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       if(targetx == -1) {\r
+           //System.printString("a\n");\r
+           // already kicked off, choose another target\r
+           int i = 0;\r
+           boolean found = false;\r
+           while((!found) && (i < map.pacMenX.length)) {\r
+               if(this.map.pacMenX[i] != -1) {\r
+                   this.target = i;\r
+                   targetx = this.map.pacMenX[i];\r
+                   targety = this.map.pacMenY[i];\r
+                   this.map.targets[i] = this.target;\r
+                   found = true;\r
+               }\r
+               i++;\r
+           }\r
+           //System.printString("b\n");\r
+           if(i == this.map.pacMenX.length) {\r
+               //System.printString("c\n");\r
+               // no more pacmen to chase\r
+               this.dx = 0;\r
+               this.dy = 0;\r
+               this.direction = 0;\r
+               return;\r
+           }\r
+           //System.printString("d\n");\r
+       }\r
+       getDestination (this.map.directions[this.target], targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}\r
diff --git a/Robust/src/Benchmarks/MMG/Nor/MMG.java b/Robust/src/Benchmarks/MMG/Nor/MMG.java
new file mode 100755 (executable)
index 0000000..93dca6f
--- /dev/null
@@ -0,0 +1,147 @@
+task startup(StartupObject s{initialstate}) {\r
+    //System.printString("Task startup\n");\r
+    \r
+    int nrofpacs = 4;\r
+    int nrofghosts = 8;\r
+    Map map = new Map(nrofpacs, nrofghosts){init};\r
+    taskexit(s{!initialstate});\r
+}\r
+\r
+task initMap(Map map{init}) {\r
+    //System.printString("Task initMap\n");\r
+    \r
+    map.init();\r
+    \r
+    int i = 0;\r
+    // create ghosts\r
+    for(i = 0; i < map.nrofghosts; i++) {\r
+       Ghost ghost = new Ghost(7, 7, map){move};\r
+       ghost.setTarget(i%map.nrofpacs);\r
+       ghost.index = i;\r
+       map.placeGhost(ghost);\r
+       map.targets[i] = ghost.target;\r
+    }\r
+    // create pacmen\r
+    int tx = 14;\r
+    int ty = 14;\r
+    for(i = 0; i < map.nrofpacs; i++) {\r
+         Pacman pacman = new Pacman(5, 7, map){move};\r
+         pacman.setTarget(tx*(i/2), ty*(i%2));\r
+         pacman.index = i;\r
+         map.placePacman(pacman);\r
+         map.desX[i] = tx*(i/2);\r
+         map.desY[i] = ty*(i%2);\r
+    }\r
+    \r
+    map.ghostcount = 0;\r
+    map.paccount = 0;\r
+    \r
+    taskexit(map{!init, updateGhost});\r
+}\r
+\r
+task moveGhost(Ghost g{move}) {\r
+    //System.printString("Task moveGhost\n");\r
+    \r
+    g.tryMove();\r
+    \r
+    taskexit(g{!move, update});\r
+}\r
+\r
+task movePacman(Pacman p{move}) {\r
+    //System.printString("Task movePacman\n");\r
+    \r
+    p.tryMove();\r
+    \r
+    taskexit(p{!move, update});\r
+}\r
+\r
+task updateGhost(Map map{updateGhost}, /*optional*/ Ghost g{update}) {\r
+    //System.printString("Task updateGhost\n");\r
+    \r
+    //if(isavailable(g)) {\r
+       g.doMove();\r
+       map.placeGhost(g);\r
+       map.ghostdirections[g.index] = g.direction;\r
+    /*} else {\r
+       System.printString("FAILURE ghost!!!\n");\r
+       //map.failghostcount++;\r
+       map.ghostcount++;\r
+    }*/\r
+    \r
+    if(map.ghostcount == map.nrofghosts) {\r
+       //map.nrofghosts -= map.failghostcount;\r
+       map.ghostcount = 0;\r
+       map.failghostcount = 0;\r
+       /*for(int i = 0; i < map.ghostsX.length; i++) {\r
+           System.printString("(" + map.ghostsX[i] + "," + map.ghostsY[i] + ") ");\r
+       }\r
+       System.printString("\n");*/\r
+       taskexit(map{updatePac, !updateGhost}, g{!update});\r
+    }\r
+    taskexit(g{!update});\r
+}\r
+\r
+task updatePac(Map map{updatePac}, /*optional*/ Pacman p{update}) {\r
+    //System.printString("Task updatePac\n");\r
+    \r
+    //if(isavailable(p)) {\r
+       p.doMove();\r
+       map.placePacman(p);\r
+       map.directions[p.index] = p.direction;\r
+       //System.printString("Pacman " + p.index + ": (" + map.pacMenX[p.index] + "," + map.pacMenY[p.index] + ")\n");\r
+       boolean death = map.check(p);\r
+       /*if(death) {\r
+           System.printString("Pacman " + p.index + " caught!\n");\r
+       }*/\r
+    /*} else {\r
+       System.printString("FAILURE pacman!!!\n");\r
+       map.deathcount++;\r
+       map.paccount++;\r
+    }*/\r
+    \r
+    boolean finish = map.paccount == map.nrofpacs;\r
+    \r
+    if(finish) {\r
+       map.nrofpacs -= map.deathcount;\r
+       //System.printString(map.nrofpacs + " pacmen left. \n");\r
+       if(map.isfinish()) {\r
+           taskexit(map{finish, !updatePac}, p{!update, !move});\r
+       } else {\r
+           taskexit(map{next, !updatePac}, p{!update, !move});\r
+       }\r
+    } else {\r
+       taskexit(p{!move, !update});\r
+    }\r
+}\r
+\r
+task next(Map map{next}) {\r
+    //System.printString("Task next\n");\r
+    \r
+    int i = 0;\r
+    for(i = 0; i < map.nrofghosts; i++) {\r
+       Ghost ghost = new Ghost(map.ghostsX[i], map.ghostsY[i], map){move};\r
+       ghost.setTarget(map.targets[i]);\r
+       ghost.index = i;\r
+       ghost.direction = map.ghostdirections[i];\r
+    }\r
+    for(i = 0; i < map.pacMenX.length; i++) {\r
+       if(map.pacMenX[i] != -1) {\r
+           // still in the map\r
+           //System.printString("new Pacman\n");\r
+           Pacman pacman = new Pacman(map.pacMenX[i], map.pacMenY[i], map){move};\r
+           pacman.setTarget(map.desX[i], map.desY[i]);\r
+           pacman.index = i;\r
+           pacman.direction = map.directions[i];\r
+       }\r
+    }\r
+    \r
+    map.paccount = 0;\r
+    map.deathcount = 0;\r
+    \r
+    taskexit(map{!next, updateGhost});\r
+}\r
+\r
+task finish(Map map{finish}) {\r
+    System.printString("Task Finish\n");\r
+    taskexit(map{!finish});\r
+}\r
diff --git a/Robust/src/Benchmarks/MMG/Nor/Map.java b/Robust/src/Benchmarks/MMG/Nor/Map.java
new file mode 100755 (executable)
index 0000000..1a861b6
--- /dev/null
@@ -0,0 +1,129 @@
+public class Map {\r
+    flag init;\r
+    flag updateGhost;\r
+    flag updatePac;\r
+    flag next;\r
+    flag finish;\r
+    \r
+    public int[] map;\r
+    public int[] pacMenX;\r
+    public int[] pacMenY;\r
+    public int[] directions;\r
+    public int[] ghostsX;\r
+    public int[] ghostsY;\r
+    public int[] ghostdirections;\r
+    public int[] targets;\r
+    public int[] desX;\r
+    public int[] desY;\r
+    \r
+    public int nrofghosts;\r
+    public int nrofpacs;\r
+    private int nrofblocks;\r
+    //public boolean toupdate;\r
+    public int ghostcount;\r
+    public int paccount;\r
+    public int deathcount;\r
+    public int failghostcount;\r
+    \r
+    public Random r;\r
+    \r
+    public Map(int nrofpacs, int nrofghosts) {\r
+       //System.printString("step 1\n");\r
+       this.nrofblocks = 15;\r
+       this.map = new int[this.nrofblocks*this.nrofblocks];\r
+       this.nrofpacs = nrofpacs;\r
+       this.nrofghosts = nrofghosts;\r
+       this.pacMenX = new int[this.nrofpacs];\r
+       this.pacMenY = new int[this.nrofpacs];\r
+       this.directions = new int[this.nrofpacs];\r
+       this.ghostsX = new int[this.nrofghosts];\r
+       this.ghostsY = new int[this.nrofghosts];\r
+       this.ghostdirections = new int[this.nrofghosts];\r
+       this.targets = new int[this.nrofghosts];\r
+       this.desX = new int[this.nrofpacs];\r
+       this.desY = new int[this.nrofpacs];\r
+       //this.toupdate = false;\r
+       this.ghostcount = 0;\r
+       this.paccount = 0;\r
+       this.deathcount = 0;\r
+       this.failghostcount = 0;\r
+       \r
+       this.r = new Random();\r
+       \r
+       //System.printString("step 2\n");\r
+       for(int i = 0; i < this.nrofpacs; i++) {\r
+           this.pacMenX[i] = this.pacMenY[i] = -1;\r
+           this.desX[i] = this.desY[i] = -1;\r
+       }\r
+       //System.printString("step 3\n");\r
+       for(int i = 0; i < this.nrofghosts; i++) {\r
+           this.ghostsX[i] = this.ghostsY[i] = -1;\r
+           this.targets[i] = -1;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    public void init() {\r
+       int i = 0;\r
+       this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=15;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=6;this.map[i++]=1;this.map[i++]=10;this.map[i++]=4;this.map[i++]=3;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=6;this.map[i++]=5;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=5;this.map[i++]=3;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=12;this.map[i++]=5;this.map[i++]=9;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=12;\r
+       this.map[i++]=6;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=3;\r
+       this.map[i++]=4;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=10;this.map[i++]=10;this.map[i++]=10;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=1;\r
+       this.map[i++]=12;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=10;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=9;\r
+       this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=2;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=8;this.map[i++]=4;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=1;this.map[i++]=8;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=2;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;this.map[i++]=13;this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12; // 15*15    \r
+    } \r
+\r
+    public void placePacman(Pacman t) {\r
+       this.pacMenX[t.index] = t.x;\r
+       this.pacMenY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 16;\r
+       this.paccount++;\r
+    }\r
+    \r
+    public void placeGhost(Ghost t) {\r
+       this.ghostsX[t.index] = t.x;\r
+       this.ghostsY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 32;\r
+       this.ghostcount++;\r
+    }\r
+    \r
+    public boolean check(Pacman t) {\r
+       boolean death = false;\r
+       int i = 0;\r
+       while((!death) && (i < this.nrofghosts)) {\r
+           if((t.x == this.ghostsX[i]) && (t.y == this.ghostsY[i])) {\r
+               death = true;\r
+           }\r
+           i++;\r
+       }\r
+       if((!death) && (t.x == t.tx) && (t.y == t.ty)) {\r
+           // reach the destination\r
+           //System.printString("Hit destination!\n");\r
+           death = true;\r
+       }\r
+       if(death) {\r
+           // pacman caught by ghost\r
+           // set pacman as death\r
+           t.death = true;\r
+           // kick it out\r
+           //this.map[t.y * this.nrofblocks + t.x - 1] -= 16;\r
+           this.deathcount++;\r
+           this.pacMenX[t.index] = -1;\r
+           this.pacMenY[t.index] = -1;\r
+       }\r
+       return death;\r
+    }\r
+    \r
+    public boolean isfinish() {\r
+       return nrofpacs == 0;\r
+    }\r
+}\r
diff --git a/Robust/src/Benchmarks/MMG/Nor/Pacman.java b/Robust/src/Benchmarks/MMG/Nor/Pacman.java
new file mode 100755 (executable)
index 0000000..3482a5e
--- /dev/null
@@ -0,0 +1,304 @@
+public class Pacman {\r
+    flag move;\r
+    flag update;\r
+\r
+    public int x;\r
+    public int y;\r
+    public boolean death;\r
+    public int index;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    public int tx;\r
+    public int ty;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Pacman(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.death = false;\r
+       this.index = -1;\r
+       this.tx = this.ty = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int x, int y) {\r
+       this.tx = x;\r
+       this.ty = y;\r
+    }\r
+    \r
+    public void tryMove() {\r
+       // decide dx & dy\r
+\r
+       // Don't let the pacman go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.tx;\r
+       //System.printString("aaa\n");\r
+       int targety = this.ty;\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       getDestination (this.direction, targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       // System.printString("dx: " + this.dx + ", dy: " + this.dy + "\n");\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}\r
diff --git a/Robust/src/Benchmarks/MMG/Tag/Ghost.java b/Robust/src/Benchmarks/MMG/Tag/Ghost.java
new file mode 100755 (executable)
index 0000000..da511d0
--- /dev/null
@@ -0,0 +1,327 @@
+public class Ghost {\r
+    flag move;\r
+    flag update;\r
+\r
+    public int x;\r
+    public int y;\r
+    public int index;\r
+    public int target;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Ghost(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.index = -1;\r
+       this.target = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int pacman) {\r
+       this.target = pacman;\r
+    }\r
+    \r
+    // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    public void tryMove() {\r
+       //System.printString("step 1\n");\r
+       //System.printString("target: " + this.target + "\n");\r
+       \r
+       // Don't let the ghost go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.map.pacMenX[this.target];\r
+       //System.printString("aaa\n");\r
+       int targety = this.map.pacMenY[this.target];\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       if(targetx == -1) {\r
+           //System.printString("a\n");\r
+           // already kicked off, choose another target\r
+           int i = 0;\r
+           boolean found = false;\r
+           while((!found) && (i < map.pacMenX.length)) {\r
+               if(this.map.pacMenX[i] != -1) {\r
+                   this.target = i;\r
+                   targetx = this.map.pacMenX[i];\r
+                   targety = this.map.pacMenY[i];\r
+                   this.map.targets[i] = this.target;\r
+                   found = true;\r
+               }\r
+               i++;\r
+           }\r
+           //System.printString("b\n");\r
+           if(i == this.map.pacMenX.length) {\r
+               //System.printString("c\n");\r
+               // no more pacmen to chase\r
+               this.dx = 0;\r
+               this.dy = 0;\r
+               this.direction = 0;\r
+               return;\r
+           }\r
+           //System.printString("d\n");\r
+       }\r
+       getDestination (this.map.directions[this.target], targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Tag/MMG.java b/Robust/src/Benchmarks/MMG/Tag/MMG.java
new file mode 100755 (executable)
index 0000000..4be7468
--- /dev/null
@@ -0,0 +1,147 @@
+task startup(StartupObject s{initialstate}) {\r
+    //System.printString("Task startup\n");\r
+    \r
+    int nrofpacs = 4;\r
+    int nrofghosts = 8;\r
+    Map map = new Map(nrofpacs, nrofghosts){init};\r
+    taskexit(s{!initialstate});\r
+}\r
+\r
+task initMap(Map map{init}) {\r
+    //System.printString("Task initMap\n");\r
+    \r
+    map.init();\r
+    \r
+    int i = 0;\r
+    // create ghosts\r
+    for(i = 0; i < map.nrofghosts; i++) {\r
+       Ghost ghost = new Ghost(7, 7, map){move};\r
+       ghost.setTarget(i%map.nrofpacs);\r
+       ghost.index = i;\r
+       map.placeGhost(ghost);\r
+       map.targets[i] = ghost.target;\r
+    }\r
+    // create pacmen\r
+    int tx = 14;\r
+    int ty = 14;\r
+    for(i = 0; i < map.nrofpacs; i++) {\r
+         Pacman pacman = new Pacman(5, 7, map){move};\r
+         pacman.setTarget(tx*(i/2), ty*(i%2));\r
+         pacman.index = i;\r
+         map.placePacman(pacman);\r
+         map.desX[i] = tx*(i/2);\r
+         map.desY[i] = ty*(i%2);\r
+    }\r
+    \r
+    map.ghostcount = 0;\r
+    map.paccount = 0;\r
+    \r
+    taskexit(map{!init, updateGhost});\r
+}\r
+\r
+task moveGhost(Ghost g{move}) {\r
+    //System.printString("Task moveGhost\n");\r
+    \r
+    g.tryMove();\r
+    \r
+    taskexit(g{!move, update});\r
+}\r
+\r
+task movePacman(Pacman p{move}) {\r
+    //System.printString("Task movePacman\n");\r
+    \r
+    p.tryMove();\r
+    \r
+    taskexit(p{!move, update});\r
+}\r
+\r
+task updateGhost(Map map{updateGhost}, optional Ghost g{update}) {\r
+    //System.printString("Task updateGhost\n");\r
+    \r
+    if(isavailable(g)) {\r
+       g.doMove();\r
+       map.placeGhost(g);\r
+       map.ghostdirections[g.index] = g.direction;\r
+    } else {\r
+       //System.printString("FAILURE ghost!!!\n");\r
+       //map.failghostcount++;\r
+       map.ghostcount++;\r
+    }\r
+    \r
+    if(map.ghostcount == map.nrofghosts) {\r
+       //map.nrofghosts -= map.failghostcount;\r
+       map.ghostcount = 0;\r
+       map.failghostcount = 0;\r
+       /*for(int i = 0; i < map.ghostsX.length; i++) {\r
+           System.printString("(" + map.ghostsX[i] + "," + map.ghostsY[i] + ") ");\r
+       }\r
+       System.printString("\n");*/\r
+       taskexit(map{updatePac, !updateGhost}, g{!update});\r
+    }\r
+    taskexit(g{!update});\r
+}\r
+\r
+task updatePac(Map map{updatePac}, optional Pacman p{update}) {\r
+    //System.printString("Task updatePac\n");\r
+    \r
+    if(isavailable(p)) {\r
+       p.doMove();\r
+       map.placePacman(p);\r
+       map.directions[p.index] = p.direction;\r
+       //System.printString("Pacman " + p.index + ": (" + map.pacMenX[p.index] + "," + map.pacMenY[p.index] + ")\n");\r
+       boolean death = map.check(p);\r
+       /*if(death) {\r
+           System.printString("Pacman " + p.index + " caught!\n");\r
+       }*/\r
+    } else {\r
+       //System.printString("FAILURE pacman!!!\n");\r
+       map.deathcount++;\r
+       map.paccount++;\r
+    }\r
+    \r
+    boolean finish = map.paccount == map.nrofpacs;\r
+    \r
+    if(finish) {\r
+       map.nrofpacs -= map.deathcount;\r
+       //System.printString(map.nrofpacs + " pacmen left. \n");\r
+       if(map.isfinish()) {\r
+           taskexit(map{finish, !updatePac}, p{!update, !move});\r
+       } else {\r
+           taskexit(map{next, !updatePac}, p{!update, !move});\r
+       }\r
+    } else {\r
+       taskexit(p{!move, !update});\r
+    }\r
+}\r
+\r
+task next(Map map{next}) {\r
+    //System.printString("Task next\n");\r
+    \r
+    int i = 0;\r
+    for(i = 0; i < map.nrofghosts; i++) {\r
+       Ghost ghost = new Ghost(map.ghostsX[i], map.ghostsY[i], map){move};\r
+       ghost.setTarget(map.targets[i]);\r
+       ghost.index = i;\r
+       ghost.direction = map.ghostdirections[i];\r
+    }\r
+    for(i = 0; i < map.pacMenX.length; i++) {\r
+       if(map.pacMenX[i] != -1) {\r
+           // still in the map\r
+           //System.printString("new Pacman\n");\r
+           Pacman pacman = new Pacman(map.pacMenX[i], map.pacMenY[i], map){move};\r
+           pacman.setTarget(map.desX[i], map.desY[i]);\r
+           pacman.index = i;\r
+           pacman.direction = map.directions[i];\r
+       }\r
+    }\r
+    \r
+    map.paccount = 0;\r
+    map.deathcount = 0;\r
+    \r
+    taskexit(map{!next, updateGhost});\r
+}\r
+\r
+task finish(Map map{finish}) {\r
+    System.printString("Task Finish\n");\r
+    taskexit(map{!finish});\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Tag/Map.java b/Robust/src/Benchmarks/MMG/Tag/Map.java
new file mode 100755 (executable)
index 0000000..906acdb
--- /dev/null
@@ -0,0 +1,129 @@
+public class Map {\r
+    flag init;\r
+    flag updateGhost;\r
+    flag updatePac;\r
+    flag next;\r
+    flag finish;\r
+    \r
+    public int[] map;\r
+    public int[] pacMenX;\r
+    public int[] pacMenY;\r
+    public int[] directions;\r
+    public int[] ghostsX;\r
+    public int[] ghostsY;\r
+    public int[] ghostdirections;\r
+    public int[] targets;\r
+    public int[] desX;\r
+    public int[] desY;\r
+    \r
+    public int nrofghosts;\r
+    public int nrofpacs;\r
+    private int nrofblocks;\r
+    //public boolean toupdate;\r
+    public int ghostcount;\r
+    public int paccount;\r
+    public int deathcount;\r
+    public int failghostcount;\r
+    \r
+    public Random r;\r
+    \r
+    public Map(int nrofpacs, int nrofghosts) {\r
+       //System.printString("step 1\n");\r
+       this.nrofblocks = 15;\r
+       this.map = new int[this.nrofblocks*this.nrofblocks];\r
+       this.nrofpacs = nrofpacs;\r
+       this.nrofghosts = nrofghosts;\r
+       this.pacMenX = new int[this.nrofpacs];\r
+       this.pacMenY = new int[this.nrofpacs];\r
+       this.directions = new int[this.nrofpacs];\r
+       this.ghostsX = new int[this.nrofghosts];\r
+       this.ghostsY = new int[this.nrofghosts];\r
+       this.ghostdirections = new int[this.nrofghosts];\r
+       this.targets = new int[this.nrofghosts];\r
+       this.desX = new int[this.nrofpacs];\r
+       this.desY = new int[this.nrofpacs];\r
+       //this.toupdate = false;\r
+       this.ghostcount = 0;\r
+       this.paccount = 0;\r
+       this.deathcount = 0;\r
+       this.failghostcount = 0;\r
+       \r
+       this.r = new Random();\r
+       \r
+       //System.printString("step 2\n");\r
+       for(int i = 0; i < this.nrofpacs; i++) {\r
+           this.pacMenX[i] = this.pacMenY[i] = -1;\r
+           this.desX[i] = this.desY[i] = -1;\r
+       }\r
+       //System.printString("step 3\n");\r
+       for(int i = 0; i < this.nrofghosts; i++) {\r
+           this.ghostsX[i] = this.ghostsY[i] = -1;\r
+           this.targets[i] = -1;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    public void init() {\r
+       int i = 0;\r
+       this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=6;this.map[i++]=9;this.map[i++]=12;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=15;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=6;this.map[i++]=1;this.map[i++]=10;this.map[i++]=4;this.map[i++]=3;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=6;this.map[i++]=5;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=5;this.map[i++]=3;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=12;this.map[i++]=5;this.map[i++]=9;this.map[i++]=2;this.map[i++]=8;this.map[i++]=2;this.map[i++]=10;this.map[i++]=2;this.map[i++]=12;\r
+       this.map[i++]=6;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=11;this.map[i++]=8;this.map[i++]=14;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=7;this.map[i++]=5;this.map[i++]=3;\r
+       this.map[i++]=4;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=10;this.map[i++]=10;this.map[i++]=10;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=5;this.map[i++]=1;\r
+       this.map[i++]=12;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=10;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=13;this.map[i++]=5;this.map[i++]=9;\r
+       this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=2;this.map[i++]=10;this.map[i++]=0;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;\r
+       this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=15;this.map[i++]=5;this.map[i++]=3;this.map[i++]=2;this.map[i++]=2;this.map[i++]=6;this.map[i++]=5;\r
+       this.map[i++]=5;this.map[i++]=9;this.map[i++]=8;this.map[i++]=8;this.map[i++]=4;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=1;this.map[i++]=8;this.map[i++]=8;this.map[i++]=12;this.map[i++]=5;\r
+       this.map[i++]=1;this.map[i++]=10;this.map[i++]=10;this.map[i++]=6;this.map[i++]=13;this.map[i++]=5;this.map[i++]=11;this.map[i++]=2;this.map[i++]=14;this.map[i++]=5;this.map[i++]=13;this.map[i++]=3;this.map[i++]=10;this.map[i++]=10;this.map[i++]=4;\r
+       this.map[i++]=5;this.map[i++]=11;this.map[i++]=14;this.map[i++]=1;this.map[i++]=10;this.map[i++]=8;this.map[i++]=6;this.map[i++]=13;this.map[i++]=3;this.map[i++]=8;this.map[i++]=10;this.map[i++]=4;this.map[i++]=11;this.map[i++]=14;this.map[i++]=5;\r
+       this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=12;this.map[i++]=3;this.map[i++]=6;this.map[i++]=9;this.map[i++]=10;this.map[i++]=10;this.map[i++]=12; // 15*15    \r
+    } \r
+\r
+    public void placePacman(Pacman t) {\r
+       this.pacMenX[t.index] = t.x;\r
+       this.pacMenY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 16;\r
+       this.paccount++;\r
+    }\r
+    \r
+    public void placeGhost(Ghost t) {\r
+       this.ghostsX[t.index] = t.x;\r
+       this.ghostsY[t.index] = t.y;\r
+       //this.map[t.y * this.nrofblocks + t.x - 1] |= 32;\r
+       this.ghostcount++;\r
+    }\r
+    \r
+    public boolean check(Pacman t) {\r
+       boolean death = false;\r
+       int i = 0;\r
+       while((!death) && (i < this.nrofghosts)) {\r
+           if((t.x == this.ghostsX[i]) && (t.y == this.ghostsY[i])) {\r
+               death = true;\r
+           }\r
+           i++;\r
+       }\r
+       if((!death) && (t.x == t.tx) && (t.y == t.ty)) {\r
+           // reach the destination\r
+           //System.printString("Hit destination!\n");\r
+           death = true;\r
+       }\r
+       if(death) {\r
+           // pacman caught by ghost\r
+           // set pacman as death\r
+           t.death = true;\r
+           // kick it out\r
+           //this.map[t.y * this.nrofblocks + t.x - 1] -= 16;\r
+           this.deathcount++;\r
+           this.pacMenX[t.index] = -1;\r
+           this.pacMenY[t.index] = -1;\r
+       }\r
+       return death;\r
+    }\r
+    \r
+    public boolean isfinish() {\r
+       return nrofpacs == 0;\r
+    }\r
+}
\ No newline at end of file
diff --git a/Robust/src/Benchmarks/MMG/Tag/Pacman.java b/Robust/src/Benchmarks/MMG/Tag/Pacman.java
new file mode 100755 (executable)
index 0000000..48693a2
--- /dev/null
@@ -0,0 +1,304 @@
+public class Pacman {\r
+    flag move;\r
+    flag update;\r
+\r
+    public int x;\r
+    public int y;\r
+    public boolean death;\r
+    public int index;\r
+    public int direction;  // 0:still, 1:up, 2:down, 3:left, 4:right\r
+    int dx;\r
+    int dy;\r
+    public int tx;\r
+    public int ty;\r
+    int destinationX;\r
+    int destinationY;\r
+    Map map;\r
+    \r
+    public Pacman(int x, int y, Map map) {\r
+       this.x = x;\r
+       this.y = y;\r
+       this.dx = this.dy = 0;\r
+       this.death = false;\r
+       this.index = -1;\r
+       this.tx = this.ty = -1;\r
+       this.direction = 0;\r
+       this.destinationX = -1;\r
+       this.destinationY = -1;\r
+       this.map = map;\r
+    }\r
+    \r
+    public void setTarget(int x, int y) {\r
+       this.tx = x;\r
+       this.ty = y;\r
+    }\r
+    \r
+    public void tryMove() {\r
+       // decide dx & dy\r
+\r
+       // Don't let the pacman go back the way it came.\r
+       int prevDirection = 0;\r
+\r
+       // If there is a destination, then check if the destination has been reached.\r
+       if (destinationX >= 0 && destinationY >= 0) {\r
+           // Check if the destination has been reached, if so, then\r
+           // get new destination.\r
+           if (destinationX == x && destinationY == y) {\r
+               destinationX = -1;\r
+               destinationY = -1;\r
+               prevDirection = direction;\r
+           } else {\r
+               // Otherwise, we haven't reached the destionation so\r
+               // continue in same direction.\r
+               return;\r
+           }\r
+       }\r
+       setNextDirection (prevDirection);\r
+    }\r
+    \r
+    private void setNextDirection(int prevDirection) {\r
+       // get target's position\r
+       int targetx = this.tx;\r
+       //System.printString("aaa\n");\r
+       int targety = this.ty;\r
+       int[] nextLocation = new int[2];\r
+       nextLocation[0] = nextLocation[1] = -1;\r
+       \r
+       //System.printString("bbb\n");\r
+       getDestination (this.direction, targetx, targety, nextLocation);\r
+       targetx = nextLocation[0];\r
+       targety = nextLocation[1];\r
+       \r
+       //System.printString("step 2\n");\r
+       // check the distance\r
+       int deltax = this.x - targetx; // <0: move right; >0: move left\r
+       int deltay = this.y - targety; // <0: move down; >0: move up\r
+       // decide the priority of four moving directions\r
+       int[] bestDirection = new int[4];\r
+       //System.printString("dx: " + deltax + "; dy: " + deltay + "\n");\r
+       if((Math.abs(deltax) > Math.abs(deltay)) && (deltay != 0)) {\r
+           // go first along y\r
+           if(deltay > 0) {\r
+               bestDirection[0] = 1;\r
+               bestDirection[3] = 2;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 2;\r
+               bestDirection[3] = 1;\r
+               if(deltax > 0) {\r
+                   bestDirection[1] = 3;\r
+                   bestDirection[2] = 4;\r
+               } else {\r
+                   bestDirection[1] = 4;\r
+                   bestDirection[2] = 3;\r
+               }\r
+           }\r
+       } else {\r
+           if(deltax > 0) {\r
+               bestDirection[0] = 3;\r
+               bestDirection[3] = 4;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           } else {\r
+               bestDirection[0] = 4;\r
+               bestDirection[3] = 3;\r
+               if(deltay > 0) {\r
+                   bestDirection[1] = 1;\r
+                   bestDirection[2] = 2;\r
+               } else {\r
+                   bestDirection[1] = 2;\r
+                   bestDirection[2] = 1;\r
+               }\r
+           }\r
+       }\r
+       /*for(int i = 0; i < 4; i++) {\r
+           System.printString(bestDirection[i] + ",");\r
+       }\r
+       System.printString("\n");*/\r
+       \r
+       // There's a 50% chance that the ghost will try the sub-optimal direction first.\r
+       // This will keep the ghosts from following each other and to trap Pacman.\r
+       if (this.map.r.nextDouble() < .50) {  \r
+           int temp = bestDirection[0];\r
+           bestDirection[0] = bestDirection[1];\r
+           bestDirection[1] = temp;\r
+       }\r
+             \r
+       //System.printString("step 3\n");\r
+       // try to move one by one\r
+       int i = 0;\r
+       boolean set = false;\r
+       this.dx = 0;\r
+       this.dy = 0;\r
+       while((!set) && (i < 4)) {\r
+           if(bestDirection[i] == 1) {\r
+               // try to move up\r
+               if((prevDirection != 2) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 2) == 0)) {\r
+                   //System.printString("a\n");\r
+                   if (getDestination (1, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = -1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 2) {\r
+               // try to move down\r
+               if((prevDirection != 1) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 8) == 0)) {\r
+                   //System.printString("b\n");\r
+                   if (getDestination (2, this.x, this.y, nextLocation)) {\r
+                       this.dx = 0;\r
+                       this.dy = 1;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 3) {\r
+               // try to move left\r
+               if((prevDirection != 4) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 1) == 0)) {\r
+                   //System.printString("c\n");\r
+                   if (getDestination (3, this.x, this.y, nextLocation)) {\r
+                       this.dx = -1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           } else if (bestDirection[i] == 4) {\r
+               // try to move right\r
+               if((prevDirection != 3) && ((int)(this.map.map[y * this.map.nrofblocks + x] & 4) == 0)) {\r
+                   //System.printString("d\n");\r
+                   if (getDestination (4, this.x, this.y, nextLocation)) {\r
+                       this.dx = 1;\r
+                       this.dy = 0;\r
+                       set = true;\r
+                   }\r
+               }\r
+           }\r
+           i++;\r
+       }\r
+       //System.printString("step 4\n");\r
+    }\r
+    \r
+    // This method will take the specified location and direction and determine\r
+    // for the given location if the thing moved in that direction, what the\r
+    // next possible turning location would be.\r
+    boolean getDestination (int direction, int locX, int locY, int[] point) {\r
+       // If the request direction is blocked by a wall, then just return the current location\r
+       if ((direction == 1 && (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0) || // up\r
+           (direction == 3 && (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) ||  // left\r
+           (direction == 2 && (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0) || // down\r
+           (direction == 4 && (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0)) { // right \r
+          point[0] = locX;\r
+          point[1] = locY;\r
+          return false;\r
+       }\r
+          \r
+       // Start off by advancing one in direction for specified location\r
+       if (direction == 1) {\r
+          // up\r
+          locY--;\r
+       } else if (direction == 2) {\r
+          // down\r
+          locY++;\r
+       } else if (direction == 3) {\r
+          // left\r
+          locX--;\r
+       } else if (direction == 4) {\r
+          // right\r
+          locX++;\r
+       }\r
+       \r
+       // If we violate the grid boundary,\r
+       // then return false.\r
+       if (locY < 0 ||\r
+           locX < 0 ||\r
+           locY == this.map.nrofblocks ||\r
+           locX == this.map.nrofblocks) {\r
+          return false;\r
+       }\r
+       \r
+       boolean set = false;\r
+       // Determine next turning location..\r
+       while (!set) {\r
+          if (direction == 1 || direction == 2) { \r
+              // up or down\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 4) == 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) == 0 || // left\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 2) != 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) != 0)  { // down\r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+               } else {\r
+                  if (direction == 1) {\r
+                      // Check for Top Warp\r
+                      if (locY == 0) {\r
+                          point[0] = locX;\r
+                          point[1] = this.map.nrofblocks - 1;\r
+                          set = true;\r
+                      } else {\r
+                          locY--;\r
+                      }\r
+                  } else {\r
+                      // Check for Bottom Warp\r
+                      if (locY == this.map.nrofblocks - 1) {\r
+                          point[0] = locX;\r
+                          point[1] = 0;\r
+                          set = true;\r
+                      } else {\r
+                          locY++;\r
+                      }\r
+                  }\r
+               }\r
+          } else {\r
+              // left or right\r
+              if ((this.map.map[locX + locY * this.map.nrofblocks] & 2) == 0 || // up\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 8) == 0 || // down\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 4) != 0 || // right\r
+                     (this.map.map[locX + locY * this.map.nrofblocks] & 1) != 0) { // left  \r
+                 point[0] = locX;\r
+                 point[1] = locY;\r
+                 set = true;\r
+              } else {\r
+                 if (direction == 3) {\r
+                     // Check for Left Warp\r
+                     if (locX == 0) {\r
+                         point[0] = this.map.nrofblocks - 1;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX--;\r
+                     }\r
+                 } else {\r
+                     // Check for Right Warp\r
+                     if (locX == this.map.nrofblocks - 1) {\r
+                         point[0] = 0;\r
+                         point[1] = locY;\r
+                         set = true;\r
+                     } else {\r
+                         locX++;\r
+                     }\r
+                 }\r
+              }\r
+          }\r
+       }\r
+       return true;\r
+    }\r
+    \r
+    public void doMove() {\r
+       // System.printString("dx: " + this.dx + ", dy: " + this.dy + "\n");\r
+       this.x += this.dx;\r
+       this.y += this.dy;\r
+       //this.dx = 0;\r
+       //this.dy = 0;\r
+    }\r
+}
\ No newline at end of file