Specification of Parameterized System

The FC2Parameterized format allows the systems specification using parameterized networks of communicating automata. It is an extension of the standard FC2 format with additional operators and user defined variables. This extension is done using the declarations section of FC2 format. We use a graphical syntax for a better understanding.

Example description

We use the well known Consumer-Producer system as an example. The example is shown in Fig. 1, it is composed of a single bounded buffer, with a maximal capacity of $Max$ elements, and a bounded quantity of consumers ( $\char93 consumer$) and producers ( $\char93 producer$) running in parallel.

Figure 1: Consumer-Producer system interaction

Both producers and consumers have a single functionality. The producers keep feeding the buffer with an arbitrary quantity ($x$) of elements without waiting for a response, while the consumers request an element from the buffer and wait for its response.

On the contrary, the buffer has two functionalities. On one side it keeps a bounded stock where elements are added and taken, but it also manages a queue where the request from the consumers are enqueued until elements become available.

We model each functionality of the system as a pLTS, and the hierarchical composition of this functionalities (pLTS) as pNets. We chose to describe the example behaviour in two FC2 files: SystemParameterized.fc2 describes the synchronisation network (i.e. the composition) between the producers, consumers and the buffer; both the behaviour of a consumer and the behaviour of a producer is included in the same file, while the behaviour of the buffer is described in the file BufferParameterized.fc2.

The System

Let's take a look back to the system, it is shown in Figure 2. The arbitrary numbers of consumers and producers are respectively represented by the exponents $c$ and $p$ in the figure.

Figure 2: Parameterized consumer-producer system

In the FC2Parameterized format, the system is described by three nets (consumer, producer and buffer) and a fourth net defining the synchronisation between them (having the synchronisation vectors) as follows:

declarations
constant consumers() ->any
constant producers() ->any
infix & (any any ) -> any priority 8
... % other necessary declarations
nets 4
   hook"main" > 0
   struct"Consumer-Producer"
   net 1
      struct "Buffer"
... % the rest of the net definition (semantic table)
   net 2
      struct "Consumer"
... % the rest of the net definition (semantic table & vertices table)
   net 3
      struct "Producer"
... % the rest of the net definition (semantic table & vertices table)
   net 0
      hook "synch_vector"
      struct _< 1,2&consumers,3&producers
... % the rest of the net definition (including synchronisation vectors)

When writing a parameterized system, all the variables and operators not predefined in the standard FC2 format should be declared in the declarations section of the file. In our example, the file begins declaring the variables consumers and producers, encoding respectively the set of consumers and producers. The keyword to declare a variable in FC2Parameterized is constant. The type of the variables (after the arrow) can be any of the FC2 Types. However, the FC2Instantiate tool does not make type checking yet, meanwhile we mainly use the type ``any''.

The operator & declared as infix in the file, when is used within the struct label of a net instantiates the referenced net (its left argument) to the size of the given set (its right argument). Then struct _< 1,2&consumers,3&producers indicates that the network is composed by one single instance of the network 1, #consumers instances of the network 2 and # producers instances of the network 3. For instance if consumers = {"cons1", "cons2"} and producers = [2, 4], then using the tool struct _< 1,2&consumers,3&producers is expanded to struct _< 1,2,2,3,3,3.

Before given the complete SystemParameterized.fc2 file contents, we analyse each one of its networks.

Consumer

The parameterized automaton modelling the Consumer behaviour is shown in Figure 3.

Figure 3: Parameterized Consumer

... 
   net 2
      struct "Consumer"
      behavs 2
         :0 "Q_get()"
         :1 "R_get()"
      logic "initial">0
      behav !0+?1
      hook "automaton"
      vertice 2
         vertex 0
            edges 1
               edge0 
                  behav !0 -> 1
         vertex 1
            edges 1
               edge0 
                  behav ?1 -> 0
...

Since the consumer does not use parameters, its definition is done using the standard FC2 format as shown next to the figure.

Producer

The parameterized automaton modelling a Producer behaviour is shown in Figure 4. The transition's alphabet is specified in the behaviour's semantic table of the net. The semantic table for the Producer is shown next to the figure.

Figure 4: Parameterized Producer

declarations 
...  
  infix & (any any ) -> any  priority 8 
  prefix in (any any) -> any 
...  
  net 3 
    behavs 1 
      :0 "Q_put"&in(1,Max) 
...

