A Glimpse of Erlang

Friendlier Representations

Local behavior: communicating machines

Finite-state machine

From source node to sink node.

fork gate - join gate

branch gate - merge gate

There should be one active participant

Any non-active participant should be passive decides which branch to take in a choice.

A is active when it locally decides which branch to take in a choice.

B is passive when

either B behaves uniformly in each branch
or B unambiguously understand which branch A opted for through the information received on each branch.

Well-branchedness: When the above holds true for each choice, the choreography is well-branched. This enables correctness-by-design

\(G_1=A\rightarrow B:int+A\rightarrow B:str\)

This is well-branched, because B unambiguously understand which branch A would choose.

\(G_2=A\rightarrow B:int+\emptyset\)

This is not well-branched, because when A choose to do nothing, B will feel ambiguous.

\(G_3=A\rightarrow B:int+A\rightarrow C:str\)

This is not well-branched, because whichever branch A choose, there always be one between B and C feeling ambiguous.

\(G_4=A\rightarrow C:int;A\rightarrow B:bool+A\rightarrow C:str;A\rightarrow C:bool;A\rightarrow B:bool\)

This is well-branched, because B behaves uniformly in both branches. For C, it always knows which branch A choose.

Empty

Interaction \(A\rightarrow B:m\)

Fork \(G|G\)

choice \(sel\{G+\cdots+G\}\)

Sequential \(G;G\)

iteration \(repeat\ G\)