7.1 Simulation Trace

A simulation trace records the evolution of the state (and possibly, the messages being sent) over time. In SVM it is obtained as text output of a simulation. This output is sent by the model with the DUMP macro. Different models may have different output formats. However, if the models conform to a single standard and provide enough information in the output, the output trace is useful to check the correctness of those models.

An example of chat rooms and clients is introduced in [40]. Chat rooms and clients are the two different types of DCharts components. The communication between them conforms to the following simplified protocol:

• There are 5 clients and 2 chat rooms in the system. Initially, the clients are not connected. They try to connect to a random chat room every 1 to 3 seconds (uniformly distributed). The requested chat room instantaneously receives the request (zero network delay and reliable communication are assumed).

• A chat room accepts at most 3 clients. It accepts a connection request if and only if its capacity is not exceeded.

• The requesting client receives an acceptance or rejection notice from the requested server immediately.

• A client must be accepted by a chat room before it may send chat messages.

• When connected, a client sends random messages to the chat room that it is connected to every 1 to 5 seconds (uniformly distributed). The chat room immediately receives the messages. It takes 1 second to process a message and broadcast it to all the clients connected to it, except the sender.

• The clients instantaneously receive the broadcast.

The following is a part of the output trace generated by a simulation of the whole system with 2 chat rooms and 5 clients:

......
CLOCK: (10.5s,0)
Client 0
Says "Hello!" to ChatRoom 1
......
CLOCK: (11.5s,0)
ChatRoom 1
Broadcasts "Hello!" to all clients except Client 0
......
CLOCK: (11.5s,2)
Client 1
Receives "Hello!" from Client 0
......

For more insight into this example, the readers are referred to the paper published at the UML 2003 conference [40]. This example is cited here only to demonstrate model verification. This output trace consists of a number of output segments, each of which is composed of three lines: the time when the output is produced, the component that produces the output and a brief message from the component.

The time is written in an enhanced format. A time tuple consists of a float number that denotes the number of seconds elapsed since the simulation was started, and an integer that denotes the sequence of the multiple events received at that time. For example, time (10.5s,0) means 10.5 seconds have elapsed since the simulation is started and the event is the first ($0+1$) to occur at that time. Time (11.5s,2) means 11.5 seconds after the simulation is started and that the event is the third ($2+1$) to occur at that time.

This extended time format allows the specification of multiple events that occur at exactly the same time, while their order is still important. For example, according to the protocol, as soon as the server broadcasts a message, the clients receive it. The two events occur at exactly the same time, but in the output trace, the message sent from the chat room must appear before the message received by the clients (a causality constraint).