Benchmark pacman.60

Download
model.prism (0.07 MB)
property.props (0.01 MB)
model.jani (1.65 MB)
Origin
Taken from QVBS (January 2026).
The given benchmark (including parameter instantiation and property) has been considered in QComp 2019 and QComp 2020.

Original Prism model and property files have been adapted for compatibility and simplicity:
- Constants: All open constants are now explicitly set within model.prism (no need to set them via command line)
- Properties: The properties only refer to labels and rewards as defined in the model.prism file. No variables or constants are used in the property.
- Formulas: some PRISM formula declarations have been renamed so that their identify does not crash with a label.
Contents of file: model.prism
// %%%%%%%%%%%%
// %..........%
// %.%.%%.%.%.%
// %.%.%%.%.%.%
// %..........%
// %%%.%.%%%%.%
// %...%......%
// %%%%%%%%%%%%

mdp

//CONSTANTS
const xSize = 11;
const ySize = 7;

const MAXSTEPS=60;

formula deactive0 = (xG0 = 0);
formula deactive1 = (xG1 = 0);

module arbiter
  pMove : [0 .. 2] init 0; //token to determine who is allowed to move
  steps : [0 .. MAXSTEPS] init 0; //number of steps we plan ahead

  [g0]  (pMove = 0) & !deactive0 & ((xG0 < xP ? xP - xG0 : xG0 - xP) + (yG0 < yP ? yP - yG0 : yG0 - yP) <= 2*(MAXSTEPS - steps)) -> 1:(pMove' = 1);
  [stop0]    (pMove = 0) & (deactive0 | ((xG0 < xP ? xP - xG0 : xG0 - xP) + (yG0 < yP ? yP - yG0 : yG0 - yP) > 2*(MAXSTEPS - steps))) -> 1:(pMove' = 1);
  [g1]  (pMove = 1) & !deactive1 & ((xG1 < xP ? xP - xG1 : xG1 - xP) + (yG1 < yP ? yP - yG1 : yG1 - yP) <= 2*(MAXSTEPS - steps)) -> 1:(pMove' = 2);
  [stop1]    (pMove = 1) & (deactive1 | ((xG1 < xP ? xP - xG1 : xG1 - xP) + (yG1 < yP ? yP - yG1 : yG1 - yP) > 2*(MAXSTEPS - steps))) -> 1:(pMove' = 2);
  

  [p]     (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1);
  [left]  (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1);
  [right] (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1);
  [up]    (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1);
  [down]  (pMove = 2 & steps < MAXSTEPS ) -> 1:(pMove' = 0) & (steps' = steps + 1);
  
  [] (pMove = 2 & (steps = MAXSTEPS | (deactive0 & deactive1))) -> 1:(pMove'=2);
endmodule


//GHOST#0
module ghost0
  xG0 : [0..xSize] init 3; // x position of Ghost
  yG0 : [0..ySize] init 4; // y position of Ghost
  dG0 : [0..3] init 0; //direction of ghost (0=right, 1=up, 2=left, 3=down)
  
  [p] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1);
  [p] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0);
  [right] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1);
  [right] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0);
  [left] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1);
  [left] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0);
  [down] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1);
  [down] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0);
  [up] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG0'=xG1) & (yG0'=yG1) & (dG0'=dG1);
  [up] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG0'=xG0);


  [stop0] true -> 1:(xG0'=0) & (yG0'=0);
    //horizontal corridor
  [g0] (yG0=1 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=1 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=1 & xG0 >=4 & xG0 <=5 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=1 & xG0 >=4 & xG0 <=5 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=1 & xG0 >=7 & xG0 <=7 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=1 & xG0 >=7 & xG0 <=7 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=1 & xG0 >=9 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=1 & xG0 >=9 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=4 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=4 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=4 & xG0 >=4 & xG0 <=4 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=4 & xG0 >=4 & xG0 <=4 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=4 & xG0 >=7 & xG0 <=7 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=4 & xG0 >=7 & xG0 <=7 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=4 & xG0 >=9 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=4 & xG0 >=9 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=6 & xG0 >=2 & xG0 <=2 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=6 & xG0 >=2 & xG0 <=2 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 
  //horizontal corridor
  [g0] (yG0=6 & xG0 >=6 & xG0 <=9 & dG0 =0) -> 1:(xG0'=xG0+1) & (dG0'=0); 
  [g0] (yG0=6 & xG0 >=6 & xG0 <=9 & dG0 =2) -> 1:(xG0'=xG0-1) & (dG0'=2); 

  //vertical corridor
  [g0] (xG0=1 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=1 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=3 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=3 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=3 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=3 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=5 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=5 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=6 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=6 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=8 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=8 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=10 & yG0 >=2 & yG0 <=3 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=10 & yG0 >=2 & yG0 <=3 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 
  //vertical corridor
  [g0] (xG0=10 & yG0 >=5 & yG0 <=5 & dG0=1) -> 1:(yG0'=yG0+1) & (dG0'=1); 
  [g0] (xG0=10 & yG0 >=5 & yG0 <=5 & dG0 =3) -> 1:(yG0'=yG0-1) & (dG0'=3); 

  //deadends
  [g0] (xG0=1 & yG0=6) -> 1: (xG0'=xG0+1) & (dG0'=0);

  //corners
  [g0] (xG0=1 & yG0=1 & (dG0=2 | dG0=1))-> 1: (yG0'=yG0+1) & (dG0'=1);
  [g0] (xG0=1 & yG0=1 & (dG0=3 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0);
  [g0] (xG0=1 & yG0=4 & (dG0=2 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3);
  [g0] (xG0=1 & yG0=4 & (dG0=1 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0);
  [g0] (xG0=3 & yG0=6 & (dG0=0 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3);
  [g0] (xG0=3 & yG0=6 & (dG0=1 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2);
  [g0] (xG0=5 & yG0=6 & (dG0=2 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3);
  [g0] (xG0=5 & yG0=6 & (dG0=1 | dG0=0)) -> 1: (xG0'=xG0+1) & (dG0'=0);
  [g0] (xG0=10 & yG0=1 & (dG0=0 | dG0=1))-> 1: (yG0'=yG0+1) & (dG0'=1);
  [g0] (xG0=10 & yG0=1 & (dG0=3 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2);
  [g0] (xG0=10 & yG0=6 & (dG0=0 | dG0=3)) -> 1: (yG0'=yG0-1) & (dG0'=3);
  [g0] (xG0=10 & yG0=6 & (dG0=1 | dG0=2)) -> 1: (xG0'=xG0-1) & (dG0'=2);


  //crossing at position (3, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g0] (xG0=3 & yG0=1 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=3 & yG0=1 & dG0=3 & xG0 0.92: (xG0'=xG0+1) & (dG0'=0) + 0.08: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=3 & yG0=1 & dG0=2 & xG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g0] (xG0=3 & yG0=1 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=3 & yG0=1 & dG0=3 & yG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=3 & yG0=1 & dG0=2 & yG0 0.8: (yG0'=yG0+1) & (dG0'=1) + 0.2: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g0] (xG0=3 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=3 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=3 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g0] (xG0=3 & yG0=1 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=3 & yG0=1 & dG0=3 & xG0 0.78: (xG0'=xG0+1) & (dG0'=0) + 0.22: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=3 & yG0=1 & dG0=2 & xG0 0.86: (yG0'=yG0+1) & (dG0'=1) + 0.14: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g0] (xG0=3 & yG0=1 & dG0=0 & xG0>xP & yG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=3 & yG0=1 & dG0=3 & xG0>xP & yG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=3 & yG0=1 & dG0=2 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g0] (xG0=3 & yG0=1 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (6, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g0] (xG0=6 & yG0=1 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=6 & yG0=1 & dG0=3 & xG0 0.64: (xG0'=xG0+1) & (dG0'=0) + 0.36: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=6 & yG0=1 & dG0=2 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g0] (xG0=6 & yG0=1 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=6 & yG0=1 & dG0=3 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=6 & yG0=1 & dG0=2 & yG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g0] (xG0=6 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=6 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=6 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 0.22: (yG0'=yG0+1) & (dG0'=1) + 0.78: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g0] (xG0=6 & yG0=1 & dG0=0 & xG0 0.46: (xG0'=xG0+1) & (dG0'=0) + 0.54: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=6 & yG0=1 & dG0=3 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=6 & yG0=1 & dG0=2 & xG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g0] (xG0=6 & yG0=1 & dG0=0 & xG0>xP & yG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=6 & yG0=1 & dG0=3 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=6 & yG0=1 & dG0=2 & xG0>xP & yG0 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.67: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g0] (xG0=6 & yG0=1 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (8, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g0] (xG0=8 & yG0=1 & dG0=0 & xG0 0.4: (xG0'=xG0+1) & (dG0'=0) + 0.6: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=8 & yG0=1 & dG0=3 & xG0 0.92: (xG0'=xG0+1) & (dG0'=0) + 0.08: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=8 & yG0=1 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g0] (xG0=8 & yG0=1 & dG0=0 & yG0 0.4: (xG0'=xG0+1) & (dG0'=0) + 0.6: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=8 & yG0=1 & dG0=3 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=8 & yG0=1 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g0] (xG0=8 & yG0=1 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=8 & yG0=1 & dG0=3 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=8 & yG0=1 & dG0=2 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g0] (xG0=8 & yG0=1 & dG0=0 & xG0 0.36: (xG0'=xG0+1) & (dG0'=0) + 0.64: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=8 & yG0=1 & dG0=3 & xG0 0.75: (xG0'=xG0+1) & (dG0'=0) + 0.25: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=8 & yG0=1 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g0] (xG0=8 & yG0=1 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=8 & yG0=1 & dG0=3 & xG0>xP & yG0 0.2: (xG0'=xG0+1) & (dG0'=0) + 0.8: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=8 & yG0=1 & dG0=2 & xG0>xP & yG0 0.67: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g0] (xG0=8 & yG0=1 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (3, 4)  [center crossing]

  //- positioning pacman = r

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0 0.61: (xG0'=xG0+1) & (dG0'=0) + 0.26: (xG0'=xG0-1) & (dG0'=2) + 0.13: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u

  [g0] (xG0=3 & yG0=4 & dG0=0 & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & yG0 0.16: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1) + 0.17: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & yG0 0.28: (yG0'=yG0+1) & (dG0'=1) + 0.43: (xG0'=xG0-1) & (dG0'=2) + 0.29: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = l

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.34: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d

  [g0] (xG0=3 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u-r

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.25: (xG0'=xG0-1) & (dG0'=2) + 0.25: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u-l

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0 0.34: (yG0'=yG0+1) & (dG0'=1) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d-r

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0yP ) -> 0.67: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d-l

  [g0] (xG0=3 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 0.34: (xG0'=xG0+1) & (dG0'=0) + 0.33: (yG0'=yG0+1) & (dG0'=1) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g0] (xG0=3 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right, up or left
  [g0] (xG0=3 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go up, left or down
  [g0] (xG0=3 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go right, left or down

  //- position pacman == position ghost

  [g0] (xG0=3 & yG0=4 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (5, 4)  [t-up crossing]
 
  //- positioning pacman = r

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0 0.89: (xG0'=xG0+1) & (dG0'=0) + 0.11: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g0] (xG0=5 & yG0=4 & dG0=0 & yG0 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & yG0 0.83: (yG0'=yG0+1) & (dG0'=1) + 0.17: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.17: (xG0'=xG0+1) & (dG0'=0) + 0.83: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.17: (yG0'=yG0+1) & (dG0'=1) + 0.83: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d

  [g0] (xG0=5 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0 0.75: (yG0'=yG0+1) & (dG0'=1) + 0.25: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d-r

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0yP ) -> 0.95: (xG0'=xG0+1) & (dG0'=0) + 0.05: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d-l

  [g0] (xG0=5 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0+1) & (dG0'=1);  // ghost is moving to the right -> continues to go right or up
  [g0] (xG0=5 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 0.11: (xG0'=xG0+1) & (dG0'=0) + 0.89: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go right or left
  [g0] (xG0=5 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g0] (xG0=5 & yG0=4 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (6, 4)  [t-down crossing]
 
  //- positioning pacman = r

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0 0.57: (xG0'=xG0+1) & (dG0'=0) + 0.43: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u

  [g0] (xG0=6 & yG0=4 & dG0=0 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = l

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.75: (xG0'=xG0-1) & (dG0'=2) + 0.25: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d

  [g0] (xG0=6 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-r

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0 0.89: (xG0'=xG0+1) & (dG0'=0) + 0.11: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-l

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0 0.67: (xG0'=xG0-1) & (dG0'=2) + 0.33: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-r

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0yP ) -> 0.69: (xG0'=xG0+1) & (dG0'=0) + 0.31: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0yP ) -> 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0yP ) -> 0.33: (xG0'=xG0-1) & (dG0'=2) + 0.67: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-l

  [g0] (xG0=6 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=6 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=6 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving left -> continues to go left or down

  //- position pacman == position ghost

  [g0] (xG0=6 & yG0=4 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (8, 4)  [t-down crossing]
 
  //- positioning pacman = r

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u

  [g0] (xG0=8 & yG0=4 & dG0=0 & yG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = l

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 0.44: (xG0'=xG0+1) & (dG0'=0) + 0.56: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0=yP ) -> 0.83: (xG0'=xG0-1) & (dG0'=2) + 0.17: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d

  [g0] (xG0=8 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.43: (xG0'=xG0+1) & (dG0'=0) + 0.57: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & yG0>yP & xG0=xP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-r

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0 1.0: (xG0'=xG0+1) & (dG0'=0);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-l

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0 0.33: (xG0'=xG0+1) & (dG0'=0) + 0.67: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0 0.83: (xG0'=xG0-1) & (dG0'=2) + 0.17: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-r

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0yP ) -> 0.56: (xG0'=xG0+1) & (dG0'=0) + 0.44: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-l

  [g0] (xG0=8 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go right or down
  [g0] (xG0=8 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0+1) & (dG0'=0) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go right or left
  [g0] (xG0=8 & yG0=4 & dG0=2 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving left -> continues to go left or down

  //- position pacman == position ghost

  [g0] (xG0=8 & yG0=4 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);

  //crossing at position (10, 4)  [t-left crossing]

  //- positioning pacman = u

  [g0] (xG0=10 & yG0=4 & dG0=0 & yG0 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go up or down
  [g0] (xG0=10 & yG0=4 & dG0=1 & yG0 0.45: (yG0'=yG0+1) & (dG0'=1) + 0.55: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go up or left
  [g0] (xG0=10 & yG0=4 & dG0=3 & yG0 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = l

  [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0=yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go up or down
  [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0=yP ) -> 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go up or left
  [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0=yP ) -> 0.79: (xG0'=xG0-1) & (dG0'=2) + 0.21: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = d

  [g0] (xG0=10 & yG0=4 & dG0=0 & yG0>yP & xG0=xP ) -> 0.2: (yG0'=yG0+1) & (dG0'=1) + 0.8: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go up or down
  [g0] (xG0=10 & yG0=4 & dG0=1 & yG0>yP & xG0=xP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go up or left
  [g0] (xG0=10 & yG0=4 & dG0=3 & yG0>yP & xG0=xP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = u-l

  [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0 0.75: (yG0'=yG0+1) & (dG0'=1) + 0.25: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go up or down
  [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0 0.44: (yG0'=yG0+1) & (dG0'=1) + 0.56: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go up or left
  [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0 1.0: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = d-l

  [g0] (xG0=10 & yG0=4 & dG0=0 & xG0>xP & yG0>yP ) -> 1.0: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving to the right -> continues to go up or down
  [g0] (xG0=10 & yG0=4 & dG0=1 & xG0>xP & yG0>yP ) -> 0.5: (yG0'=yG0+1) & (dG0'=1) + 0.5: (xG0'=xG0-1) & (dG0'=2);  // ghost is moving up -> continues to go up or left
  [g0] (xG0=10 & yG0=4 & dG0=3 & xG0>xP & yG0>yP ) -> 0.5: (xG0'=xG0-1) & (dG0'=2) + 0.5: (yG0'=yG0-1) & (dG0'=3);  // ghost is moving down -> continues to go left or down

  //- position pacman == position ghost

  [g0] (xG0=10 & yG0=4 &  xG0=xP & yG0=yP) -> 1: (xG0'=xG0);
endmodule

//GHOST#1
module ghost1
  xG1 : [0..xSize] init 3; // x position of Ghost
  yG1 : [0..ySize] init 4; // y position of Ghost
  dG1 : [0..3] init 0; //direction of ghost (0=right, 1=up, 2=left, 3=down)
  
  [p] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0);
  [p] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1);
  [right] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0);
  [right] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1);
  [left] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0);
  [left] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1);
  [down] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0);
  [down] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1);
  [up] (xG0 > xG1 | (xG0 = xG1 & yG0 > yG1)) -> 1:(xG1'=xG0) & (yG1'=yG0) & (dG1'=dG0);
  [up] (xG0 <= xG1 & (xG0 != xG1 | yG0 <= yG1)) -> 1:(xG1'=xG1);

  [stop1] true -> 1:(xG1'=0) & (yG1'=0);
  

    //horizontal corridor
  [g1] (yG1=1 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=1 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=1 & xG1 >=4 & xG1 <=5 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=1 & xG1 >=4 & xG1 <=5 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=1 & xG1 >=7 & xG1 <=7 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=1 & xG1 >=7 & xG1 <=7 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=1 & xG1 >=9 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=1 & xG1 >=9 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=4 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=4 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=4 & xG1 >=4 & xG1 <=4 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=4 & xG1 >=4 & xG1 <=4 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=4 & xG1 >=7 & xG1 <=7 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=4 & xG1 >=7 & xG1 <=7 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=4 & xG1 >=9 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=4 & xG1 >=9 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=6 & xG1 >=2 & xG1 <=2 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=6 & xG1 >=2 & xG1 <=2 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 
  //horizontal corridor
  [g1] (yG1=6 & xG1 >=6 & xG1 <=9 & dG1 =0) -> 1:(xG1'=xG1+1) & (dG1'=0); 
  [g1] (yG1=6 & xG1 >=6 & xG1 <=9 & dG1 =2) -> 1:(xG1'=xG1-1) & (dG1'=2); 

  //vertical corridor
  [g1] (xG1=1 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=1 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=3 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=3 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=3 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=3 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=5 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=5 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=6 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=6 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=8 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=8 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=10 & yG1 >=2 & yG1 <=3 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=10 & yG1 >=2 & yG1 <=3 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 
  //vertical corridor
  [g1] (xG1=10 & yG1 >=5 & yG1 <=5 & dG1=1) -> 1:(yG1'=yG1+1) & (dG1'=1); 
  [g1] (xG1=10 & yG1 >=5 & yG1 <=5 & dG1 =3) -> 1:(yG1'=yG1-1) & (dG1'=3); 

  //deadends
  [g1] (xG1=1 & yG1=6) -> 1: (xG1'=xG1+1) & (dG1'=0);

  //corners
  [g1] (xG1=1 & yG1=1 & (dG1=2 | dG1=1))-> 1: (yG1'=yG1+1) & (dG1'=1);
  [g1] (xG1=1 & yG1=1 & (dG1=3 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0);
  [g1] (xG1=1 & yG1=4 & (dG1=2 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3);
  [g1] (xG1=1 & yG1=4 & (dG1=1 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0);
  [g1] (xG1=3 & yG1=6 & (dG1=0 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3);
  [g1] (xG1=3 & yG1=6 & (dG1=1 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2);
  [g1] (xG1=5 & yG1=6 & (dG1=2 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3);
  [g1] (xG1=5 & yG1=6 & (dG1=1 | dG1=0)) -> 1: (xG1'=xG1+1) & (dG1'=0);
  [g1] (xG1=10 & yG1=1 & (dG1=0 | dG1=1))-> 1: (yG1'=yG1+1) & (dG1'=1);
  [g1] (xG1=10 & yG1=1 & (dG1=3 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2);
  [g1] (xG1=10 & yG1=6 & (dG1=0 | dG1=3)) -> 1: (yG1'=yG1-1) & (dG1'=3);
  [g1] (xG1=10 & yG1=6 & (dG1=1 | dG1=2)) -> 1: (xG1'=xG1-1) & (dG1'=2);


  //crossing at position (3, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g1] (xG1=3 & yG1=1 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=3 & yG1=1 & dG1=3 & xG1 0.92: (xG1'=xG1+1) & (dG1'=0) + 0.08: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=3 & yG1=1 & dG1=2 & xG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g1] (xG1=3 & yG1=1 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=3 & yG1=1 & dG1=3 & yG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=3 & yG1=1 & dG1=2 & yG1 0.8: (yG1'=yG1+1) & (dG1'=1) + 0.2: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g1] (xG1=3 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=3 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=3 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g1] (xG1=3 & yG1=1 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=3 & yG1=1 & dG1=3 & xG1 0.78: (xG1'=xG1+1) & (dG1'=0) + 0.22: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=3 & yG1=1 & dG1=2 & xG1 0.86: (yG1'=yG1+1) & (dG1'=1) + 0.14: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g1] (xG1=3 & yG1=1 & dG1=0 & xG1>xP & yG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=3 & yG1=1 & dG1=3 & xG1>xP & yG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=3 & yG1=1 & dG1=2 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g1] (xG1=3 & yG1=1 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (6, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g1] (xG1=6 & yG1=1 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=6 & yG1=1 & dG1=3 & xG1 0.64: (xG1'=xG1+1) & (dG1'=0) + 0.36: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=6 & yG1=1 & dG1=2 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g1] (xG1=6 & yG1=1 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=6 & yG1=1 & dG1=3 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=6 & yG1=1 & dG1=2 & yG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g1] (xG1=6 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=6 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=6 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 0.22: (yG1'=yG1+1) & (dG1'=1) + 0.78: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g1] (xG1=6 & yG1=1 & dG1=0 & xG1 0.46: (xG1'=xG1+1) & (dG1'=0) + 0.54: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=6 & yG1=1 & dG1=3 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=6 & yG1=1 & dG1=2 & xG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g1] (xG1=6 & yG1=1 & dG1=0 & xG1>xP & yG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=6 & yG1=1 & dG1=3 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=6 & yG1=1 & dG1=2 & xG1>xP & yG1 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.67: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g1] (xG1=6 & yG1=1 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (8, 1)  [t-up crossing]
 
  //- positioning pacman = r

  [g1] (xG1=8 & yG1=1 & dG1=0 & xG1 0.4: (xG1'=xG1+1) & (dG1'=0) + 0.6: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=8 & yG1=1 & dG1=3 & xG1 0.92: (xG1'=xG1+1) & (dG1'=0) + 0.08: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=8 & yG1=1 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g1] (xG1=8 & yG1=1 & dG1=0 & yG1 0.4: (xG1'=xG1+1) & (dG1'=0) + 0.6: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=8 & yG1=1 & dG1=3 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=8 & yG1=1 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g1] (xG1=8 & yG1=1 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=8 & yG1=1 & dG1=3 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=8 & yG1=1 & dG1=2 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g1] (xG1=8 & yG1=1 & dG1=0 & xG1 0.36: (xG1'=xG1+1) & (dG1'=0) + 0.64: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=8 & yG1=1 & dG1=3 & xG1 0.75: (xG1'=xG1+1) & (dG1'=0) + 0.25: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=8 & yG1=1 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g1] (xG1=8 & yG1=1 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=8 & yG1=1 & dG1=3 & xG1>xP & yG1 0.2: (xG1'=xG1+1) & (dG1'=0) + 0.8: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=8 & yG1=1 & dG1=2 & xG1>xP & yG1 0.67: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g1] (xG1=8 & yG1=1 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (3, 4)  [center crossing]

  //- positioning pacman = r

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1 0.61: (xG1'=xG1+1) & (dG1'=0) + 0.26: (xG1'=xG1-1) & (dG1'=2) + 0.13: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u

  [g1] (xG1=3 & yG1=4 & dG1=0 & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & yG1 0.16: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1) + 0.17: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & yG1 0.28: (yG1'=yG1+1) & (dG1'=1) + 0.43: (xG1'=xG1-1) & (dG1'=2) + 0.29: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = l

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.34: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d

  [g1] (xG1=3 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u-r

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.25: (xG1'=xG1-1) & (dG1'=2) + 0.25: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = u-l

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1 0.34: (yG1'=yG1+1) & (dG1'=1) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d-r

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1yP ) -> 0.67: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- positioning pacman = d-l

  [g1] (xG1=3 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 0.34: (xG1'=xG1+1) & (dG1'=0) + 0.33: (yG1'=yG1+1) & (dG1'=1) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right, up or down
  [g1] (xG1=3 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right, up or left
  [g1] (xG1=3 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go up, left or down
  [g1] (xG1=3 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go right, left or down

  //- position pacman == position ghost

  [g1] (xG1=3 & yG1=4 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (5, 4)  [t-up crossing]
 
  //- positioning pacman = r

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1 0.89: (xG1'=xG1+1) & (dG1'=0) + 0.11: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u

  [g1] (xG1=5 & yG1=4 & dG1=0 & yG1 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & yG1 0.83: (yG1'=yG1+1) & (dG1'=1) + 0.17: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = l

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.17: (xG1'=xG1+1) & (dG1'=0) + 0.83: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.17: (yG1'=yG1+1) & (dG1'=1) + 0.83: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d

  [g1] (xG1=5 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-r

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1 0.75: (yG1'=yG1+1) & (dG1'=1) + 0.25: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = u-l

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d-r

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1yP ) -> 0.95: (xG1'=xG1+1) & (dG1'=0) + 0.05: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- positioning pacman = d-l

  [g1] (xG1=5 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1+1) & (dG1'=1);  // ghost is moving to the right -> continues to go right or up
  [g1] (xG1=5 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 0.11: (xG1'=xG1+1) & (dG1'=0) + 0.89: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go right or left
  [g1] (xG1=5 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving to the left -> continues to go up or left

  //- position pacman == position ghost

  [g1] (xG1=5 & yG1=4 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (6, 4)  [t-down crossing]
 
  //- positioning pacman = r

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1 0.57: (xG1'=xG1+1) & (dG1'=0) + 0.43: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u

  [g1] (xG1=6 & yG1=4 & dG1=0 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = l

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.75: (xG1'=xG1-1) & (dG1'=2) + 0.25: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d

  [g1] (xG1=6 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-r

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1 0.89: (xG1'=xG1+1) & (dG1'=0) + 0.11: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-l

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1 0.67: (xG1'=xG1-1) & (dG1'=2) + 0.33: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-r

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1yP ) -> 0.69: (xG1'=xG1+1) & (dG1'=0) + 0.31: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1yP ) -> 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1yP ) -> 0.33: (xG1'=xG1-1) & (dG1'=2) + 0.67: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-l

  [g1] (xG1=6 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=6 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=6 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving left -> continues to go left or down

  //- position pacman == position ghost

  [g1] (xG1=6 & yG1=4 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (8, 4)  [t-down crossing]
 
  //- positioning pacman = r

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u

  [g1] (xG1=8 & yG1=4 & dG1=0 & yG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = l

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 0.44: (xG1'=xG1+1) & (dG1'=0) + 0.56: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1=yP ) -> 0.83: (xG1'=xG1-1) & (dG1'=2) + 0.17: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d

  [g1] (xG1=8 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.43: (xG1'=xG1+1) & (dG1'=0) + 0.57: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & yG1>yP & xG1=xP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-r

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1 1.0: (xG1'=xG1+1) & (dG1'=0);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = u-l

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1 0.33: (xG1'=xG1+1) & (dG1'=0) + 0.67: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1 0.83: (xG1'=xG1-1) & (dG1'=2) + 0.17: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-r

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1yP ) -> 0.56: (xG1'=xG1+1) & (dG1'=0) + 0.44: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- positioning pacman = d-l

  [g1] (xG1=8 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go right or down
  [g1] (xG1=8 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1+1) & (dG1'=0) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go right or left
  [g1] (xG1=8 & yG1=4 & dG1=2 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving left -> continues to go left or down

  //- position pacman == position ghost

  [g1] (xG1=8 & yG1=4 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);

  //crossing at position (10, 4)  [t-left crossing]

  //- positioning pacman = u

  [g1] (xG1=10 & yG1=4 & dG1=0 & yG1 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go up or down
  [g1] (xG1=10 & yG1=4 & dG1=1 & yG1 0.45: (yG1'=yG1+1) & (dG1'=1) + 0.55: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go up or left
  [g1] (xG1=10 & yG1=4 & dG1=3 & yG1 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = l

  [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1=yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go up or down
  [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1=yP ) -> 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go up or left
  [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1=yP ) -> 0.79: (xG1'=xG1-1) & (dG1'=2) + 0.21: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = d

  [g1] (xG1=10 & yG1=4 & dG1=0 & yG1>yP & xG1=xP ) -> 0.2: (yG1'=yG1+1) & (dG1'=1) + 0.8: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go up or down
  [g1] (xG1=10 & yG1=4 & dG1=1 & yG1>yP & xG1=xP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go up or left
  [g1] (xG1=10 & yG1=4 & dG1=3 & yG1>yP & xG1=xP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = u-l

  [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1 0.75: (yG1'=yG1+1) & (dG1'=1) + 0.25: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go up or down
  [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1 0.44: (yG1'=yG1+1) & (dG1'=1) + 0.56: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go up or left
  [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1 1.0: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving down -> continues to go left or down

  //- positioning pacman = d-l

  [g1] (xG1=10 & yG1=4 & dG1=0 & xG1>xP & yG1>yP ) -> 1.0: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving to the right -> continues to go up or down
  [g1] (xG1=10 & yG1=4 & dG1=1 & xG1>xP & yG1>yP ) -> 0.5: (yG1'=yG1+1) & (dG1'=1) + 0.5: (xG1'=xG1-1) & (dG1'=2);  // ghost is moving up -> continues to go up or left
  [g1] (xG1=10 & yG1=4 & dG1=3 & xG1>xP & yG1>yP ) -> 0.5: (xG1'=xG1-1) & (dG1'=2) + 0.5: (yG1'=yG1-1) & (dG1'=3);  // ghost is moving down -> continues to go left or down

  //- position pacman == position ghost

  [g1] (xG1=10 & yG1=4 &  xG1=xP & yG1=yP) -> 1: (xG1'=xG1);
endmodule

//PACMAN
module pacman
  xP : [1..xSize] init 1;// x position of Pacman
  yP : [1..ySize] init 1;// y position of Pacman
  dP : [0 .. 3] init 0; //direction of pacman (0=right, 1=up, 2=left, 3=down)

  //horizontal corridor
  [p] (yP=1 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=1 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=1 & xP >=4 & xP <=5 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=1 & xP >=4 & xP <=5 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=1 & xP >=7 & xP <=7 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=1 & xP >=7 & xP <=7 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=1 & xP >=9 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=1 & xP >=9 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=4 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=4 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=4 & xP >=4 & xP <=4 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=4 & xP >=4 & xP <=4 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=4 & xP >=7 & xP <=7 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=4 & xP >=7 & xP <=7 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=4 & xP >=9 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=4 & xP >=9 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=6 & xP >=2 & xP <=2 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=6 & xP >=2 & xP <=2 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 
  //horizontal corridor
  [p] (yP=6 & xP >=6 & xP <=9 & dP =0) -> 1:(xP'=xP+1) & (dP'=0); 
  [p] (yP=6 & xP >=6 & xP <=9 & dP =2) -> 1:(xP'=xP-1) & (dP'=2); 

  //vertical corridor
  [p] (xP=1 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=1 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=3 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=3 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=3 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=3 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=5 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=5 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=6 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=6 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=8 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=8 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=10 & yP >=2 & yP <=3 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=10 & yP >=2 & yP <=3 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 
  //vertical corridor
  [p] (xP=10 & yP >=5 & yP <=5 & dP=1) -> 1:(yP'=yP+1) & (dP'=1); 
  [p] (xP=10 & yP >=5 & yP <=5 & dP =3) -> 1:(yP'=yP-1) & (dP'=3); 

  //deadends
  [p] (xP=1 & yP=6) -> 1: (xP'=xP+1) & (dP'=0);

  //corners
  [p] (xP=1 & yP=1 & (dP=2 | dP=1))-> 1: (yP'=yP+1) & (dP'=1);
  [p] (xP=1 & yP=1 & (dP=3 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0);
  [p] (xP=1 & yP=4 & (dP=2 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3);
  [p] (xP=1 & yP=4 & (dP=1 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0);
  [p] (xP=3 & yP=6 & (dP=0 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3);
  [p] (xP=3 & yP=6 & (dP=1 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2);
  [p] (xP=5 & yP=6 & (dP=2 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3);
  [p] (xP=5 & yP=6 & (dP=1 | dP=0)) -> 1: (xP'=xP+1) & (dP'=0);
  [p] (xP=10 & yP=1 & (dP=0 | dP=1))-> 1: (yP'=yP+1) & (dP'=1);
  [p] (xP=10 & yP=1 & (dP=3 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2);
  [p] (xP=10 & yP=6 & (dP=0 | dP=3)) -> 1: (yP'=yP-1) & (dP'=3);
  [p] (xP=10 & yP=6 & (dP=1 | dP=2)) -> 1: (xP'=xP-1) & (dP'=2);

  // crossing at position(3, 1)

  [right] (xP=3 & yP=1) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=3 & yP=1) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=3 & yP=1) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=3 & yP=1 & pMove=2) -> 1: (xP'=xP);

  // crossing at position(6, 1)

  [right] (xP=6 & yP=1) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=6 & yP=1) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=6 & yP=1) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=6 & yP=1 & pMove=2) -> 1: (xP'=xP);

  // crossing at position(8, 1)

  [right] (xP=8 & yP=1) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=8 & yP=1) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=8 & yP=1) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=8 & yP=1 & pMove=2) -> 1: (xP'=xP);

  // crossing at position(3, 4)

  [right] (xP=3 & yP=4) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=3 & yP=4) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=3 & yP=4) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=3 & yP=4) -> 1: (yP'=yP-1) & (dP'=3);

  // crossing at position(5, 4)

  [right] (xP=5 & yP=4) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=5 & yP=4) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=5 & yP=4) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=5 & yP=4 & pMove=2) -> 1: (xP'=xP);

  // crossing at position(6, 4)

  [right] (xP=6 & yP=4) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=6 & yP=4 & pMove=2) -> 1: (xP'=xP);
  [left] (xP=6 & yP=4) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=6 & yP=4) -> 1: (yP'=yP-1) & (dP'=3);

  // crossing at position(8, 4)

  [right] (xP=8 & yP=4) -> 1: (xP'=xP+1) & (dP'=0);
  [up] (xP=8 & yP=4 & pMove=2) -> 1: (xP'=xP);
  [left] (xP=8 & yP=4) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=8 & yP=4) -> 1: (yP'=yP-1) & (dP'=3);

  // crossing at position(10, 4)

  [right] (xP=10 & yP=4 & pMove=2) -> 1: (xP'=xP);
  [up] (xP=10 & yP=4) -> 1: (yP'=yP+1) & (dP'=1);
  [left] (xP=10 & yP=4) -> 1: (xP'=xP-1) & (dP'=2);
  [down] (xP=10 & yP=4) -> 1: (yP'=yP-1) & (dP'=3);

endmodule

//CRASH
label "Crash" = (xP = xG0 & yP = yG0) | (xP = xG1 & yP = yG1);
//label "Safe" = deactive0 & deactive1;
Contents of file: property.props
"crash": Pmin=? [F "Crash"]
Contents of file: model.jani
File too large to display (size: 1.65 MB).