Go backward to Message: Channel Messages Go up to 5.1 Types

GlobalAssertion: Network Conditions

abstract class GlobalAssertion
{
  abstract boolean assert(Program program[])
  String getText()
  static Message[] getMessages(InChannel c)
  static Message[] getMessages(OutChannel c)
}

An object a of this type is passed to an assert call. The function a.assert(p) is then invoked on the array p of programs associated to the nodes of the network (in the order in which the nodes were created). If this function returns false, execution is aborted with the error message returned by a.getText(); otherwise execution is continued.

When a.assert(p) is called, it can rely on the fact that each program p[i] is either in the initial state, has terminated execution, is blocked on a communication operation before the corresponding message was sent respectively received, or has explicitly interrupted execution by a call of yield.

ms = getMessages(c)
  Message[] ms
  InChannel c
ms = getMessages(c)
  Message[] ms
  OutChannel c

This function may be used by an assertion to determine the contents of a channel c. Its return value is the array of messages contained in c in the order in which they were sent.