Examples

5 Examples

We now interpret the results obtained when analyzing our example:

5.1 An ftp-server

5.1.1 An ftp-server

An ftp-server can be described by the following system:


(# request)(# make)(# server)(# duplicate)
(# instance)(# answer)(# client)
(
server[   
 !open duplicate.0 
      | !(k).instance[in k.open request.(rep).
               ( answer[<rep>] | out server.0 )
              ]
      ]
|

client[
 !(x).((# q)(# p) p[  
              out client.0
                   |
       request[<q>]
            |  
       open instance.0
            |
       in server.duplicate[out p.<p>]   

    ]

     | <make>)
|

<make>]

)

A resource creates recursively an unbounded number of clients. Each client is represented by a packet p[] which contains an ambient named request. This ambient contains the client's query á q ñ. At first, each packet exit the client ambient, enters the server ambient, and then activates a pilot ambient duplicate which communicates the packet name to the server. This communication creates a recursive instance of an ambient named instance which will process the packet. The instance ambient enters the packet, reads the request and sends it back inside an ambient named answer. At last, the packet exits the server ambient.

Analysis output can be consulted.

The analyzer proves that a name created by the restriction (# q) can only be communicated to the variable q of the agent á q ñ²⁷ in a request ambient surrounded by a packet ambient, or to the variable rep of the agent á rep ñ¹⁸ in an answer ambient surrounded by a packet ambient. We also capture the following information about markers:

whenever a name created by the restriction (# q) is communicated to the variable rep of an agent á rep ñ¹⁸, the marker of the instance having declared the name is on the form (21,34)(21,33)^m while the marker of the agent this name is communicated is on the form (21,34)(21,33)^m(12,32);
whenever a request ambient contains an agent á rep ñ¹⁸, the marker of the request ambient is on the form (21,34)(21,33)ⁿ while the marker of the contained agent is on the form (21,34)(21,33)ⁿ(12,32);
whenever a packet ambient contains a request ambient, the marker of the packet ambient is on the form (21,34)(21,33)^o while the marker of the request ambient is on the form (21,34)(21,33)^o(12,32);
whenever a name created by the restriction (# p) is communicated to the variable p of the packet ambient, the marker of the instance having declared the name is on the form (21,34)(21,33)^q while the marker of the ambient is on the form (21,34)(21,33)^q.

this proves that the name communicated inside the answer ambient and the name of the packet which surrounds this answer ambient have been both declared by the same recursive instance of the client resource.