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

