1

我似乎太傻了,看不到它。日志显示我的语法错误在哪里(第 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

我很乐意给小费..

4

1 回答 1

2

事实证明,我需要在 if 语句之后使用分号。

于 2013-10-02T21:30:38.117 回答