# Exclusion Pattern

### Syntax

Exclusion(R_1,R_2,...,R_n), where R_i is a region (1<=i<=n).

### Description

Threads can be in at most one region out of n regions at any point of time (mutally exclusion).

### Diagram

### Representation as Global Invariant

UnboundedGlobal InvariantLet Comb(n,n-1) denote the collection of combinations of n-1 out of n from the set {1,2,...,n}. Then the global invariant is

Or_{C in Comb(n,n-1)}(And_{ i in C }(In_i - Out_i == 0))For example, if n=3, Comb(3,2) is {{1,2},{1,3},{2,3}}. Therefore, the global invariant for Exclusion(R_1,R_2,R_3) is

((In_1 - Out_1 == 0) and (In_2 - Out_2 == 0)) or

((In_1 - Out_1 == 0) and (In_3 - Out_3 == 0)) or

((In_2 - Out_2 == 0) and (In_3 - Out_3 == 0))

Bounded Global Invariant Counter Version

Or_{C in Comb(n,n-1)}(And_{ i in C }((E_i == 0)))

### Links to examples that use this pattern

Single Sleeping Barber Problem, Multiple Sleeping Barbers Problem, Reader writer problem, and Gyroscope Rudder problem