The second example describes a simple filesystem with several users communicating through a file server. The users address read/write requests to the server and wait for the corresponding accept/reject answers. The server policy is parameterized by two external procedures FileAvailableForRead and FileAvailableForWrite, described here by external C code. The global architecture is presented in figure 4.
The specification is parameterized by two values: N, the number of users and M, the number of files in the filesystem. It contains the definition of several application specific data types, respectively, integer domains (User and File), and the enumerated lists (Mode and Result). The specification provides description of the communication signals open, close and answer. Finally, there is the description of the processes in the system, respectively user and server. At this point, let us notice the number of user process instances is defined to be N.
Figure 5 describe the user processes. Basically, after an initialization phase they send non-deterministically open and close requests to the file server.
Let us focus on the initialization transition. The first two assignments illustrate the conversion operators {-} allowing to convert (in this example) integer values to process identifiers and back.
In order to understand these operators, imagine that the process identifier values are couples of the form [process,integer]. For instance [user,7] is a valid process identifier for an user process instance. Now, the operator {integer} applied to a pid value will extract the integer component of it (for the example above, {integer} [user,7] = 7). Conversely, the operator {process} applied to an integer will construct a pid value (example, {user} 7 = [user,7]).
In the user example, the expression {integer} self extract the integer value corresponding to the self process identifier, hence, a number between 0 and N-1, depending on the instance which execute the transition. Conversely, the construction {server} 0 means the process identifier of the server instance.
Finally, remark also the construction nextstate -; which means remaining in the same state, where the transition begins.
The server process is sketched in the figure 6. In few words, it stores the file system status in a two-dimensional array, which is modified accordingly opening and closing requests addressed by the users.
Let us notice the local definition of the FileSystem type, which is a two-dimensional array depending on both parameters N and M. Also, remark the definition of the external procedure FileAvailableForWrite, which implements the (possible complex) condition under that files are available for writing (e.g, true if nobody is writing, except maybe the same user u). Finally, let us observe the initialization transition. It gives an example of using the while statement, here, in order to initialize the file system status.
