Examples of pi-calculus programs

Counters.json

{
  "gravity": false
}

Counters.pi

νc0,c1.( Z[c0] | Z[c1] | M1[c0,c1] )

C[c,p] := c<p>
Z[c] := c().Z[c]
M[c1,c2] :=
    c1(r).M[r,c2]
  + c2(r).M[c1,r]
  + tau.new t.(M[t,c2] | C[t,c1])
  + tau.new t.(M[c1,t] | C[t,c2])
M1[c1,c2] :=
    c1<>.new c.( M2[c,c2] | C[c,c1] )
  + c1(r).new c.( M1[r,c] | C[c,c2] )
M2[c1,c2] :=
    c2<>.new c.( M1[c1,c] | C[c,c2] )
  + c2(r).new c.( M2[c,r] | C[c,c1] )

Couples.pi

new p,q.(M[p,q] | Gp[p] | Gq[q])

M[p,q] := p(x).(M[p,q] | PM[q,x])
Gp[p] := tau.new w.(Gp[p] | Aw[p,w])
Gq[q] := tau.new z.(Gq[q] | Bw[q,z])
Bw[q,w] := q<w>.B[w]
Aw[q,w] := q<w>.A[w]
PM[q,x] := q(y).N[x,y]

default.json

{
  "default": "Servers"
}

Hannenfass.json

{
  "showGlobals": true
}

Hannenfass.pi

/* * * * * * * * * * * * *\
 * The Rumor Mill        *
 * at the Hannenfass bar *
 * * * * * * * * * * * * * 

 Coded by Thomas Schneider 
 Adapted by Emanuele

\* * * * * * * * * * * * */


// One wise man and four naive ones walk into a bar
new table.(
  Barman[bar,table]@(0,0)
| Wise[bar,secret]
| Naive[bar]
| Naive[bar]
| Naive[bar]
| Naive[bar]
| Naive[bar]
)

// Barman
Barman[bar,t] :=
    bar<t>.B[bar,t]
  + tau.(Barman[bar,t] | Naive[bar])
B[bar,t] :=
  bar<t>.new table.Barman[bar,table]

// Wise Customer, knows the secret
Wise[bar,s] :=
    bar(t).W[bar,s,t]
W[bar,s,t] :=
    t<s>.Wise[bar,s] // Tell the secret
  + t().Wise[bar,s] + t<>.Wise[bar,s] // Chitchat

//Naive Customer
Naive[bar] :=
    bar(t).N[bar,t]
N[bar,t] :=
    t(s).Wise[bar,s]
  + t<>.Naive[bar]
  + t().Naive[bar]

/*
  bar(t) - ask for table
  t      - table-talk
  s      - secret for more excitement
*/

List.json

{
  "gravity": false
}

List.pi

new a.L[a]

L[x] := tau.new y.(L[y] | B[x,y])

Lists.json

{
  "gravity": false
}

Lists.pi

new a.A[a]

A[x] := tau.(A[x] | L[x])
L[x] := tau.new y,z.(L[y] | B[x,y,z] | C[z])

Ring.json

{
  "gravity": false,
  "palette": {
    "S": "#2ca02c",
    "M": "#1f77b4",
    "T": "#ff7f0e",
    "D": "#98df8a"
  }
}

Ring.pi

ν master.(
    M[master,master]
  | T[master]
  )

// The master of the ring
M[self, fst] :=
  self().new next,data.(
    M[self, next]
  | S[next, fst, data]
  | T[next]
)

// A slave
S[self,next,data] :=
  self().(
    S[self, next,data]
  | T[next]
  | D[data]
  )

// The Token
T[x] := x<>

Server.json

{
  "showLabels": true,
  "gravity": true
}

Server.pi

new s. (S[s] | E[s])

S[s] := s(x).νd.( S[s] | A[x,d] )
E[s] := τ.new m.(E[s] | C[s, m])
C[s, m] := τ.( C1[s,m] | Q[s,m] )
C1[s, m] := m(x).C[s, m]
A[x,d] := x<d>
Q[s,m] := s<m>

Servers.pi

new s. (S[s] | E[s])

S[s] := s(x).νd.( S[s] | A[x,d] )
E[s] := τ.new m.(E[s] | C[s, m]) + τ.νs'.(E[s'] | S[s'] | E[s])
C[s, m] := τ.( C1[s,m] | Q[s,m] )
C1[s, m] := m(x).C[s, m]
A[x,d] := x<d>
Q[s,m] := s<m>