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: ;