Go up to A.3 The Protocol Go forward to Send Actions

Initialization Actions

When starting execution, the application program first makes sure that the scheduler understands the same version of the protocol. This is achieved by writing the version string to the output channel, receiving a corresponding string from the input channel and comparing both. If they do not match, execution is aborted. Otherwise, the range of task identifiers that may be used for the naming of new tasks is received and stored.

initialize(C) ==

\/

• (send version)

  /\

  • T = null
  • write(version)
  • T' = receiveVersion

• exists v: String

  /\

  • T = receiveVersion
  • read(v)

  • \/

    • (v = version /\ T' = receiveTaskId)
    • (v != version /\ S' = terminate)

• (receive task identifier)

  /\

  • T = receiveTaskId
  • exists message: Message

    /\

    • receive(message, 2)
    • message.key = taskid
    • taskMin' = message.body(0)
    • taskMax' = message.body(1)
    • taskId' = taskMin

  • T' = null
  • S' = C