Previous Contents Next

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 27 in a request ambient surrounded by a packet ambient, or to the variable rep of the agent rep 18 in an answer ambient surrounded by a packet ambient. We also capture the following information about markers: 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.


Previous Contents Next