NAME
trace - for defining valid event sequences.

SYNTAX
trace { sequence }

DESCRIPTION
As with never claim declarations, a trace declaration does not specify new behavior, but instead states a correctness requirement on existing behavior in the remainder of the system. All channel names referenced in a trace declaration must be to globally declared message channels, and all message fields must be globally known (possibly symbolic) constants, or the predefined global variable _ . A trace declaration can be one of the modules of a Promela specification, i.e., it's structure and place within a Promela model is similar to that of an init , or never claim declaration.

An event trace declaration defines a correctness claim with the following properties.

• Each channel name that is used in an event trace declaration is monitored for compliance with the structure and context of the trace declaration.
• If only send operations on a channel appear in the trace, then only send operations on that channel are subject to the check. Similarly for receive operations. If both types appear, both are subject to the check, and they must occur in the relative order that the trace declaration gives.
• An event trace declaration may contain only send and receive operations (i.e., events), but it can contain any control flow construct. This means that no global or local variables can be declared or referred to. This excludes the use of assignments and conditions. Send and receive operations are restricted to simple sends or receives; they cannot be variations such as random receive, sorted send, receive test, etc.
• Message fields that must be matched in sends or receives must be specified either with the help of symbolic mtype names, or with constants. Message fields that have don't care values can be matched with the predefined write-only variable _ (see _(5)).
• Sends and receives that appear in an event trace are called monitored events . These events do not generate new behavior, but they are required to match send or receive events on the same channels in the model, with matching message parameters. A send or receive event occurs whenever a send or a receive statement is executed, i.e., an event occurs during a state transition.
• An event trace can capture the occurrence of receive events on rendezvous channels.
• An event trace causes a correctness violation if a send or receive action is executed in the system that is within the scope of the event trace, but that cannot be matched by a monitored event within that declaration.
• One can use accept , progress , and end -state labels in event trace declarations, with the usual interpretation.

Event traces must be deterministic (we may relax this restriction in furture releases.)

EXAMPLES
An event trace declaration that specifies the correctness requirement that send operations on channel q1 alternate with receive operations on channel q2 , and furthermore that all send operations on q1 are (claimed to be) exclusively messages with value a , and all receive operations on channel q2 are exclusively messages with value b , is written as follows:

trace {

        do

        :: q1!a; q2?b

        od

}