Single Roller Coaster Car Problem
Description
Suppose there are n passengers and one roller coaster car. The passengers repeatedly wait to take rides in the car, which holds C passengers. However, the car can go around the track only when it is full. The car takes the same T seconds to go around the track each time it fills up. After getting a ride, each passenger wanders around the amusement park for a random amount of time before returning to the roller coaster for another ride.
Diagram
The scenario for a car thread is (it repeats the following steps):
The scenario for a passenger thread is (it repeats the following steps):
- C1 {assertion: the car is empty} waits until C passengers have gotten on the car
- C2 {assertion: C passengers are on the coaster} goes around the track (elapse T seconds)
- C3 stops and has the passengers get off the car
- C4 waits until all C passengers have left
Steps C1, C3, and C4 constitute synchronization regions, denoted R_C1, R_C3, and R_C4, respectively. Steps P1, P2, and P3 constitute synchronization regions, denoted R_P1, R_P2, and R_P3, respectively. There are three clusters: (R_C1,R_P1), (R_C3,R_P2), and (R_C4,R_P3). The first forms the Group(R_C1,1,R_P1,C) synchronization. The later two clusters form the AsymmetricGroup synchronization.
- P1 waits until getting on the car
- P2 {assertion: the passenger is on the car} waits until the car goes around and stops
- P3 {assertion: the car has stopped} gets off the car
- P4 wanders around the amusement park (elapse a random amount of time)
Synchronization Specification
Cluster: C1P1;
Regions: C1,P1;
Invariant: Group(C1,1,P1,10);Cluster: C3P2;
Regions: C3,P2;
Invariant: AsymmetricGroup(1,C3,1,1,P2,10);Cluster: C4P3;
Regions: C4,P3;
Invariant: AsymmetricGroup(1,P3,10,1,C4,1);
Patterns Used
Group and AsymmetricGroup.
Global Invariant
Unbounded Global Invariant
- For cluster C1P1 which consists of regions C1 and P1:
(Out_C1 <= In_P1/C) and (Out_C1 <= In_C1) and (Out_P1 <= In_C1*C) and (Out_P1 <= In_C1/10*10)
- For cluster C3P2 which consists of regions C3 and P2:
Out_P2 <= In_C3*C
- For cluster C4P3 which consists of regions C4 and P3:
Out_C4 <= In_P3 /C
Bounded Global Invariant Counter Version
- For cluster C1P1 which consists of regions C1 and P1:
(G_11 <= 0) and (G_12 <= 0) and (G_22 <= 0) and (G_21 <= 0)
- For cluster C3P2 which consists of regions C3 and P2:
AG1_11 <= 0
- For cluster C4P3 which consists of regions C4 and P3:
AG2_11 <= 0
Core Functional Code
class Car extends Thread {
int times;
Car(int times) {
this.times = times;
}
public void run() {
while(times>0) {
// R_C1
/*** C1P1 C1 enter ***/
System.out.println("Car waits passengers");
/*** C1P1 C1 exit ***/
System.out.println("Car has C passengers");
//R_C2
System.out.println("Car goes round the track");
//R_C3
/*** C3P2 C3 enter ***/
System.out.println("Car stops and has the passenages get off the car ");
/*** C3P2 C3 exit ***/
System.out.println("");
//R_C4
/*** C4P3 C4 enter ***/
System.out.println("Car waits until all C passenagers have left");
/*** C4P3 C4 exit ***/
System.out.println("Car has all C passenagers have left");
times--;
}
}
}
class Passenger extends Thread {
private int id;
Passenger (int id) {
this.id = id;
}
public void run() {
//R_P1
/*** C1P1 P1 enter ***/
System.out.println("Passenger "+id+"waits to get on the car");
/*** C1P1 P1 exit ***/
System.out.println("Passenger "+id+"starts to get off the car");
/*** C3P2 P2 enter ***/
System.out.println("Passenger "+id+"waits to the car goes around");
/*** C3P2 P2 exit ***/
System.out.println("Passenger "+id+"the car goes around and stops");
/*** C4P3 P3 enter ***/
System.out.println("Passenger "+id+"starts to get off the car");
/*** C4P3 P3 exit ***/
System.out.println("Passenger "+id+"got off the car");
}
}
public class Roller {
public static void main(String[] arg) {
Car car = new Car(4);
Passenger passengers[] = new Passenger[30];
car.start();
for(int i=0;i<30;i++){
passengers[i] = new Passenger(i);
passengers[i].start();
}
}
}
Unbounded Coarse-Grain Solution
CLUSTER: C1P1
STATE SPACE VARIABLES: C1_in, C1_out, P1_in, P1_out;
REGION: C1
ENTER: <C1_in++;>
NOTIFY: C1_out;
NOTIFYALL: P1_out;
EXIT: <AWAIT C1_out + 1 <= C1_in && C1_out + 1 <= P1_in / 10 --> C1_out++;>
NOTIFY: ;
NOTIFYALL: ;REGION: P1
ENTER: <P1_in++;>
NOTIFY: C1_out;
NOTIFYALL: P1_out;
EXIT: <AWAIT P1_out + 1 <= C1_in * 10 && P1_out + 1 <= P1_in / 10 * 10 --> P1_out++;>
NOTIFY: ;
NOTIFYALL: ;CLUSTER: C3P2
STATE SPACE VARIABLES: C3_in, P2_out;
REGION: C3
ENTER: <C3_in++;>
NOTIFY: ;
NOTIFYALL: P2_out;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;REGION: P2
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT P2_out + 1 <= C3_in * 10 --> P2_out++;>
NOTIFY: ;
NOTIFYALL: ;CLUSTER: C4P3
STATE SPACE VARIABLES: P3_in, C4_out;
REGION: C4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT C4_out + 1 <= P3_in / 10 --> C4_out++;>
NOTIFY: ;
NOTIFYALL: ;REGION: P3
ENTER: <P3_in++;>
NOTIFY: ;
NOTIFYALL: C4_out;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;
Bounded Counter Coarse-Grain Solution
CLUSTER: C1P1
STATE SPACE VARIABLES: G1_1_1, G1_1_2, G1_2_1, G1_2_2;
LOCAL VARIABLES: L1_1, L1_2;
REGION: C1
ENTER: <L1_1+=1; if(L1_1==1) {G1_1_1 -=1;G1_2_1 -=10;L1_1=0;};>
NOTIFY: C1_out;
NOTIFYALL: P1_out;
EXIT: <AWAIT G1_1_1 <= -1 && G1_1_2 <= -1 --> G1_1_1 +=1;G1_1_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;REGION: P1
ENTER: <L1_2+=1; if(L1_2==10) {G1_1_2 -=1;G1_2_2 -=10;L1_2=0;};>
NOTIFY: C1_out;
NOTIFYALL: P1_out;
EXIT: <AWAIT G1_2_1 <= -1 && G1_2_2 <= -1 --> G1_2_1 +=1;G1_2_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;CLUSTER: C3P2
STATE SPACE VARIABLES: AG1_1_1;
LOCAL VARIABLES: LA1_1;
REGION: C3
ENTER: <LA1_1+=1; if(LA1_1==1) {AG1_1_1 -=10;LA1_1=0;};>
NOTIFY: ;
NOTIFYALL: P2_out;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;REGION: P2
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT AG1_1_1 <= -1 --> AG1_1_1 ++;>
NOTIFY: ;
NOTIFYALL: ;CLUSTER: C4P3
STATE SPACE VARIABLES: AG2_1_1;
LOCAL VARIABLES: LA2_1;
REGION: C4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT AG2_1_1 <= -1 --> AG2_1_1 ++;>
NOTIFY: ;
NOTIFYALL: ;REGION: P3
ENTER: <LA2_1+=1; if(LA2_1==10) {AG2_1_1 -=1;LA2_1=0;};>
NOTIFY: ;
NOTIFYALL: C4_out;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;