I seem to be too stupid to see it. The log shows me where my syntax errors are (line 12, 22 and 25), I read some tutorials, but cannot find the errors..
The program is very simple, it should count the amount of 0's and 1's through a synchronized channel.
Here is my code:
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()} }
And my syntax errors:
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
I'd be happy for a tip..
Turns out, I need semicolons after the if statements.