The & operator, when inside a semantic table, takes a FC2 Expression in its left side and a list of sets (each set separate by ``,'') in its right side (in our example there is only one set). This operator generates, during instantiation, an entry in the semantic table for each member of the Cartesian product of the sets in its right side.

The in operator takes two integers and generates the set of all the integers between those integers inclusive ( $in(1, 3) = \{1, 2, 3\}$). For instance, when running the FC2Instantiate tool with $Max = 3$, the semantic table above is extended to:

... 
  net 3 
    behavs 3 
      :0 "Q_put(1)" 
      :1 "Q_put(2)" 
      :2 "Q_put(3)" 
...

Within states (vertices) and transitions (edges), their local variables should be assigned using a hook label (one per variable). The variables are assigned with the infix operator =, which takes a variable name in its left side and a set in its right side. When using the tool, the variable is assigned to each element of the set.

In the producer the state has no variables. On the contrary, the only transition contains the variable $x$ which will range in the set $[1, Max]$. Then the vertices table of the Producer is:

declarations 
... 
  infix = (any any ) -> any priority 8 
  infix & (any any ) -> any priority 8 
... 
    vertice 1 
      vertex 0 
        edges 1 
          edge0 
            hook x=in(1,Max) 
            behav !(0&x) -> 0

The left parameter of the operator &, when used inside an automaton's edge (which is not a synchronisation vector), is a reference to an action in the corresponding semantic table of the net; and the right parameter is an expression. When using the tool, an expression of the form 0&x (inside an automaton edge) will be replaced by a reference to the entry 0 of the semantic table (note that the corresponding entry in the table must be also parameterized by x or equivalent) for each instantiation of x.

The complete parameterized description of a producer and its instantiation when $Max = 3$ are:

declarations constant Max() -> int constant x() -> int infix & (any any ) -> any priority 8 infix = (any any ) -> any priority 8 prefix in (any int) -> any ... net 3 behavs 1 :0 "Q_put"&in(1,Max) logic "initial">0 hook "automaton" vertice 1 vertex 0 edges 1 edge0 hook x=in(1,Max) behav !(0&x) -> 0 ...

... net 3 behavs 3 :0 "Q_put(1)" :1 "Q_put(2)" :2 "Q_put(3)" logic "initial">0 hook "automaton" vertice 1 vertex 0 edges 3 edge0 behav !0 -> 0 edge1 behav !1 -> 0 edge2 behav !2 -> 0 ...

Buffer

The buffer communicates with consumers and producers through three actions: $Q\_get$ to receive a request for element from a consumer, $R\_get$ to give the answer to the consumer and $Q\_put$ to receive feeds from producers. Since the behaviour of the buffer is given in a separate file, in the file SystemParameterized.fc2 only is specified its behaviour semantic table (i.e. its alphabet of actions) as follows:

declarations 
... 
  constant Max() -> int 
  infix & (any any ) -> any priority 8 
... 
   net 1
      struct "Buffer"
      behavs 3
         :0 "Q_get"&consumer
         :1 "R_get"&consumer
         :2 "Q_put"&in(1,Max)
      behav ?0+!1+?2
      hook "synch_vector"

Synchronisation vectors and complete SystemParameterized.fc2 file

Finally in the net 0 we give the synchronisation vectors that define the actions from the producers, consumers and the buffer which should be synchronised.

In the synchronisation vector we use the $ operator to indicate which of the instances of a network is being to be referenced.

In a synchronisation vector a reference such as behav 0&c < ?(0&c)$1, !0$(2&c) -> 0 indicates that the action labelled with the entry 0 (for an instantiation of c) in the net 1, is synchronised with the entry 0 of the net 2 (where the net 2 is instantiated for an evaluation of c). This synchronisation is observable and produces a global action labelled with the entry 0 (for an instantiation of c) in the behaviour semantic table of the net having the synchronisation vector.

The complete SystemParameterized.fc2 file is shown bellow:

