#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;有谁知道这个代码的形式规约怎么写？
微信扫一扫
