Message Flow: message label syntax

• Message label syntax:

   
  predecessor guard-condition sequence-expression 
  return-value := signature
  e.g.: 1.1a, 1.1b / [mode = evaluate] 1.2 *[z:=1..n]': prim := nextPrim (prim)
  

• Predecessor is specified as :

  sequence-number ',' ... '/' 
  e.g.: 1.1a, 1.1b /
  

  Predecessor specifies the sequence numbers (separated by commas) of messages that must be performed before the current message is sent. This determines the sequence (not the time) and is used to synchronize threads.