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