Automated Verification of Asynchronous Communicating Systems (with TLA+)

Labeled Transition System (LTS) peer syntax

Peers are written using the "ORIGIN,DESTINATION,{?,!,τ}[,CHANNEL]" format:
ORIGIN and DESTINATION are integers, representing states (negative values are all equal and represent the failure state).
? represents a message reception, and ! the sending of a message. Both require CHANNEL to be defined.
τ represents an internal action done by the peer.
The "init,STATE" line indicates which state the peer starts from.
Any (and all) positive DESTINATION values that are not also an ORIGIN are considered to be "accepting" states (i.e. states in which the peer is considered as terminated).

Communication Models

One per line. Channels may belong to multiple communication models, and multiple instances of the same communication model may appear.

Pure asynchronism

Options: None.
Example:
async,,a,b,c,d

Causal

Options: None.
Example:
causal,,a,b,c,d

Point-to-point FIFO

Options: None.
Example:
fifo11,,a,b,c,d

FIFO 1-N

Options: None.
Example:
fifo1n,,a,b,c,d

FIFO N-1

Options: None.
Example:
fifon1,,a,b,c,d

FIFO N-N (Global ordering)

Options: None.
Example:
fifonn,,a,b,c,d

Message Cap/Limit

Options: BOUND.
Example:
message_cap,BOUND <- 6,a,b,c,d
or
message_cap,6,a,b,c,d

Channel Priorities

Options: BLOCKS.
Example:
channel_priorities,"BLOCKS <- {<<{""a""},""b"">>,<<{""a"",""c""},""d"">>}",a,b,c,d
or
channel_priorities,[a blocks b; {a,c} blocks d],a,b,c,d

Inferring constraints

To successfully use the channel priority inference process, the system must have a single "analyzed_by_pf" communication model (with no options).
On the other hand, using the "analyzed_by_pf" communication model outside of the inference process is not supported.