<html> <title>-</title><body BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#0000FF" VLINK="#330088" ALINK="#FF0044"><H1>Using SPIN</H1><DL><DD><I>Gerard J. Holzmann<br>gerard@plan9.bell-labs.com<br></I></DL><DL><DD><H4>ABSTRACT</H4>SPIN can be used for proving or disproving logical propertiesof concurrent systems.To render the proofs, a concurrent system is firstmodeled in a formal specification language called PROMELA.The language allows one to specify the behaviorsof asynchronously executingprocesses that may interact through synchronousor asynchronous message passing, or through directaccess to shared variables.<br> <br>System models specified in this way can be verifiedfor both safety and liveness properties. The specificationof general properties in linear time temporal logic isalso supported.<br> <br>The first part of this manualdiscusses the basic features of the specification language PROMELA.The second part describes the verifier SPIN.</DL><H4>1 The Language PROMELA</H4><br> <br>PROMELA is short for Protocol Meta Language [Ho91].PROMELA is a <I>modeling</I> language, not a programming language.A formal model differs in two essential ways from an implementation.First, a model is meant to be an abstraction of a designthat contains only those aspects of the design that aredirectly relevant to the properties one is interested in proving.Second, a formal model must contain things that are typically not partof an implementation, such as worst-case assumptions aboutthe behavior of the environment that may interact with thesystem being studied, and a formal statement of relevant correctnessproperties. It is possible to mechanically extract abstract modelsfrom implementation level code, as discussed, for instance in [HS99].<br> <br>Verification with SPIN is often performed in a series of steps,with the construction of increasingly detailed models.Each model can be verified under different types ofassumptions about the environment and for differenttypes of correctness properties.If a property is not valid for the given assumptions aboutsystem behavior, the verifier can produce a counter-examplethat demonstrates how the property may be violated.If a property is valid, it may be possible to simplify themodel based on that fact, and prove still other properties.<br> <br>Section 1.1 covers the basic building blocks of the language.Section 1.2 introduces the control flow structures.Section 1.3 explains how correctness properties are specified.Section 1.4 concludes the first part with a discussion ofspecial predefined variables and functions that can be used toexpress some correctness properties.<br> <br>Up to date manual pages for SPIN can always be found online at:http://cm.bell-labs.com/cm/cs/what/spin/Man/<H4>1.1 Basics</H4><br> <br>A PROMELA model can contain three different types of objects:<DL><DT><DT> <DD><DL><DD>* Processes (section 1.1.1),<br>* Variables (section 1.1.2),<br>* Message channels (section 1.1.3).</DL></dl><br> <br>All processes are global objects.For obvious reasons, a PROMELA model must contain at least oneprocess to be meaningful.Since SPIN is specifically meant to prove properties ofconcurrent systems, a model typically contains more thanone process.<br> <br>Message channels and variables, the two basic types of data objects,can be declared with either a global scope or a local scope.A data object with global scope can be referred to by all processes.A data object with a local scope can be referred to by just asingle process: the process that declares and instantiates the object.As usual, all objects must be declared in the specificationbefore they are referenced.<H4>1.1.1 Processes</H4><br> <br>Here is a simple process that does nothing except printa line of text:<DL><DT><DD><TT><PRE>init { printf("it works\n")}</PRE></TT></DL>There are a few things to note.<TT>Init</TT>is a predefined keyword from the language.It can be used to declare and instantiatea single initial process in the model.(It is comparable to the<TT>main</TT>procedure of a C program.)The<TT>init</TT>process does not take arguments, but it canstart up (instantiate) other processes that do.<TT>Printf</TT>is one of a few built-in procedures in the language.It behaves the same as the C version.Note, finally, that no semicolon follows the single<TT>printf</TT>statement in the above example.In PROMELA, semicolons are used as statement separators,not statement terminators. (The SPIN parser, however, islenient on this issue.)<br> <br>Any process can start new processes by using anotherbuilt-in procedure called<TT>run</TT>.For example,<DL><DT><DD><TT><PRE>proctype you_run(byte x){ printf("my x is: %d\n", x)}</PRE></TT></DL><DL><DT><DD><TT><PRE>init { run you_run(1); run you_run(2)}</PRE></TT></DL>The word<TT>proctype</TT>is again a keyword that introduces the declarationof a new type of process.In this case, we have named that type<TT>you_run</TT>and declared that all instantiations of processesof this type will take one argument: a data objectof type<TT>byte</TT>,that can be referred to within this process by the name<TT>x</TT>.Instances of a<TT>proctype</TT>can be created with the predefined procedure<TT>run</TT>,as shown in the example.When the<TT>run</TT>statement completes, a copy of the processhas been started, and all its arguments have beeninitialized with the arguments provided.The process may, but need not, have performedany statement executions at this point.It is now part of the concurrent system,and its execution can be interleaved arbitrarily withthose of the other, already executing processes.(More about the semantics of execution follows shortly.)<br> <br>In many cases, we are only interested in creating asingle instance of each process type that is declared,and the processes require no arguments.We can define this by prefixing the keyword<TT>proctype</TT>from the process declaration with another keyword:<TT>active</TT>.Instances of all active proctypes are created when thesystem itself is initialized.We could, for instance, have avoided the use of<TT>init</TT>by declaring the corresponding process in the last exampleas follows:<DL><DT><DD><TT><PRE>active proctype main() { run you_run(1); run you_run(2)}</PRE></TT></DL>Note that there are no parameters to instantiate in thiscase. Had they been declared, they would default to azero value, just like all other data objectsthat are not explicitly instantiated.<br> <br>Multiple copies of a process type can also be created inthis way. For example:<DL><DT><DD><TT><PRE>active [4] proctype try_me() { printf("hi, i am process %d\n", _pid)}</PRE></TT></DL>creates four processes.A predefined variable<TT>_pid</TT>is assigned to each running process, and holdsits unique process instantiation number.In some cases, this number is needed when a referencehas to be made to a specific process.<br> <br>Summarizing: process behavior is declared in<TT>proctype</TT>definitions, and it is instantiated with either<TT>run</TT>statements or with the prefix<TT>active</TT>.Within a proctype declaration, statements are separated(not terminated) by semicolons.As we shall see in examples that follow, instead of thesemicolon, one can also use the alternative separator<TT>-></TT>(arrow), wherever that may help to clarify the structureof a PROMELA model.<H4>Semantics of Execution</H4><br> <br>In PROMELA there is no difference between a condition orexpression and a statement.Fundamental to the semantics of the language is thenotion of the <I>executability</I> of statements.Statements are either executable or blocked.Executability is the basic means of enforcingsynchronization between the processes in a distributed system.A process can wait for an event to happen by waitingfor a statement to become executable.For instance, instead of writing a busy wait loop:<DL><DT><DD><TT><PRE>while (a != b) /* not valid Promela syntax */ skip; /* wait for a==b */...</PRE></TT></DL>we achieve the same effect in PROMELA with the statement<DL><DT><DD><TT><PRE>(a == b);...</PRE></TT></DL>Often we indicate that the continuation of an executionis conditional on the truth of some expression by usingthe alternate statement separator:<DL><DT><DD><TT><PRE>(a == b) -> ...</PRE></TT></DL>Assignments and<TT>printf</TT>statements are always executable in PROMELA.A condition, however, can only be executed (passed) when it holds.If the condition does not hold, execution blocks until it does.There are similar rules for determining the executabilityof all other primitive and compound statements in thelanguage.The semantics of each statement is defined in terms ofrules for executability and effect.The rules for executability set a precondition on the stateof the system in which a statement can be executed.The effect defines how a statement will alter asystem state when executed.<br> <br>PROMELA assumes that all individual statements are executedatomically: that is, they model the smallest meaningful entitiesof execution in the system being studied.This means that PROMELA defines the standard asynchronous interleavingmodel of execution, where a supposed scheduler is free ateach point in the execution to select any one of the processesto proceed by executing a single primitive statement.Synchronization constraints can be used to influence theinterleaving patterns. It is the purpose of a concurrent system'sdesign to constrain those patterns in such a way that nocorrectness requirements can be violated, and all servicerequirements are met. It is the purpose of the verifiereither to find counter-examples to a designer's claim that thisgoal has been met, or to demonstrate that the claim is indeed valid.<H4>1.1.2 Variables</H4><br> <br>The table summarizes the five basic data types used in PROMELA.<TT>Bit</TT>and<TT>bool</TT>are synonyms for a single bit of information.The first three types can store only unsigned quantities.The last two can hold either positive or negative values.The precise value ranges of variables of types<TT>short</TT>and<TT>int</TT>is implementation dependent, and correspondsto those of the same types in C programsthat are compiled for the same hardware.The values given in the table are most common.<br><img src="-.22361.gif"><br><br> <br>The following example program declares a array oftwo elements of type<TT>bool</TT>and a scalar variable<TT>turn</TT>of the same type.Note that the example relies on the fact that<TT>_pid</TT>is either 0 or 1 here.<DL><DT><DD><TT><PRE>/* * Peterson's algorithm for enforcing * mutual exclusion between two processes * competing for access to a critical section */bool turn, want[2]; active [2] proctype user(){again: want[_pid] = 1; turn = _pid; /* wait until this condition holds: */ (want[1 - _pid] == 0 || turn == 1 - _pid); /* enter */critical: skip; /* leave */ want[_pid] = 0; goto again}</PRE></TT></DL>In the above case, all variables are initialized to zero.The general syntax for declaring and instantiating avariable, respectively for scalar and array variables, is:<DL><DT><DD><TT><PRE>type name = expression;type name[constant] = expression</PRE></TT></DL>In the latter case, all elements of the array are initializedto the value of the expression.A missing initializer fields defaults to the value zero.As usual, multiple variables of the same type can be groupedbehind a single type name, as in:<DL><DT><DD><TT><PRE>byte a, b[3], c = 4</PRE></TT></DL>In this example, the variable<TT>c</TT>is initialized to the value 4; variable<TT>a</TT>and the elements of array<TT>b</TT>are all initialized to zero.<br> <br>Variables can also be declared as structures.For example:<DL><DT><DD><TT><PRE>typedef Field { short f = 3; byte g}; typedef Msg { byte a[3]; int fld1; Field fld2; chan p[3]; bit b}; Msg foo;</PRE></TT></DL>introduces two user-defined data types, the first named<TT>Field</TT>and the second named<TT>Msg</TT>.A single variable named<TT>foo</TT>of type<TT>Msg</TT>is declared.All fields of<TT>foo</TT>that are not explicitly initialized (in the example, all fields except<TT>foo.fld2.f</TT>)are initialized to zero.References to the elements of a structure are written as:<DL><DT><DD><TT><PRE>foo.a[2] = foo.fld2.f + 12</PRE></TT></DL>A variable of a user-defined type can be passed as a singleargument to a new process in<TT>run</TT>statements.For instance,<DL><DT><DD><TT><PRE>proctype me(Msg z) { z.a[2] = 12}init { Msg foo; run me(foo)}</PRE></TT></DL><br> <br>Note that even though PROMELA supports only one-dimensional arrays,a two-dimensional array can be created indirectly with user-definedstructures, for instance as follows:<DL><DT><DD><TT><PRE>typedef Array { byte el[4]}; Array a[4];</PRE></TT></DL>This creates a data structure of 16 elements that can bereferenced, for instance, as<TT>a[i].el[j]</TT>.<br> <br>As in C, the indices of an array of<TT>N</TT>elements range from 0 to<TT>N-1</TT>.<H4>Expressions</H4><br> <br>Expressions must be side-effect free in PROMELA.Specifically, this means that an expression cannotcontain assignments, or send and receive operations (see section 1.1.3).<DL><DT><DD><TT><PRE>c = c + 1; c = c - 1</PRE></TT></DL>and<DL><DT><DD><TT><PRE>c++; c--</PRE></TT></DL>are assignments in PROMELA, with the same effects.But, unlike in C,<DL><DT><DD><TT><PRE>b = c++</PRE></TT></DL>is not a valid assignment, because the right-hand sideoperand is not a valid expression in PROMELA (it is not side-effect free).<br> <br>It is also possible to write a side-effect free conditionalexpression, with the following syntax:<DL><DT><DD><TT><PRE>(expr1 -> expr2 : expr3)</PRE></TT></DL>The parentheses around the conditional expression are required toavoid misinterpretation of the arrow.The example expression has the value of <TT>expr2</TT> when <TT>expr1</TT>evaluates to a non-zero value, and the value of <TT>expr3</TT> otherwise.<br> <br>In assignments like<DL><DT><DD><TT><PRE>variable = expression</PRE></TT></DL>the values of all operands used inside the expression are first cast tosigned integers before the operands are applied.After the evaluation of the expression completes, the value producedis cast to the type of the target variable before the assignment takes place.<H4>1.1.3 Message Channels</H4><br> <br>Message channels are used to model the transfer of databetween processes.They are declared either locally or globally,for instance as follows:<DL><DT><DD><TT><PRE>chan qname = [16] of { short, byte }</PRE></TT></DL>The keyword<TT>chan</TT>introduces a channel declaration.In this case, the channel is named<TT>qname</TT>,and it is declared to be capable of storing upto 16 messages.Each message stored in the channel is declared here toconsist of two fields: one of type<TT>short</TT>and one of type<TT>byte</TT>.The fields of a message can be any one of the basic types<TT>bit</TT>,<TT>bool</TT>,<TT>byte</TT>,<TT>short</TT>,<TT>int</TT>,and<TT>chan</TT>,Lines 1–500 of 2490. Load more
<html> <title> - </title> <body BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#0000FF" VLINK="#330088" ALINK="#FF0044"> <H1>Using SPIN </H1> <DL><DD><I>Gerard J. Holzmann<br> gerard@plan9.bell-labs.com<br> </I></DL> <DL><DD><H4>ABSTRACT</H4> SPIN can be used for proving or disproving logical properties of concurrent systems. To render the proofs, a concurrent system is first modeled in a formal specification language called PROMELA. The language allows one to specify the behaviors of asynchronously executing processes that may interact through synchronous or asynchronous message passing, or through direct access to shared variables. <br> <br> System models specified in this way can be verified for both safety and liveness properties. The specification of general properties in linear time temporal logic is also supported. <br> <br> The first part of this manual discusses the basic features of the specification language PROMELA. The second part describes the verifier SPIN. </DL> <H4>1 The Language PROMELA </H4> <br> <br> PROMELA is short for Protocol Meta Language [Ho91]. PROMELA is a <I>modeling</I> language, not a programming language. A formal model differs in two essential ways from an implementation. First, a model is meant to be an abstraction of a design that contains only those aspects of the design that are directly relevant to the properties one is interested in proving. Second, a formal model must contain things that are typically not part of an implementation, such as worst-case assumptions about the behavior of the environment that may interact with the system being studied, and a formal statement of relevant correctness properties. It is possible to mechanically extract abstract models from implementation level code, as discussed, for instance in [HS99]. <br> <br> Verification with SPIN is often performed in a series of steps, with the construction of increasingly detailed models. Each model can be verified under different types of assumptions about the environment and for different types of correctness properties. If a property is not valid for the given assumptions about system behavior, the verifier can produce a counter-example that demonstrates how the property may be violated. If a property is valid, it may be possible to simplify the model based on that fact, and prove still other properties. <br> <br> Section 1.1 covers the basic building blocks of the language. Section 1.2 introduces the control flow structures. Section 1.3 explains how correctness properties are specified. Section 1.4 concludes the first part with a discussion of special predefined variables and functions that can be used to express some correctness properties. <br> <br> Up to date manual pages for SPIN can always be found online at: http://cm.bell-labs.com/cm/cs/what/spin/Man/ <H4>1.1 Basics </H4> <br> <br> A PROMELA model can contain three different types of objects: <DL> <DT><DT> <DD> <DL><DD> * Processes (section 1.1.1), <br> * Variables (section 1.1.2), <br> * Message channels (section 1.1.3). </DL> </dl> <br> <br> All processes are global objects. For obvious reasons, a PROMELA model must contain at least one process to be meaningful. Since SPIN is specifically meant to prove properties of concurrent systems, a model typically contains more than one process. <br> <br> Message channels and variables, the two basic types of data objects, can be declared with either a global scope or a local scope. A data object with global scope can be referred to by all processes. A data object with a local scope can be referred to by just a single process: the process that declares and instantiates the object. As usual, all objects must be declared in the specification before they are referenced. <H4>1.1.1 Processes </H4> <br> <br> Here is a simple process that does nothing except print a line of text: <DL><DT><DD><TT><PRE> init { printf("it works\n") } </PRE></TT></DL> There are a few things to note. <TT>Init</TT> is a predefined keyword from the language. It can be used to declare and instantiate a single initial process in the model. (It is comparable to the <TT>main</TT> procedure of a C program.) The <TT>init</TT> process does not take arguments, but it can start up (instantiate) other processes that do. <TT>Printf</TT> is one of a few built-in procedures in the language. It behaves the same as the C version. Note, finally, that no semicolon follows the single <TT>printf</TT> statement in the above example. In PROMELA, semicolons are used as statement separators, not statement terminators. (The SPIN parser, however, is lenient on this issue.) <br> <br> Any process can start new processes by using another built-in procedure called <TT>run</TT>. For example, <DL><DT><DD><TT><PRE> proctype you_run(byte x) { printf("my x is: %d\n", x) } </PRE></TT></DL> <DL><DT><DD><TT><PRE> init { run you_run(1); run you_run(2) } </PRE></TT></DL> The word <TT>proctype</TT> is again a keyword that introduces the declaration of a new type of process. In this case, we have named that type <TT>you_run</TT> and declared that all instantiations of processes of this type will take one argument: a data object of type <TT>byte</TT>, that can be referred to within this process by the name <TT>x</TT>. Instances of a <TT>proctype</TT> can be created with the predefined procedure <TT>run</TT>, as shown in the example. When the <TT>run</TT> statement completes, a copy of the process has been started, and all its arguments have been initialized with the arguments provided. The process may, but need not, have performed any statement executions at this point. It is now part of the concurrent system, and its execution can be interleaved arbitrarily with those of the other, already executing processes. (More about the semantics of execution follows shortly.) <br> <br> In many cases, we are only interested in creating a single instance of each process type that is declared, and the processes require no arguments. We can define this by prefixing the keyword <TT>proctype</TT> from the process declaration with another keyword: <TT>active</TT>. Instances of all active proctypes are created when the system itself is initialized. We could, for instance, have avoided the use of <TT>init</TT> by declaring the corresponding process in the last example as follows: <DL><DT><DD><TT><PRE> active proctype main() { run you_run(1); run you_run(2) } </PRE></TT></DL> Note that there are no parameters to instantiate in this case. Had they been declared, they would default to a zero value, just like all other data objects that are not explicitly instantiated. <br> <br> Multiple copies of a process type can also be created in this way. For example: <DL><DT><DD><TT><PRE> active [4] proctype try_me() { printf("hi, i am process %d\n", _pid) } </PRE></TT></DL> creates four processes. A predefined variable <TT>_pid</TT> is assigned to each running process, and holds its unique process instantiation number. In some cases, this number is needed when a reference has to be made to a specific process. <br> <br> Summarizing: process behavior is declared in <TT>proctype</TT> definitions, and it is instantiated with either <TT>run</TT> statements or with the prefix <TT>active</TT>. Within a proctype declaration, statements are separated (not terminated) by semicolons. As we shall see in examples that follow, instead of the semicolon, one can also use the alternative separator <TT>-></TT> (arrow), wherever that may help to clarify the structure of a PROMELA model. <H4>Semantics of Execution </H4> <br> <br> In PROMELA there is no difference between a condition or expression and a statement. Fundamental to the semantics of the language is the notion of the <I>executability</I> of statements. Statements are either executable or blocked. Executability is the basic means of enforcing synchronization between the processes in a distributed system. A process can wait for an event to happen by waiting for a statement to become executable. For instance, instead of writing a busy wait loop: <DL><DT><DD><TT><PRE> while (a != b) /* not valid Promela syntax */ skip; /* wait for a==b */ ... </PRE></TT></DL> we achieve the same effect in PROMELA with the statement <DL><DT><DD><TT><PRE> (a == b); ... </PRE></TT></DL> Often we indicate that the continuation of an execution is conditional on the truth of some expression by using the alternate statement separator: <DL><DT><DD><TT><PRE> (a == b) -> ... </PRE></TT></DL> Assignments and <TT>printf</TT> statements are always executable in PROMELA. A condition, however, can only be executed (passed) when it holds. If the condition does not hold, execution blocks until it does. There are similar rules for determining the executability of all other primitive and compound statements in the language. The semantics of each statement is defined in terms of rules for executability and effect. The rules for executability set a precondition on the state of the system in which a statement can be executed. The effect defines how a statement will alter a system state when executed. <br> <br> PROMELA assumes that all individual statements are executed atomically: that is, they model the smallest meaningful entities of execution in the system being studied. This means that PROMELA defines the standard asynchronous interleaving model of execution, where a supposed scheduler is free at each point in the execution to select any one of the processes to proceed by executing a single primitive statement. Synchronization constraints can be used to influence the interleaving patterns. It is the purpose of a concurrent system's design to constrain those patterns in such a way that no correctness requirements can be violated, and all service requirements are met. It is the purpose of the verifier either to find counter-examples to a designer's claim that this goal has been met, or to demonstrate that the claim is indeed valid. <H4>1.1.2 Variables </H4> <br> <br> The table summarizes the five basic data types used in PROMELA. <TT>Bit</TT> and <TT>bool</TT> are synonyms for a single bit of information. The first three types can store only unsigned quantities. The last two can hold either positive or negative values. The precise value ranges of variables of types <TT>short</TT> and <TT>int</TT> is implementation dependent, and corresponds to those of the same types in C programs that are compiled for the same hardware. The values given in the table are most common. <br><img src="-.22361.gif"><br> <br> <br> The following example program declares a array of two elements of type <TT>bool</TT> and a scalar variable <TT>turn</TT> of the same type. Note that the example relies on the fact that <TT>_pid</TT> is either 0 or 1 here. <DL><DT><DD><TT><PRE> /* * Peterson's algorithm for enforcing * mutual exclusion between two processes * competing for access to a critical section */ bool turn, want[2]; active [2] proctype user() { again: want[_pid] = 1; turn = _pid; /* wait until this condition holds: */ (want[1 - _pid] == 0 || turn == 1 - _pid); /* enter */ critical: skip; /* leave */ want[_pid] = 0; goto again } </PRE></TT></DL> In the above case, all variables are initialized to zero. The general syntax for declaring and instantiating a variable, respectively for scalar and array variables, is: <DL><DT><DD><TT><PRE> type name = expression; type name[constant] = expression </PRE></TT></DL> In the latter case, all elements of the array are initialized to the value of the expression. A missing initializer fields defaults to the value zero. As usual, multiple variables of the same type can be grouped behind a single type name, as in: <DL><DT><DD><TT><PRE> byte a, b[3], c = 4 </PRE></TT></DL> In this example, the variable <TT>c</TT> is initialized to the value 4; variable <TT>a</TT> and the elements of array <TT>b</TT> are all initialized to zero. <br> <br> Variables can also be declared as structures. For example: <DL><DT><DD><TT><PRE> typedef Field { short f = 3; byte g }; typedef Msg { byte a[3]; int fld1; Field fld2; chan p[3]; bit b }; Msg foo; </PRE></TT></DL> introduces two user-defined data types, the first named <TT>Field</TT> and the second named <TT>Msg</TT>. A single variable named <TT>foo</TT> of type <TT>Msg</TT> is declared. All fields of <TT>foo</TT> that are not explicitly initialized (in the example, all fields except <TT>foo.fld2.f</TT>) are initialized to zero. References to the elements of a structure are written as: <DL><DT><DD><TT><PRE> foo.a[2] = foo.fld2.f + 12 </PRE></TT></DL> A variable of a user-defined type can be passed as a single argument to a new process in <TT>run</TT> statements. For instance, <DL><DT><DD><TT><PRE> proctype me(Msg z) { z.a[2] = 12 } init { Msg foo; run me(foo) } </PRE></TT></DL> <br> <br> Note that even though PROMELA supports only one-dimensional arrays, a two-dimensional array can be created indirectly with user-defined structures, for instance as follows: <DL><DT><DD><TT><PRE> typedef Array { byte el[4] }; Array a[4]; </PRE></TT></DL> This creates a data structure of 16 elements that can be referenced, for instance, as <TT>a[i].el[j]</TT>. <br> <br> As in C, the indices of an array of <TT>N</TT> elements range from 0 to <TT>N-1</TT>. <H4>Expressions </H4> <br> <br> Expressions must be side-effect free in PROMELA. Specifically, this means that an expression cannot contain assignments, or send and receive operations (see section 1.1.3). <DL><DT><DD><TT><PRE> c = c + 1; c = c - 1 </PRE></TT></DL> and <DL><DT><DD><TT><PRE> c++; c-- </PRE></TT></DL> are assignments in PROMELA, with the same effects. But, unlike in C, <DL><DT><DD><TT><PRE> b = c++ </PRE></TT></DL> is not a valid assignment, because the right-hand side operand is not a valid expression in PROMELA (it is not side-effect free). <br> <br> It is also possible to write a side-effect free conditional expression, with the following syntax: <DL><DT><DD><TT><PRE> (expr1 -> expr2 : expr3) </PRE></TT></DL> The parentheses around the conditional expression are required to avoid misinterpretation of the arrow. The example expression has the value of <TT>expr2</TT> when <TT>expr1</TT> evaluates to a non-zero value, and the value of <TT>expr3</TT> otherwise. <br> <br> In assignments like <DL><DT><DD><TT><PRE> variable = expression </PRE></TT></DL> the values of all operands used inside the expression are first cast to signed integers before the operands are applied. After the evaluation of the expression completes, the value produced is cast to the type of the target variable before the assignment takes place. <H4>1.1.3 Message Channels </H4> <br> <br> Message channels are used to model the transfer of data between processes. They are declared either locally or globally, for instance as follows: <DL><DT><DD><TT><PRE> chan qname = [16] of { short, byte } </PRE></TT></DL> The keyword <TT>chan</TT> introduces a channel declaration. In this case, the channel is named <TT>qname</TT>, and it is declared to be capable of storing up to 16 messages. Each message stored in the channel is declared here to consist of two fields: one of type <TT>short</TT> and one of type <TT>byte</TT>. The fields of a message can be any one of the basic types <TT>bit</TT>, <TT>bool</TT>, <TT>byte</TT>, <TT>short</TT>, <TT>int</TT>, and <TT>chan</TT>,