GρπF — Graphical ρπ Framework

GρπF is a web-based interactive tool for visualizing and manipulating ρπ-calculus terms using a graph rewriting semantics. It allows you to define processes, channels, and communications, apply reduction rules, and observe the evolution of processes graphically.

The tool implements the graph-based semantics introduced in the paper:

A Graph Rewriting-Based Semantics and Implementation for ρπ, by Julie Cailler and Martin Vassor

You may either install and run it locally, or use the online interpreter: https://grhopif.pythonanywhere.com/

Installation

We assume the reader has a working Python3 environment on a Linux machine. The installation procedure below sets up a virtual environment in which the dependencies will be installed. The program can be easily uninstalled by removing the directory containing the virtual environment.

Setting up the Virtual eEnvironment

$ python3 -m venv path/to/venv/directory/
$ source path/to/venv/directory/bin/activate

Note that the virtual environment directory will be created if need be. Users of csh and fish have to source activate.csh (resp. activate.fish) instead.

To deactivate later:

deactivate

Installing Dependencies

pip install networkx pyvis flask lark

Libraries used:

• networkx (graph manipulation)
• pyvis (visualization)
• flask (web interface)
• lark (parser)

Note that you also need an internet connection.

Running the Interpreter

$ python path/to/sources/app.py

This command will start a web server, which is the graphical interface of our interpreter. Go to http://127.0.0.1:5000 (by default) to use the interpreter.

You are now ready to use GρπF!

Interface Overview

The GρπF interface is make of the following buttons:

• A typing zone to write your own terms in GρπF!
• Load: Enter a ρπ-calculus term in the text area and load it as a graph.
• Restart: Clear the current graph.
• Quit: Stop the server.
• Expand all: Apply all applicable rules automatically (for one step).
• Collapse all: Collapse and delete nodes where applicable automatically (for one step).
• NuFresh/NuRestrict/Split/Bw/Fw/Merge: Apply the corresponding rule on one or multiple selected node(s) (if applicable).
• Various pre-loaded examples.

You can click a node to select it. To select multiple nodes, hold the Ctrl key while clicking on each node.

Nodes

The graph contains 6 types of nodes, each displayed in a distinct color:

• Process nodes (grey): represent a (HO)ρπ process, possibly carrying a substitution (e.g. Q{P/X}).
• Send nodes (green): represent an send action, written a⟨P⟩, meaning that process P is sent on channel a.
• Receive nodes (yellow): represent an receive action, written a(X) ▷ Q, meaning that a message received on channel a is bound to variable X in continuation Q.
• Parallel nodes (orange): represent a parallel composition P || Q.
• Nu nodes (purple): represent a name restriction νa.(P). Applying NuFresh opens the restriction by replacing a with a globally fresh name a_i (displayed with a # prefix, e.g. #a_1) and removes the binder.
• FreshName node (pink): a unique global counter node that tracks the next available fresh channel name thanks to a counter.

Write your own terms

You can write your own ρπ terms directly in the input area of GρπF.

The supported syntax is the following:

• Terminated Process: 0
• Processes: Lowercase (p, q, r, ...)
• Variables: Uppercase (X, Y, ...)
• Channels: Lowercase (a, b, ...)
• Parallel composition: |
• Send: send channel.process
• Receive: recv channel VARIABLE.process
• Nu: nu channel.(process)

Note that parallel composition is left-associative and parentheses can be used to group processes. Also, only variables may start with uppercase letters, whereas channel and process names must be lowercase.

Examples

Several example terms are available in the examples/ folder.
You can copy and paste them directly into the input area of the interface and click Load.

Example 1 — Communication

nu a. ((send a.p) | (recv a X. q))

This example illustrates a single communication. Two processes, P and Q, interact through a restricted channel a. The sender broadcasts process P, which is then substituted for the variable X in the receiver, producing the continuation Q.

Suggested steps:

• Apply NuFresh to open the restriction and generate a fresh channel.
• Apply Split to separate the parallel components.
• Select the sender and the receiver, then apply Fw to perform the communication.
• A new node Q appears, with causal edges from both the sender and the receiver to the continuation.
• Optionally, apply Bw and then Merge to undo the communication and restore the original processes.

Example 2 — Replication

nu c. (recv c X. (X | send c.X)) | (send c.(recv c X.((X | send c.X) | p)))

This term is adapted from the higher-order π-calculus replicator.
After a few communications on channel c, process P is replicated arbitrarily many times.

You can:

• Apply Nufresh to open the restriction on channel c.
• Repeatedly apply Split and Fw (or use Expand all) to observe the growth of the process and observe how causal dependencies accumulate.
• Use Collapse all to explore backward reductions.