- 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
Inline Definitions
Some motivation for and examples of the use of PROMELA inline’s was already given in the last chapter. The PROMELA inline is meant to provide some of the structuring mechanism of a traditional procedure call, without introducing any overhead during the verification process. The PROMELA parser replaces each point of invocation of an inline with the text of the inline body. If any parameters are used, their actual values from the call will textually replace the formal place holders that are used inside the definition of the inline body. That is, there is no concept of value passing with inline’s. The parameter names used inside the definition are mere stand ins for the names provided at the place of call. A small example can clarify the working and intent of this mechanism, as follows:
inline example(x, y) {
y = a;
x = b;
assert(x)
}
init {
int a, b;
example(a,b)
}
In this example we have defined an inline named example and we gave it two parameters. The parameters do not have a type associated with them. They could in fact be replaced in a call with variables of any type that matches the use of the names inside the inline body.
At the point of invocation the names of two variables are provided as actual parameters. The parser treats this code as if we had written the following specification instead:
init {
int a, b;
b = a;
a = b;
assert(a)
}
This version of the model is obtained by inserting the body of the inline at the point of call, while textually replacing every occurrence of the name x with the name a and every occurrence of y with b, as stipulated by the parameter list at the point of invocation.
We could have achieved the same effect by defining a C-style macro, as follows:
#define example(x, y) y = a; x = b; assert(x)
init {
int a, b;
example(a,b)
}
For a small inline function the difference is not that remarkable, but for larger pieces of code the macro method can quickly become unwieldy. There is one other benefit to the use of an inline compared to a macro definition. When we simulate (or verify) the version of the example using the inline definition of example, we see the following output:
$ spin inline.pml spin: line 4 "inline", Error: assertion violated spin: text of failed assertion: assert(a) #processes: 1 3: proc 0 (:init:) line 4 "inline" (state 3) 1 process created
Not surprisingly, the assertion is violated. The line number pointed at by SPIN is the location of the assert statement inside the inline body, as one would expect. If, however, we try to do the same with the version using a macro, we see this result:
$ spin macro.pml spin: line 9 "macro", Error: assertion violated spin: text of failed assertion: assert(a) #processes: 1 3: proc 0 (:init:) line 9 "macro" (state 3) 1 process created
The same assertion violation is reported, but the line number reference now gives the point of invocation of the macro, rather than the location of the failing assertion. Finding the source of an error by searching through possibly complex macro definitions can be challenging, which makes the use of PROMELA inlines preferable in most cases.
To help find out what really happens with parameter substitution in inline functions and preprocessing macros, option -I causes SPIN to generate a version of the source text that shows the result of all macro-processing and inlining on proctype bodies. It can be an invaluable source of information in determining the cause of subtle problems with preprocessing. The two versions of our sample program, the first using an inline definition and the second using a macro, produce the following results:
$ spin -I inline.pml
proctype :init:()
{
{
b = a;
a = b;
assert(a);
};
}
$ spin -I macro.pml
proctype :init:()
{
b = a;
a = b;
assert(a);
}
Note that the version of the model that is generated with the -I option is not itself a complete model. No variable declarations are included, and some of the names used for proctypes and labels are the internally assigned names used by SPIN (using, for instance, :init: instead of init). The proctype body text, though, shows the result of all preprocessing.
There is not much difference in the output for the two versions, except that the use of the inline function creates a non-atomic sequence (the part enclosed in curly braces), where the macro definition does not. There is no difference in behavior.
When using inline definitions, it is good to keep the scope rules of PROMELA in mind. Because PROMELA only knows two levels of scope for variables, global and process local, there is no subscope for inline bodies. This means that an attempt to declare a local scratch variable, such as this:
inline thisworks(x) {
int y;
y = x;
printf("%d\n", y)
}
init {
int a;
a = 34;
thisworks(a)
}
produces the following, after inlining is performed:
init {
int a;
a = 34;
int y;
y = a;
printf("%d\n", y) }
This works because variable declarations can appear anywhere in a PROMELA model, with their scope extending from the point of declaration to the closing curly brace of the surrounding proctype or init body. This means that the variable y remains in scope, also after the point of invocation of the inline. It would therefore be valid, though certainly confusing, to write
inline thisworks2(x) {
int y;
y = x;
printf("%d\n", y)
}
init {
int a;
a = 34;
thisworks(a);
y = 0
}
that is, to access the variable y outside the inline body in which it was declared.