Hi! This π-calculus simulator has been brought to you by
You can use the syntax of π-calculus with the ascii notation:
zero(it can be omitted after an action:
α.zerocan be abbreviated
P | Q
α1.P1 + … + αn.Pn
P[y1,...,yn] := M
Parentheses can be used to group actions, for example:
x(y).x(z) + x<a> is different from
x(y).(x(z) + x<a>).
Your program should have the form
INITis a process and
DEFSis a sequence of definitions.
You should write normalised programs: the initial term should not contain sums and only the top-level of each definition should be a sum. For example:
is normalised, but
new x,y.(A[x] | B[x,y]) A[x] := x(u).new z.(A[u] | B[u,x] | C[z,u]) B[x,y] := x<y>
is not since the initial term contains a sum
new x,y.(A[x] | x<y>) A[x] := new z.x(u).(A[u] | u<x>| C[z,u])
x<y>, and so does the continuation in the definition of
A[x]. Moreover the definition of
A[x]contains a restriction at top level which is not allowed: if you need it there, move it outside in the call of
A[x], otherwise consider if you meant to use it under a prefix.
A is not defined, will be treated as if the definition was
A[x] := 0.
Another important restriction:
the free names of the body of a definition have to be bound by the definition's head!
This means that the definition
A[x] := x(y).(z<y> | A[y])
is not valid because
z occurs free in the body but is not in the argument list. To fix the definition you have to include it as in
A[x,z] := x(y).(z<y> | A[y,z]).
Note that the initial process can contain free names. They will however be treated as top-level restrictions in displaying the communication topology, unless the "Hide globally free names" () option is selected.
Here is an explanation for the controls: