形式语言与自动机的规约有没有人会，能写下面代码的规约吗？

Question

#define true 1
#define false 0
#define true 1
#define false 0

bool busy[3];

chan   up[3] = [1] of { byte };
chan down[3] = [1] of { byte };

mtype = { start, attention, data, stop }

proctype station(,byte id; chan inp, out)
{    do
    :: inp?start ->
        atomic { !busy[id] -> busy[id] = true };
        out!attention;
        do
        :: inp?data -> out!data
        :: inp?stop -> break
        od;
        out!stop;
        busy[id] = false
    :: atomic { !busy[id] -> busy[id] = true };
        out!start;
        inp?attention;
        do
        :: out!data -> inp?data
        :: out!stop -> break
        od;
        inp?stop;
        busy[id] = false
    od
}

init {
    atomic {
        run station(0, up[2], down[2]);
        run station(1, up[0], down[0]);
        run station(2, up[1], down[1]);

        run station(0, down[0], up[0]);
        run station(1, down[1], up[1]);
        run station(2, down[2], up[2])
    }
}