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

  • 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
The scenario for a passenger thread is (it repeats the following steps):
  • 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)
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.

single roller coaster 
      ride diagram

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

 

Unbounded and Bounded Fine-Grain Solutions