Go backward to Initialization Actions Go up to A.3 The Protocol Go forward to Receive Actions

Send Actions

When a new task is created, the task is assigned the next identifier in the task range.

sendTask(C) ==

• exists message: Message

  /\

  • send(message, 2)
  • message.key = task
  • message.body[0] = taskId
  • exists exp: Expression
    • message.body[1] = exp
  • taskId < taskMax
  • taskId' = taskId+1

• S' = C

When a "wait" request is issued, a message is sent that contains the identifier of the corresponding task.

sendWait(C) ==

/\

• exists message: Message

  /\

  • send(message, 1)
  • message.key = wait
  • exists taskid: TaskId
    • message.body[0] = taskid
  • waitStack[waitDepth] = message
  • waitDepth' = waitDepth+1
  • S' = C

• S' = C

An "nwait" request contains a list of task identifiers; we request the result of any of these tasks.

sendNWait(C) ==

/\

• exists message: Message, n: Natural

  /\

  • send(message, n+1)
  • message.key = nwait
  • message.body[0] = n
  • forall i: 1 <=i <=n
    • exists taskid: TaskId
      • message.body[i] = taskid
  • waitStack[waitDepth] = message
  • waitDepth' = waitDepth+1

• S' = C

An "all" message asks for the evaluation of a command on each application program.

sendAll(C) ==

/\

• exists message: Message

  /\

  • send(message, 1)
  • message.key = all
  • exists command: Command
    • message.body[0] = command

• S' = C

A "quit" message asks for the termination of the session and waits for a corresponding acknowledgement.

sendQuit(C) ==

\/

• (send quit request)

  /\

  • T = null
  • exists message: Message, code: Integer

    /\

    • send(message, 1)
    • message.key = quit
    • message.body[0] = code

  • T' = receiveAck

• (receive acknowledgement)

  /\

  • T = receiveAck
  • exists message: Message, code: Integer

    /\

    • receive(message, 1)
    • message.key = quit
    • message.body[0] = code

  • T' = null
  • S' = C

An "abort" message aborts the session immediately.

sendAbort(C) ==

/\

• exists message: Message

  /\

  • send(message, 1)
  • message.key = abort

• S' = C

A start message asks for the connection of a new node to the session; we receive either an okay or an error message as an acknowledgement.

sendStart(C) ==

\/

• (send start request)

  /\

  • T = null
  • exists message: Message

    /\

    • send(message, 2)
    • message.key = start

  • T' = receiveAck

• (receive acknowledgement)

  /\

  • T = receiveAck

  • \/

    • (okay)

      /\

      • receive(message, 0)
      • message.key = okay

    • (error)

      /\

      • receive(message, 1)
      • message.key = error
      • exists string: String
        • message.body[0] = string

  • T' = null
  • S' = C

A delete message asks for the deletion of a task result.

sendDelete(C) ==

/\

• exists message: Message

  /\

  • send(message, 1)
  • message.key = delete
  • exists taskid: TaskId
    • message.body[0] = taskid

• S' = C

A flush message asks for the session caches to be flushed and to switch flushing off (0) or on (1).

sendFlush(C) ==

/\

• exists message: Message

  /\

  • send(message, 1)
  • message.key = flush

  • \/

    • message.body[0] = 0
    • message.body[0] = 1

• S' = C

A reset message restarts the session resetting the range of task identifiers.

sendReset(C) ==

/\

• exists message: Message

  /\

  • send(message, 0)
  • message.key = reset
  • taskId' = taskMin

• S' = C

A result message contains the result of the task currently under evaluation (stored on top of the stack).

sendResult(C) ==

/\

• exists message: Message

  /\

  • send(message, 2)
  • message.key = result
  • taskDepth > 0
  • exists taskid: TaskId, exp: Expression

    /\

    • taskStack[taskDepth-1].body[0] = taskid
    • message.body[0] = taskid
    • message.body[1] = exp

  • taskDepth' = taskDepth-1

• S' = C