SGCluster.java

class SGCluster$C1C3 {
// STATE SPACE VARIABLES: 

private static int B1 , B2 , E1_0 , E1_1 ;

// LOCAL VARIABLES: 

private static Object clusterCounterLock = new Object();


/**======================================================**
 **
 ** Generated lock and methods for await: C1$enter
 **
 **======================================================**/

private static Object condition$C1$enter = new Object();

public static void C1$enter(){
   synchronized (condition$C1$enter) {

      while ( !check$C1$enter())
         try {

            condition$C1$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$C1$enter() {

   synchronized (clusterCounterLock) {
      if (B1 == 0 && E1_1 == 0 ) {

         B1 ++ ; E1_0 ++ ; ;

         return true;
      } else
         return false;

   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: C1$exit
 **
 **======================================================**/

public static void C1$exit() {

   synchronized (clusterCounterLock) {
      B1 -- ; E1_0 -- ; ;

   }
   synchronized (condition$C1$enter) {
      condition$C1$enter.notify(); 
   }

   synchronized (condition$C3$enter) {
      condition$C3$enter.notifyAll(); 
   }


}


/**======================================================**
 **
 ** Generated lock and methods for await: C3$enter
 **
 **======================================================**/

private static Object condition$C3$enter = new Object();

public static void C3$enter(){
   synchronized (condition$C3$enter) {

      while ( !check$C3$enter())
         try {

            condition$C3$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$C3$enter() {

   synchronized (clusterCounterLock) {
      if (B2 == 0 && E1_0 == 0 ) {

         B2 ++ ; E1_1 ++ ; ;

         return true;
      } else
         return false;

   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: C3$exit
 **
 **======================================================**/

public static void C3$exit() {

   synchronized (clusterCounterLock) {
      B2 -- ; E1_1 -- ; ;

   }
   synchronized (condition$C3$enter) {
      condition$C3$enter.notify(); 
   }

   synchronized (condition$C1$enter) {
      condition$C1$enter.notifyAll(); 
   }


}

}


syntax highlighted by Code2HTML, v. 0.9