## 4   Result

Our analyzer produces a html file containing a description of the input system behaviour.

### 4.1   Communication analysis

The analyzer describes the potential communications between agents. Due to the approximation, some of the discovered communications may be ineffective. But the analyzer detects all the communications. So if the analyzer detects no communication between two agents, there can be no communication between them.

#### 4.1.1   What is computed ?

We call a communication between a name restriction (# x) and a variable y the fact that a name created by an instance of the name restriction (# x) may be communicated to the variable y. For each interaction ((# x),y), we collect an approximation of the set I(x,y) of pair of words (idp,idc) such that a channel name created by the name restriction of an instance the marker of which is idc can be communicated to the variable of an instance the marker of which is idp. This approximation is given by both two grammars describing respectively the set of the first components of the elements of I(x,y) and the set of second components of the elements of I(x,y) and a relational approximation which calculates a set a affine constrains which are satisfied by the letter occurrence number of both element components of I(x,y).

#### 4.1.2   Interface

Interaction description can be obtained by clicking on a name restriction, and then on a variable.

### 4.2   Migration analysis

The analyzer describes the potential locations of agents. Due to the approximation, some of the discovered locations may be ineffective. But the analyzer detects all the locations. So if the analyzer detects no an agent can never be inside an ambient, it is correct.

#### 4.2.1   What is computed ?

We call a migration between an agent of an ambient labelled l and an ambient labelled l' the fact that an instance of the ambient n[·] may contain an instance of the agent P. For each migration (l,l'), we collect an approximation of the set I(l,l') of pair of words (idl,idl') such that an instance of the ambients labelled l' with the marker idl' may contain an instance of the ambient or of the agent labelled l with the marker idl. This approximation is given by both two grammars describing respectively the set of the first components of the elements of I(P,l') and the set of second components of the elements of I(P,l') and a relational approximation which calculates a set a affine constrains which are satisfied by the letter occurrence number of both element components of I(P,l').

#### 4.2.2   Interface

Interaction description can be obtained by clicking on the name of an ambient or on the first action of an agent, and then on the potential surrounding ambient.

### 4.3   Content analysis

Content analysis captures an upper approximation of the number of simultaneous instances of both agents and ambients that may occur inside a given syntactic ambients. This information is partitioned in accordance to the potential surrounding ambient.

This information can be obtained by first clicking on the name of the ambient, then clicking on the name of the potential surrounding ambient. To get the content of not surrounded ambient, a top-level ambient has been added. The number of agents occurring at the top-level can be obtained by clicking directly on the top-level ambient name.

For the sake of the simplicity we only display non relational information about occurrence number of agents. For that purpose, we associate to each syntactic agent an interval which described the potential number of simultaneous syntactic copies of this agent.

The result of this analysis is displayed as follows:
• agents which cannot occurs are displayed in grey;
• agents which may occurs an unbounded number of time simultaneously are displayed in orange. Due to the approximation of the analysis, it is only a warning, we cannot conclude whether the number of simultaneous occurrences of this agent is effectively unbounded or whether the analysis is not accurate enough;
• the label of each syntactic agent is tagged with the interval which describes its occurrence number.

### 4.4   Global occurrence analysis

Global occurrence analysis captures an upper approximation of the number of simultaneous instances of both agents and ambients that may occur in the system.

The result of this analysis is displayed as follows:
• agents which cannot occurs are displayed in grey;
• agents which may occurs an unbounded number of time simultaneously are displayed in orange. Due to the approximation of the analysis, it is only a warning, we cannot conclude whether the number of simultaneous occurrences of this agent is effectively unbounded or whether the analysis is not accurate enough;
• the label of each syntactic agent is tagged with the interval which describes its occurrence number.