6.1 输出迹

    宏[DUMP(msg)]用来在文件中记录消息msg，一直到执行结束为止(或者自动，或者由调试器手动控制)。每条消息包括三个部分：时间tuple(t, s)，有着惟一ID的发送者或接收者，和消息体。下面是从输出中截取的一部分内容：

    . . . . . .

    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

    . . . . . .

    管理器产生输出，它可以访问通信过程中的所有信息。ID为0的客户在时刻10.5发送了一条消息。根据协议，1号聊天室在一秒钟后把该消息广播出去。另一个连接在1号聊天室的客户1在同一时刻收到消息。这里也可以看出消息的最初发送者。

    6.2 与时序图的一致性

    与时序图的一致性可以通过一套基于规则的方法检查。这些规则在文本文件中定义。检查程序读取文件，检查输出迹是否可以满足所有的规则。正则表达式被扩展之后用以描述规则。规则由四部分组成：前置条件、后置条件、监视哨(任选)和计数规则属性(任选)。前置条件是正则表达式，用来匹配部分输出迹。它与监视哨(一个布尔表达式)结合，定义何时可以使用规则。当规则可用，并且计数规则属性为false时，后置条件(另一个正则表达式)必须要在输出迹中找到;如果计数规则属性为true，后置条件一定不可满足。

    例如，下面的规则就说明了消息的发送者并没有在一秒钟后收到广播。

    前置条件

    CLOCK: \((\d+\.{0,1}\d*)s,(\d+\.{0,1}\d*)\)\n\Client (\d+)\nSays "(.*?)" to ChatRoom (\d+)\n

    后置条件

    CLOCK: \([(\1+1)]s,(\d+\.{0,1}\d*)\)\nClient [(\3)]\n Receives"[(\4)]" from Client [(\3)]\n

    监视哨

    [(\1+1)]<50

    计数规则

    True

    在前置条件中，在括号中定义了五个表达式分组。分别编号从1到5。组1匹配浮点时间。组2匹配序号。它们组成时间元组。组3匹配以整数标记的发送者的客户ID。组4匹配消息，它可以是任意的字符串。组5匹配发送者所在的聊天室。

    在后置条件中，[(…)]包含一个表达式，分组值可以在 “\”后使用索引号来引用。这样，[(\1+1)]是第一个组的值加一。[(\3)]等于组3。关于正则表达式的更多内容可以在[5]中找到。

    假定执行过程停止在仿真时刻50那里，检查就不应该超过时刻50。在没有额外条件的情况下，如果在时刻49.5一条消息发送到聊天室，检查程序会希望在时刻50.5时见到相应的广播。为了实现这项功能，引入了一个监视哨[(\1+1)]<50。它会告知检查程序这条规则仅在分组1的值加一小于50时可用。

    客户不应该接收到它自己的消息，这就是一条计数规则。