declarations                           net 3
constant Max() -> int                    struct "Producer"
constant x() -> int                      behavs 1
constant consumers() ->any                  :0 "Q_put"&in(1,Max)
constant producers() ->any                logic "initial">0
constant c() ->any                       behav !0
constant p() ->any                       hook "automaton"
constant queue() ->any                   vertice 1
infix & (any any ) -> any priority 8       vertex 0
infix $ (any any ) -> any priority 8         edges 1
infix = (any any ) -> any priority 8           edge0 
prefix in (any int) -> any                       hook x=in(1,Max)
nets 4                                           behav !(0&x) -> 0
  hook"main" > 0                      net 0
  struct"Consumer-Producer"             struct _< 1,2&consumers,3&producers
  net 1                                 hook "synch_vector"
    struct "Buffer"                    behavs 3
    behavs 3                             :0 "Q_get"&consumers
      :0 "Q_get"&consumers                :1 "R_get"&consumers
      :1 "R_get"&consumers                :2 "Q_put"&(producers,in(1,Max))
      :2 "Q_put"&in(1,Max)              behav 0+1+2
    behav ?0+!1+?2                       vertice 1
    hook "synch_vector"                     vertex 0
  net 2                                      edges 3
    struct "Consumer"                          edge 0
    behavs 2                                     hook c=consumers
      :0 "Q_get()"                                behav 0&c < ?(0&c)$1, !0$(2&c) -> 0
      :1 "R_get()"                              edge 1  
    logic "initial">0                            hook c=consumers
    behav !0+?1                                  behav 1&c < !(1&c)$1, ?1$(2&c) -> 0
    hook "automaton"                           edge 2  
    vertice 2                                    hook p=producers
      vertex 0                                   hook x=in(1,Max)
        edges 1                                  behav 2&(p,x) < ?(2&x)$1, !(0&x)$(3&p) -> 0
          edge0                                  
            behav !0 -> 1 vertex 1
      vertex 1
        edges 1
          edge0 
            behav ?1 -> 0

As we mention before, if consumers = {"cons1", "cons2"} and producers = [2, 4], then using the tool the expression struct _< 1,2&consumers,3&producers is expanded to struct _< 1,2,2,3,3,3. Then when c="cons2" and p=3, the vector behav 0&c < ?(0&c)$1, !0$(2&c) -> 0 becomes behav 1 < ?1,*, !0, *,*, * -> 0.

Buffer's behaviour

The buffer's behaviour is described through a synchronisation network between two components: stock and queue. stock takes care of keeping the actual number of elements (up to $Max$) in the buffer's stock and receive the feeds from the producers. queue receives the requests from the consumers and put them in a queue. The answers to the consumers are given in FIFO order from the request queue until elements are available in the buffer's stock.

The network describing the buffer behaviour is shown in Figure 5.

Figure 5: Parameterized Buffer

The behaviour of the buffer is specified in a separate file because FC2Instantiate does not support nested synchronisation networks in a single file.

