I am learning promela syntax for Spin Modal Checker. I encountered this simple piece of code.
int count;
active proctype count(){
if
:: count++
:: count--
fi
}
As I know semicolon is used to define end of statement. Can I use ; in the end of both count++ and count-- and after fi; Will it change the way program is behaving? I would be grateful for clearing this semicolon thing for me.
Semicolons in Promela are so-called separators.
From the reference:
The semicolon and the arrow are equivalent statement separators in Promela; they are not statement terminators, although the parser has been taught to be forgiving for occasional lapses. The last statement in a sequence need not be followed by a statement separator, unlike, for instance, in the C programming language.
So the answer to your question is: you don't need to put semicolons after count++, count--, or fi because they are the last statements. The parser will ignore if you put them there anyway.