// Queue of maximum length 2 - accepts a and b interactions
// ex means enter interaction x - gx means get interaction x
Q1 = (ea -> Q1a | eb -> Q1b),
Q1a = (ea -> Q1aa | eb -> Q1ba | ga -> Q1),
Q1b = (ea -> Q1ab | eb -> Q1bb | gb -> Q1),
Q1aa = (ga -> Q1a),
Q1ab = (gb -> Q1a),
Q1ba = (ga -> Q1b),
Q1bb = (gb -> Q1b).

// Queue of maximum length 2 - accepts only c interactions
Q2 = (ec -> Q2c),
Q2c = (ec -> Q2cc  | gc -> Q2),
Q2cc = (gc -> Q2c).

// state machine A - accepts a from environment, then sends c to machine B, 
// or accepts b and goes back to initial state
A0 = (ga -> ec -> A0  | gb -> A0).

// state machine B - accepts c then sends d to the environment
B0 = (gc  -> eb -> ed -> B0).

// composition of these 4 components
||SYSTEM = (A0 || Q1 || Q2 || B0).