AXDEF_ONE_DECL=Only one name can be declared in each axiomatic definition. AXDEF_FORMAT=Format of axiomatic definition is not supported. EXTCH_BRANCH=Process {0}, action {1}: A prefixing action must be a direct branch of an external choice. CHAN_INST=Process {0}, action {1}: Generic channel must be instantiated with a free type or {3} or {4}. CHAN_FORMAT=Process {0}, action {1}: Communication on channel {2}: only the last field can be input or output. EXPR_MEMB=Process {0}, action {1}: Membership expression is not supported. FUNCAPP_FORMAT=Process {0}, action {1}: Invalid format of function application. OP_UNSUPP=Process {0}, action {1}: Operator {2} is not supported. PAR_WRITERS=Process {0}, action {1}: Parallelism defines more than one writer. CHANUSE_UNIF=Process {0}, action {1}: Not possible to unify the ChanUse. CHANSYNC_UNIF=Process {0}, action {1}: Not possible to unify the ChanSync. DIFF_CARD=Process {0}, action {1}: Processes have different cardinalities. CHAN_NOT_DEF=Process {0}, action {1}: Channel {2} has not been defined. NAME_NOT_DEF=Process {0}, action {1}: Name {2} has not been defined. DIFF_CHAN_SYNC=Process {0}, action {1}: Channel {2} has different sync uses in a process. HIDE_PROC_ILLEGAL=Process {0}: Hiding is only allowed as the last operator in a process definition. OUTPUT_EXT_CHOICE=Process {0}, action {1}: Output channel {2} is being used in an external choice. CANCEL_TRANSLATION=Translation was canceled by the user.