module MutualExclusionModule {
  var s: integer;
  var y0: boolean;
  var y1: boolean;
  var pc0: integer;
  var pc1: integer;

  init {
    s = 1;
    y0 = false;
    y1 = false;
    pc0 = 0;
    pc1 = 0;

  }
  next {
    pc0' = (if (pc0 == 0) then 1 else (if (pc0 == 1) then 2 else (if ((pc0 == 2) && (!y1 || (s != 0))) then 3 else (if (pc0 == 3) then 4 else (if (pc0 == 4) then 5 else 0)))));
    pc1' = (if (pc1 == 0) then 1 else (if (pc1 == 1) then 2 else (if ((pc1 == 2) && (!y0 || (s != 1))) then 3 else (if (pc1 == 3) then 4 else (if (pc1 == 4) then 5 else 0)))));
    y0' = (if (pc0 == 2) then true else (if (pc0 == 5) then false else y0));
    y1' = (if (pc1 == 2) then true else (if (pc1 == 5) then false else y1));
    s' = (if (pc0 == 2) then 0 else (if (pc1 == 2) then 1 else s));

  }
}
