我似乎太傻了,看不到它。日志显示我的语法错误在哪里(第 12、22 和 25 行),我阅读了一些教程,但找不到错误。
程序很简单,它应该通过一个同步通道计算0和1的数量。
这是我的代码:
1
2 chan ch = [0] of {bool};
3 byte zero, one;
4 bool message;
5
6 proctype A() {
7 startA:
8 if
9 :: ch ! 0
10 :: ch ! 1
11 fi
12 goto startA
13 }
14
15 proctype B() {
16 startB:
17 ch ? message;
18 if
19 :: message -> one++
20 :: ! message -> zero++
21 fi
22 goto startB
23 }
24
25 init { atomic {run A(); run B()} }
还有我的语法错误:
spin: firstchannel.pml:12, Error: syntax error saw 'keyword: goto' near 'goto'
spin: firstchannel.pml:22, Error: syntax error saw 'keyword: goto' near 'goto'
spin: firstchannel.pml:25, Error: proctype A not found
我很乐意给小费..