Search code examples
if-statementsyntaxpromelaspin

Semicolon usage in Promela

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.

Solution

  • 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.