From 8925c05d917e9a00fd701ce2dfce61368175ed24 Mon Sep 17 00:00:00 2001
From: jzhou <jzhou>
Date: Tue, 2 Sep 2008 03:57:29 +0000
Subject: [PATCH] add new benchmark MMG for Bristlecone

---
 Robust/src/Benchmarks/MMG/Java/Ghost.java  | 324 ++++++++++++++++++++
 Robust/src/Benchmarks/MMG/Java/MMG.java    |  81 +++++
 Robust/src/Benchmarks/MMG/Java/Map.java    | 122 ++++++++
 Robust/src/Benchmarks/MMG/Java/Pacman.java | 301 +++++++++++++++++++
 Robust/src/Benchmarks/MMG/Nor/Ghost.java   | 327 +++++++++++++++++++++
 Robust/src/Benchmarks/MMG/Nor/MMG.java     | 147 +++++++++
 Robust/src/Benchmarks/MMG/Nor/Map.java     | 129 ++++++++
 Robust/src/Benchmarks/MMG/Nor/Pacman.java  | 304 +++++++++++++++++++
 Robust/src/Benchmarks/MMG/Tag/Ghost.java   | 327 +++++++++++++++++++++
 Robust/src/Benchmarks/MMG/Tag/MMG.java     | 147 +++++++++
 Robust/src/Benchmarks/MMG/Tag/Map.java     | 129 ++++++++
 Robust/src/Benchmarks/MMG/Tag/Pacman.java  | 304 +++++++++++++++++++
 12 files changed, 2642 insertions(+)
 create mode 100755 Robust/src/Benchmarks/MMG/Java/Ghost.java
 create mode 100755 Robust/src/Benchmarks/MMG/Java/MMG.java
 create mode 100755 Robust/src/Benchmarks/MMG/Java/Map.java
 create mode 100755 Robust/src/Benchmarks/MMG/Java/Pacman.java
 create mode 100755 Robust/src/Benchmarks/MMG/Nor/Ghost.java
 create mode 100755 Robust/src/Benchmarks/MMG/Nor/MMG.java
 create mode 100755 Robust/src/Benchmarks/MMG/Nor/Map.java
 create mode 100755 Robust/src/Benchmarks/MMG/Nor/Pacman.java
 create mode 100755 Robust/src/Benchmarks/MMG/Tag/Ghost.java
 create mode 100755 Robust/src/Benchmarks/MMG/Tag/MMG.java
 create mode 100755 Robust/src/Benchmarks/MMG/Tag/Map.java
 create mode 100755 Robust/src/Benchmarks/MMG/Tag/Pacman.java

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