Indexing
Both local process names and action names may be indexed. This greatly increases the expressive power of FSP as demonstrated by the following examples.
The first example is a single cell buffer which stores integer values in the range 0..2.
BUFFER = EMPTY, EMPTY = (in[x:0..2] -> FULL[x]), FULL[x:0..2] = (out[x] -> EMPTY).
Initially the buffer is empty until an in action to store a value occurs. This action may be to store the value 0, 1 or 2 as indicated by the range [x:0..2]. The process moves into a state in which it stores the appropriate value FULL[0], FULL[1] or FULL[2]. Outputting the value returns the buffer to the EMPTY state. The scope of the range variable x in each case is the local process in which it is declared. The LTS for the process is depicted below:
The buffer process can be expressed more succinctly as below. BUF is exactly equivalent to BUF and generates an identical LTS.
BUF = (in[x:0..2] -> out[x] -> BUF).
When modelling behaviour of concurrent systems, it is frequently convenient to think of an action with a range as inputting a value in that range and an action indexed with a variable as outputting the value of that variable.
Ranges may be explicitly declared as shown below:
range T = 0..2 BUF = (in[x:T] -> out[x] -> BUF).
A store location may be modelled as below. To ensure a small LTS, the location stores a single bit:
range BIT = 0..1 STORE = VAL[0], VAL[b:BIT] = ( write[v:BIT] -> VAL[v] | read[b] -> VAL[b] ).
Both local processes and actions may have more than one index as illustrated by this example (for actions). A process which outputs the sum of two integers (in the range 0..N).
const N = 1 SUM = (in[a:0..N][b:0..N] -> out[a+b] -> SUM).
The observant reader will notice that the LTS for SUM is not minimal. The minimal system can be arrived at by minimising using LTSA or redefining SUM as follows:
const N = 1 SUM = (in[a:0..N][b:0..N] -> TOTAL[a+b]), TOTAL[s:0..2*N] = (out[s] -> SUM).