This page describes the work done by Damien Pous (http://www.ens-lyon.fr/~dpous/), from ENS Lyon, France, during a summer internship in our project (see [1]). The aim was to use the Icobjs programming platform developped here to design a new and graphical implementation for the ambient calculus.

Some implementations had been proposed in the past, but they were all textual only and were suffering from a complex and costly mechanism of lock acquiring and releasing, with difficult theoretical problems to ensure that no deadlock could occur.

The current challenge was to design a completely graphical implementation where one could "see" the boundaries of an ambient. Moreover, we wanted to benefit from the reactive approach and the natural "atomicity" of operations induced by the physical simulation to get rid of these locking problems. The result is a Java program and applet which is able to "physically" simulate any ambient expression in any of the four dialects mentioned above, and see them evolve on the screen.

To get to some more concrete stuff, here is for example how the process

Each ambient is represented by a named and colored circle, whose size depends on its contents, and whose limits act as real boundaries for what is inside. The capability

A capability

A capability

This is the way mobile ambients react. Concerning the other models with co-capabilities (especially safe ambients), the co-capabilities are represented by "doors" moving around the boundaries of the ambient, which attract the corresponding capabilities.

(Note that any icobj can be moved by dragging it with the left mouse-button.)

First Example: Taxis

This example models a city with different sites, cabs and clients willing to go from one site to another. The complete protocol was presented in [7]. This demo is first initialized with three different sites a, b and c, two cabs available in the city, and three clients willing to go repeatedly back and forth from a to b, a to c, and b to c respectively. You can add more clients or cabs by left-clicking on the corresponding constructors on the left.

Click here to start the demo

This example comes from [8], where the encoding is extensively developped. In this demo, you can create channels of name n, outputs and inputs on these channels, and even more complex recursive pi-processes. The corresponding translation in pure ambients is then released and you can let the system evolve.

Click here to start the demo

General Ambient Factory

This applet provides general constructors for four different dialects of ambients: mobile ambients, safe ambients, robust ambients and controlled ambients. Left-clicking on the hand pops up a window asking for an ambient term. A second window asks for a name for the constructor. If the term is valid, a new constructor is created, and by left-clicking on it, we can launch the corresponding ambient as many times as we want.

Below are a few examples to familiarize with the syntax. The best way is to start the applet (it will start in another window) and simply perform copy-and-paste between the examples and the applet.

Click here to start the demo (in another window)

Syntax

In any of the 4 models, ambients are written

**mobile ambients:**`in n`,`out n`and`open n`**safe ambients:**`in n`,`out n`,`open n`, and`in_ n`,`out_ n`and`open_ n`for the corresponding co-capabilities (be careful not to forget a space after the underscore)**robust ambients:**same, except that the meaning of the name is different for co-capabilities**controlled ambients:**`in n`,`out n`,`open n`,`in_u n`,`in_d n`,`out_u n`,`out_d n`and`open_ (n,h)`

Then, try to release many copies of the same processes at the same time. See how capabilities are attracted by different ambients concurrently and how the first ambient encountered wins (this, combined with the randomness of shocks between ambients and walls, provides the non-determinism of the system). Finally, try to release processes

Another example to see recursion in action; an infinite number of ambients named x are released:

The following process creates a new private
name n (which should appear in the form "n#10"), creates some intricate
ambients named n and an ambient a which has the capabilities to enter or
exit n at any time. Theoretically, you should see the ambient a moving around
inside and outside any combination of n, and thus indefinitely.

And a last example (always in safe ambients),
to test the robustness of the implementation:

`
x[ rec X.out_ x.X | rec X.in_ x.X`

| rec Z.sleep 10.open n.( n[out x.in y.open_ n]

| n[out x.in y.open_ n]

| Z)]

| y[ rec X.out_ y.X | rec X.in_ y.X

| rec Z.sleep 10.open n.( n[out y.in x.open_ n]

| n[out y.in x.open_ n]

| Z)]

| n[in x.open_ n]

Two ambients x and y contain the same program: each time they encounter an ambient n, they open it, replace it with two fresh ambients n and send them to the other one. An initial n starts the process. The result is that x and y start exchanging an increasing number of ambients n.

Here is what you may get after a few hours... ;-)

| rec Z.sleep 10.open n.( n[out x.in y.open_ n]

| n[out x.in y.open_ n]

| Z)]

| y[ rec X.out_ y.X | rec X.in_ y.X

| rec Z.sleep 10.open n.( n[out y.in x.open_ n]

| n[out y.in x.open_ n]

| Z)]

| n[in x.open_ n]

Two ambients x and y contain the same program: each time they encounter an ambient n, they open it, replace it with two fresh ambients n and send them to the other one. An initial n starts the process. The result is that x and y start exchanging an increasing number of ambients n.

Here is what you may get after a few hours... ;-)

And now ?

Now it is your turn to play and invent new systems... Be creative ! ;-)

Download Area

ambicobj.jar (1056k)

This file contains all the necessary Java classes to use the demo either as a stand-alone application or as an applet. To launch it alone, use the command:

where

`arena`for the general ambient factory (by default)`taxis`for the taxis demo in robust ambients`taxis_`for a variant in controlled ambients`pi`for the pi-encoding in (pure) safe ambients`pi_`for Xudong Guan's variant in (pure) robust ambients`firewall`,`firewall_`,`pendulum`and`pentagon`also exist, but are undocumented

References:

[1] Damien Pous,

[2]

[3]

[4] Luca Cardelli and Andy Gordon,

[5] Francesca Levi and Davide Sangiorgi,

[6] Xudong Guan, Yiling Yang and Jinyuan You,

[7] David Teller, Pascal Zimmer and Daniel Hirschkoff,

[8] Pascal Zimmer,

Pascal Zimmer, October 2nd, 2002