Multiple Roller Coaster Cars Problem


Description

This problem is an generalization of single roller coaster car ride problem to contain M cars. For passenger safety, only one car at a time is permitted to go around the track.

Diagram

As being similar to the multiple barbers problem, we assume that each coaster car owns two synchronization objects, one used in cluster(R_C3, R_P2), and another used in cluster(R_C4, R_P3). The differences from the solution for the single car problem are:

  1. use the Group with Information Exchange synchronization in cluster(R_C1, R_P1) to inform the passengers of the references to the synchronization objects of the matching coaster car,
  2. use the specific AsymmetricGroup synchronization in clusters (R_C3, R_P2) and (R_C4, R_P3), using the synchronization objects of the car, instead of the anonymous AsymmetricGroup synchronization, and
  3. form synchronization region R_C2 for step C2, which forms a cluster(R_C2) with synchronization Bound(R_C2, 1); this guarantees only one car can go around the track.
In the diagram, R_C2 overlaps with region R_C1.

multiple 
      roller coaster cars diagram

Synchronization Specification


Cluster: C1P1R1;
Regions: C1,P1;
Invariant: Bound(C1,1) + Bound(P1,10);

Cluster: C1P1R2;
Regions: C1,P1;
Invariant: Group(C1,1,P1,10);

Cluster: C1P1R3;
Regions: C1,P1;
Invariant: Group(C1,1,P1,10);

Cluster: RC2;
Regions: C2;
Invariant: Bound(C2,1);

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, Bound, AsymmetricGroup.

Global Invariant

Unbounded Global Invariant

  • For cluster C1P1R1 which consists of regions C11 and P11:
    (In_C11 - Out_C11 <= 1) and (In_P11 - Out_P11 <=C)
  • For cluster C1P1R2 which consists of regions C12 and P12:
    (Out_C12 <= In_P12/C) and (Out_C12 <= In_C12) and (Out_P12 <= In_C12*C) and (Out_P12 <= In_C12/10*10)
  • For cluster C1P1R3 which consists of regions C13 and P13:
    (Out_C13 <= In_P13/C) and (Out_C13 <= In_C13) and (Out_P13 <= In_C13*C) and (Out_P13 <= In_C13/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 C1P1R1 which consists of regions C11 and P11:
    (B1 <= 1) and (B2 <= C)
  • For cluster C1P1R2 which consists of regions C12 and P12:
    (G1_11 <= 0) and (G1_12 <= 0) and (G1_22 <= 0) and (G1_21 <= 0)
  • For cluster C1P1R3 which consists of regions C13 and P13:
    (G2_11 <= 0) and (G2_12 <= 0) and (G2_22 <= 0) and (G2_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

To be added.

Unbounded Coarse-Grain Solution

CLUSTER: C1P1R1
STATE SPACE VARIABLES: C11_in, C11_out, P11_in, P11_out;
REGION: C11
ENTER: <AWAIT C11_in == C11_out --> C11_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <C11_out++;>
NOTIFY: C11_in;
NOTIFYALL: ;

REGION: P11
ENTER: <AWAIT P11_in <= P11_out + 9 --> P11_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <P11_out++;>
NOTIFY: P11_in;
NOTIFYALL: ;

CLUSTER: C1P1R2
STATE SPACE VARIABLES: C12_in, C12_out, P12_in, P12_out;
REGION: C12
ENTER: <C12_in++;>
NOTIFY: C12_out;
NOTIFYALL: P12_out;
EXIT: <AWAIT C12_out + 1 <= C12_in && C12_out + 1 <= P12_in / 10 --> C12_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: P12
ENTER: <P12_in++;>
NOTIFY: C12_out;
NOTIFYALL: P12_out;
EXIT: <AWAIT P12_out + 1 <= C12_in * 10 && P12_out + 1 <= P12_in / 10 * 10 --> P12_out++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: C1P1R3
STATE SPACE VARIABLES: C13_in, C13_out, P13_in, P13_out;
REGION: C13
ENTER: <C13_in++;>
NOTIFY: C13_out;
NOTIFYALL: P13_out;
EXIT: <AWAIT C13_out + 1 <= C13_in && C13_out + 1 <= P13_in / 10 --> C13_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: P13
ENTER: <P13_in++;>
NOTIFY: C13_out;
NOTIFYALL: P13_out;
EXIT: <AWAIT P13_out + 1 <= C13_in * 10 && P13_out + 1 <= P13_in / 10 * 10 --> P13_out++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: RC2
STATE SPACE VARIABLES: C2_in, C2_out;
REGION: C2
ENTER: <AWAIT C2_in == C2_out --> C2_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <C2_out++;>
NOTIFY: C2_in;
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: C1P1R1
STATE SPACE VARIABLES: B1, B2;
LOCAL VARIABLES: ;
REGION: C11
ENTER: <AWAIT B1 == 0 --> B1++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B1--;>
NOTIFY: C11_in;
NOTIFYALL: ;

REGION: P11
ENTER: <AWAIT B2 <= 9 --> B2++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B2--;>
NOTIFY: P11_in;
NOTIFYALL: ;

CLUSTER: C1P1R2
STATE SPACE VARIABLES: G1_1_1, G1_1_2, G1_2_1, G1_2_2;
LOCAL VARIABLES: L1_1, L1_2;
REGION: C12
ENTER: <L1_1+=1; if(L1_1==1) {G1_1_1 -=1;G1_2_1 -=10;L1_1=0;};>
NOTIFY: C12_out;
NOTIFYALL: P12_out;
EXIT: <AWAIT G1_1_1 <= -1 && G1_1_2 <= -1 --> G1_1_1 +=1;G1_1_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;

REGION: P12
ENTER: <L1_2+=1; if(L1_2==10) {G1_1_2 -=1;G1_2_2 -=10;L1_2=0;};>
NOTIFY: C12_out;
NOTIFYALL: P12_out;
EXIT: <AWAIT G1_2_1 <= -1 && G1_2_2 <= -1 --> G1_2_1 +=1;G1_2_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: C1P1R3
STATE SPACE VARIABLES: G2_1_1, G2_1_2, G2_2_1, G2_2_2;
LOCAL VARIABLES: L2_1, L2_2;
REGION: C13
ENTER: <L2_1+=1; if(L2_1==1) {G2_1_1 -=1;G2_2_1 -=10;L2_1=0;};>
NOTIFY: C13_out;
NOTIFYALL: P13_out;
EXIT: <AWAIT G2_1_1 <= -1 && G2_1_2 <= -1 --> G2_1_1 +=1;G2_1_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;

REGION: P13
ENTER: <L2_2+=1; if(L2_2==10) {G2_1_2 -=1;G2_2_2 -=10;L2_2=0;};>
NOTIFY: C13_out;
NOTIFYALL: P13_out;
EXIT: <AWAIT G2_2_1 <= -1 && G2_2_2 <= -1 --> G2_2_1 +=1;G2_2_2 +=1;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: RC2
STATE SPACE VARIABLES: B3;
LOCAL VARIABLES: ;
REGION: C2
ENTER: <AWAIT B3 == 0 --> B3++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B3--;>
NOTIFY: C2_in;
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

To be added.