- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
Assignments And Expressions
As in C, the assignments
c = c + 1; c = c - 1 /* valid */
can be abbreviated to
c++; c-- /* valid */
but, unlike in C,
b = c++
is not a valid assignment in PROMELA, because the right-hand side operand is not a side effect free expression. There is no equivalent to the shorthands
--c; ++c /* not valid */
in PROMELA, because assignment statements such as
c = c-1; c = c+1 /* valid */
when taken as a unit are not equivalent to expressions in PROMELA. With these constraints, a statement such as --c is always indistinguishable from c--, which is supported.
In assignments such as
variable = expression
the values of all operands used in the expression on the right-hand side of the assignment operator are first cast to signed integers, before any of the operands are applied. The operator precedence rules from C determine the order of evaluation, as reproduced in Table 3.2. After the evaluation of the right-hand side expression completes, and before the assignment takes place, the value produced is cast to the type of the target variable. If the right-hand side yields a value outside the range of the target type, truncation of the assigned value can result. In simulation mode SPIN issues a warning when this occurs; in verification mode, however, this type of truncation is not intercepted.
It is also possible to use C-style conditional expressions in any context where expressions are allowed. The syntax, however, is slightly different from the one used in C. Where in C one would write
expr1 ? expr2 : expr3 /* not valid */
one writes in PROMELA
(expr1 -> expr2 : expr3) /* valid */
The arrow symbol is used here to avoid possible confusion with the question mark from PROMELA receive operations. The value of the conditional expression is equal to the value of expr2 if and only if expr1 evaluates to true and otherwise it equals the value of expr3. PROMELA conditional expressions must be surrounded by parentheses (round braces) to avoid misinterpretation of the arrow as a statement separator.
Table 3.2. Operator Precedence, High to Low
|
Operators |
Associativity |
Comment |
|---|---|---|
|
() [] . |
left to right |
parentheses, array brackets |
|
! ~ ++ -- |
right to left |
negation, complement, increment, decrement |
|
* / % |
left to right |
multiplication, division, modulo |
|
+ - |
left to right |
addition, subtraction |
|
<< >> |
left to right |
left and right shift |
|
< <= > >= |
left to right |
relational operators |
|
== != |
left to right |
equal, unequal |
|
& |
left to right |
bitwise and |
|
^ |
left to right |
bitwise exclusive or |
|
| |
left to right |
bitwise or |
|
&& |
left to right |
logical and |
|
|| |
left to right |
logical or |
|
-> : |
right to left |
conditional expression operators |
|
= |
right to left |
assignment (lowest precedence) |