Stargazer: A Pi-Calculus Simulator

Try Reload

Cancel

Examples

Open the example programs and start playing!

Url/Hash

Your browser does not support the File API.

File

New empty suite

Cancel

Creating Gist...

Load from new Gist Open on GitHub

Close

Hi! This π-calculus simulator has been brought to you by

emanuele.dosualdo

Visit emanueledosualdo.com for details.

Stargazer by Emanuele D'Osualdo is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

I would appreciate if you contacted me before using the simulator in presentations/other material. Note that the current version is experimental. A new, open-sourced version will be released at some point.

You can use the syntax of π-calculus with the ascii notation:

Actions α.P
- Output: x<y₁,...,y_n>.P
- Input: x(y₁,...,y_n).P
- Internal: tau.P
The inactive process: 0 or zero (it can be omitted after an action: α.zero can be abbreviated α)
Parallel: P | Q
Guarded Sum (M): α₁.P₁ + … + α_n.P_n
Process call: P[y₁,...,y_n]
Restriction: new y₁,...,y_n.P
Process definition: P[y₁,...,y_n] := 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

INIT
DEFS

Where INIT is a process and DEFS is 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:

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 normalised, but

new x,y.(A[x] | x<y>)
A[x] := new z.x(u).(A[u] | u<x>| C[z,u])

is not since the initial term contains a sum 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.

Process calls A[x] where 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:

Runs the simulation by picking random reductions.

Displays the list of available reductions. Click on a reduction in the list to fire it. Hovering on reductions will highlight the subjects involved.

Adjust the speed of the simulation. Clicking on the percentage will restore it to 50%.

Show the code editor panel.

Toggle the visibility of the globally free names (if any).

Toggle the visibility of the labels displaying the names and the process identifiers in the topology. Hovering on an element will also reveal its complete label.

Toggle gravity in the layout.

Toggle collapse of names selected through search. Experimental.

(Config panel) Add some sequential processes to the current configuration. The syntax is a parallel composition of process calls. Any name of the current configuration can be used, unknown names will be interpreted as new top-level restrictions.

Show a list of preloaded examples.

Take a screenshot. Screenshots are vectorial SVG files that will be added to the menu and can be downloaded by selecting the menu entry.

Shows this help.