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.