Promela |
Extension |
c_decl |
NAME
c_decl , c_state , c_track -
embedded C data declarations.
SYNTAX
c_decl { /* c declaration */ }
c_state string string [ string ]
c_track string string [ string ]
EXECUTABILITY
true
DESCRIPTION
The primitives
c_decl , c_state , and
c_track are global primitives that can only appear in a model as
global declarations outside all
proctype declarations.
The c_decl primitive provides a capability to embed general C data type declarations into a model. These type declarations are placed in the generated pan.h file before the declaration of the state-vector structure, which is also included in that file. This means that the data types introduced in a c_decl primitive can be referenced anywhere in the generated code, including inside the state vector with the help of c_state primitives. Data type declarations can also be introduced in global c_code fragments, but in this case the generated code is placed in the pan.c file, and therefore appears necessarily after the declaration of the state-vector structure. Therefore, these declarations cannot be used inside the state vector.
The c_state keyword is followed by either two or three quoted strings. The first argument specifies the type and the name of a data object. The second argument the scope of that object. A third argument can optionally be used to specify an initial value for the data object. (It is best not to assume a known default initial value for objects that are declared in this way.)
There are three possible scopes: global, local, or hidden. A global scope is indicated by the use of the quoted string "Global." If local, the name Local must be followed by the name of the proctype in which the declaration is to appear, as in "Local ex2." If the quoted string "Hidden" is used for the second argument, the data object will be declared as a global object that remains outside the state vector.
The primitive c_track is a global primitive that can declare any state object, or more generally any piece of memory, as holding state information. This primitive takes two string arguments. The first argument specifies an address, typically a pointer to a data object declared elsewhere. The second argument gives the size in bytes of that object, or more generally the number of bytes starting at the address that must be tracked as part of the system state.
EXAMPLES
The first example illustrates how
c_decl , c_code and
c_state declarations
can be used to define either visible or hidden state variables, referring to
type definitions that must precede the internal Spin state-vector declaration.
For an explanation of the rules for prefixing global and local variables
inside
c_code and
c_expr statements, see the manual pages for these two statements.
c_decl { typedef struct Proc { int rlock; int state; struct Rendez *r; } Proc; typedef struct Rendez { int lck; int cond; Proc *p; } Rendez; } c_code { Proc H1; Proc *up0 = &H1; Rendez RR; }
/* * The following two c_state declarations presume type * Rendez known the first enters R1 into state vector * as a global variable, and the second enters R2 into * proctype structure as local variable. */ c_state "Rendez R1" "Global" c_state "Rendez R2" "Local ex2" "now.R1"
/* * The next two c_state declarations are kept outside * the state vector. They define H1 and up0 as global * objects, which are declared elsewhere. */ c_state "extern Proc H1" "Hidden" c_state "extern Proc *up0" "Hidden"
/* * The following declaration defines that RR is to be * treated as a state variable -- no matter how it was * declared; it can be an arbitrary external variable. */ c_decl { \#include "types.h" /* declare type Rendez */ /* not needed if the explicit c_decl from before is used */ } c_track "&RR" "sizeof(Rendez)"
active proctype ex2() { c_code { now.R1.cond = 1; }; /* global */ c_code { Pex2->R2.lck = 0; }; /* local */ c_code { H1.rlock = up0->state; }; /* C */ printf("This is Spin Version 4.0\n") }The c_track statement can have a third argument that must be one of the words: "UnMatched" or "StackOnly" in double quotes. For instance
c_track "&cnt" "sizeof(int)" "UnMatched"Without the third argument, the default behavior for c_track is equivalent to "Matched".
If "UnMatched" or "StackOnly" is present, it means that the data object is tracked on the stack, but its value is not considered to be part of the system state. So, the concrete value is accurately maintained during the depth-first search, while separately an abstract version of the same value can be stored in the statespace, as explained in this paper on Model Driven Software Verification.
NOTES
Spin instruments the code of the verifier to copy all data pointed to via
c_track primitives into and out of the state vector on forward and backward moves
during the depth-first search that it performs.
Where there is a choice, the use of
c_state primitives will always result in more efficiently executed code,
since Spin can instrument the generated verifier to directly embed
data objects into the state vector itself, avoiding the copying process.
To get a better feeling for how precisely these primitives are interpreted by Spin, consider generating code from the last example, and look in the generated files pan.h and pan.c for all appearances of variables R1 , R2 , P1 , and up0 .
Avoid using type-names that clash with internal types used within the Spin-generated verifiers. This includes names such as State , P0 , P1 , etc., and Q0 , Q1 , etc. Name clashes caused by unfortunate choices of type names are reliably caught by the C compiler when the verification code is compiled.
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 22 November 2017) |