cps-2014-concurrency.lts

const N = 3

SENDER = SENDER[1],
SENDER[i:1..N] = (send[i] -> SENDER[i+1]),
SENDER[N+1] = STOP.

RECEIVER = RECEIVER[1],
RECEIVER[i:1..N] = (recv[i] -> RECEIVER[i+1]
| pass[i]->RECEIVER[i+1]),
RECEIVER[N+1]= STOP.

CHANNEL = CHANNEL[1],
CHANNEL[i:1..N] = (input[i]->CHOICE[i]),
CHOICE[i:1..N] = (success -> output[i] -> CHANNEL[i+1]
|fail -> lost[i] -> CHANNEL[i+1]),
CHANNEL[N+1] = STOP.

||SYSTEM=(SENDER||RECEIVER||CHANNEL)/{send[i:1..N]/input[i],recv[i:1..N]/output[i],lost[i:1..N]/pass[i]}.
||SPEC = (SYSTEM)\{success,fail}.

// https://i.imgur.com/3mBi1PK.png