Our tool takes as an input an ASCII file containing the description
of a p-calculus system. This description shall be recognized by
the following grammar:
P
::=
(# x)P
(name restriction)
aP
(action with a continuation)
a
(action without continuation)
(P | ... | P)
(Parallel composition)
(P + ... + P)
(Internal choice)
a
::=
x![x1;...;xn]
(output)
y?[y1;...;yn]
(input)
*y?[y1;...;yn]
(replication)
Name restriction, input and replication are the only name binders.
This means that in (# x)P (resp. y?[y1;...;yn]P) (resp. *y?[y1;...;yn]P) occurrences of x (resp. y1,...,yn) (resp. y1,...,yn) in P are considered bound. All other name occurrences are considered free.
2.2 Operational semantics
Name restriction introduces a fresh name in an agent; parallel
composition allows in concurrently computing several agents; internal
choice denotes a non deterministic choice between several agents,
only one agent will be computed while the others will be ignored,
the choice is internal and does not depend on the other agents.
As an action, an agent can send or receive a message which is a tuple of channel names. The result of a
communication is given by using substitution. We use a lazy version of
replication: a resource is an agent which syntacticly duplicates itself
before receiving a message. Lazy replications enable to trace agent
creation.
2.3 Unsafe names
The analyzed system may contain free names. Such names are supposed to
be shared with an hostile context. No assumptions are made on them origin,
This means that we do not assume that they are distinct.
The hostile context is enable to use unsafe names to interact with the system.
It can spoil the system by sending unsafe names via an unsafe name, and it can spy the system by receiving names via an unsafe names, this way it gets control over the names it has received.