In the stock, its only state is parameterized with the variable stock. The variable stock encodes the quantity of elements actually available in stock. When an element is taken, this variable is decreased by 1, which is expressed by a transition to the state encoding the stock having one element less, in the figure correspond to the transition labelled $[stock>0]!getElement \to stock -1$. When feeding the stock (action $Q\_put$) this variable is incremented by the quantity of elements received, transition labelled as $?Q\_put(x)$ ( $[0 \leq x \leq Max - stock]?Q\_put(x) \to stock+x$ in the figure. Note that both transitions are guarded to avoid taken an element from an empty stock or to overfill it.

The FC2 file describing the stock is:

declarations
constant Max() ->any
constant stock() ->any
constant x() ->any
infix & (any any ) -> any priority 8
infix = (any any ) -> any priority 8
infix - (any any ) -> any priority 8
prefix in (any int) -> any
prefix greaterThan (any any) -> any
prefix when (any) -> any
...
   net 2
      struct "stock"
      behavs 2
         :0 "Q_put"&in(0,Max)
         :1 "getElement"
      logic "initial">0
      behav ?0+!1
      hook "automaton"
      vertice 1
         vertex 0
            hook stock=in(0,Max)
            edges 2
               edge0 
                  hook x=in(1,(Max-stock))
                  behav ?(0&x) -> 0&(stock+x)
               edge1 
                  hook when(greaterThan(stock,0))
                  behav !1 -> 0&(stock-1)

As you can see, new operators supported by the tool are introduced: the conditional operator when, the comparison operator greaterThan, and the arithmetic operators - and +.

In the queue, the states are parameterized by the state variable queue which encodes the states of a queue. A queue is characterised by its contents.

When a request for one element is received ( $?Q\_get(c)$), the caller id ($c$) is appended to the end of the queue $put(queue,c)$. As soon as an element is available in the stock ( $?getElement$), the first caller from the queue is taken ( $getFirst(queue)$) and a response to it is given ( $!R\_get(c)$). At the same time the caller is removed from the queue ( $removeFirst(queue)$).

Figure 5 introduces several operators supported by the FC2Instantiate tool to manipulate queues. Their complete descriptions are given in section 5.1.

The FC2 file describing the Queue is:

declarations
constant consumers() ->any
constant c() ->any
constant queue() ->any
infix & (any any ) -> any priority 8
infix = (any any ) -> any priority 8
prefix when (any) -> any
prefix instantiateQueue (any) -> any
prefix getFirst (any) -> any
prefix removeFirst (any) -> any
prefix fullQueue (any) -> any
prefix emptyQueue (any) -> any
prefix putQueue (any) -> any
prefix size (any) -> any
...
   net 1
      struct "queue"
      behavs 3
         :0 "Q_get"&consumers
         :1 "R_get"&consumers
         :2 "getElement"
      logic "initial">0
      behav ?0+!1+?2
      hook "automaton"
      vertice 2
         vertex 0
            hook queue=instantiateQueue(size(consumers),consumers)
            edges 2
               edge0 
                  hook c=consumers
                  hook when(!fullQueue(queue))
                  behav ?(0&c) -> 0&putQueue(queue,c)
               edge1 
                  hook when(!emptyQueue(queue))
                  behav ?2 -> 1&queue
         vertex 1
            hook queue=instantiateQueue(size(consumers),consumers)
            edges 1
               edge0 
                  hook when(!emptyQueue(queue))
                  behav !(1&getFirst(queue)) -> 0&removeFirst(queue)
...

As specified in Figure 5, the complete Buffer behaviour is done by synchronising the $getElement$ action of stock and of queue (the queue request elements from the stock). The full FC2 file describing this synchronisation is following:

declarations
constant Max() ->any
constant consumers() ->any
constant stock() ->any
constant x() ->any
constant c() ->any
constant queue() ->any
infix & (any any ) -> any priority 8
infix $ (any any ) -> any priority 8
infix = (any any ) -> any priority 8
infix - (any any ) -> any priority 8
prefix in (any int) -> any
prefix greaterThan (any any) -> any
prefix when (any) -> any
prefix instantiateQueue (any) -> any
prefix getFirst (any) -> any
prefix removeFirst (any) -> any
prefix fullQueue (any) -> any
prefix emptyQueue (any) -> any
prefix putQueue (any) -> any
prefix size (any) -> any
nets 3
   hook"main" > 0
   struct"Buffer"
   net 1
      struct "queue"
      behavs 3
         :0 "Q_get"&consumers
         :1 "R_get"&consumers
         :2 "getElement"
      logic "initial">0
      behav ?0+!1+?2
      hook "automaton"
      vertice 2
         vertex 0
            hook queue=instantiateQueue(size(consumers),consumers)
            edges 2
               edge0 
                  hook c=consumers
                  hook when(!fullQueue(queue))
                  behav ?(0&c) -> 0&putQueue(queue,c)
               edge1 
                  hook when(!emptyQueue(queue))
                  behav ?2 -> 1&queue
         vertex 1
            hook queue=instantiateQueue(size(consumers),consumers)
            edges 1
               edge0 
                  hook when(!emptyQueue(queue))
                  behav !(1&getFirst(queue)) -> 0&removeFirst(queue)
   net 2
      struct "stock"
      behavs 2
         :0 "Q_put"&in(0,Max)
         :1 "getElement"
      logic "initial">0
      behav ?0+!1
      hook "automaton"
      vertice 1
         vertex 0
            hook stock=in(0,Max)
            edges 2
               edge0 
                  hook x=in(1,(Max-stock))
                  behav ?(0&x) -> 0&(stock+x)
               edge1 
                  hook when(greaterThan(stock,0))
                  behav !1 -> 0&(stock-1)
   net 0
      behavs 3
         :0 "Q_get"&consumers
         :1 "R_get"&consumers
         :2 "Q_put"&in(1,Max)
      struct _< 1,2
      behav ?0+!1+?2
      hook "synch_vector"
      vertice 1
         vertex 0
         edges 4
           edge 0
             hook c=consumers
             behav ?(0&c) < ?(0&c)$1 -> 0
           edge 1
             hook c=consumers
             behav !(1&c) < !(1&c)$1 -> 0
           edge 2
             hook x=in(1,Max)
             behav ?(2&x) < ?(0&x)$2 -> 0
           edge 3
             behav tau < ?2$1, !1$2 -> 0