Asymmetric Group Pattern


AsymmetricGroup(n,R_11,N_11,R_12,N_12...,R_1n,N_1n,m,R_21,N_21,R_22,N_22,...,R_2m,N_2m), where R_1i and R_2j (1<=i<=n,1<=j<=m) are regions, and n,m,N_1i, and N_2j (1<=i<=n,1<=j<=m) are integers.


For 0<=k, all threads from the (k*N_2j)th thread to the ((k+1)*N_2j-1)th thread entering R_2j, for 1<=j<=m, may leave their respective regions only if all threads from the (k*N_1i)th thread to the ((k+1)*N_1i-1)th thread have arrived at regions R_1i, for 1<=i<=n.


Representation as Global Invariant

Unbounded Global Invariant

And 1<= j <= m ( And 1<= i <= n (Out_2j <= (In_1i/N_1i) * N_2j))

Bounded Global Invariant Counter Version

And 1<= j <= m (And 1<= i <= n (G_ji <= 0))

Links to examples that use this pattern

Single Roller Coaster Car Problem and Multiple Roller Coaster Cars Problem