chan ch[3] = [2] of {byte};

byte critical = 0;
#define mutex (critical <=1)

proctype P(byte inch; byte outch)
{
byte msg;
do
:: /* Waiting for token */
    ch[inch] ? msg;
    /*in critical region */
    critical++;
    /* Leaving critical region */
    critical--;
    ch[outch] ! msg;
od;
}

init {
    ch[0] ! 0;
    atomic {
        run P(0,1);
        run P(1,2);
        run P(2,0);
    }
}

ltl{[]mutex}