FC2Parameterized reference manual

While the FC2Parameterized format is not ``human-friendly'', it is a powerful language to describe behaviour of systems. Even when humans may directly use this language to model distributed system, its main target is to be the intermediate format produced by our automatic tools in order to do verification.

This section contains a preliminary version of the FC2Parameterized reference manual. It is expected that the tool (FC2Instantiate) and the format will evolve quickly in the short term, and a separate reference manual document will follow.

Additionally to the predefined operators in the FC2 format, the FC2Parameterized defines the following (all of them supported in the FC2Instantiate):

General Operators

• $\& : Exp × Exp \to Exp$, where Exp is an FC2 expression. Its semantic depends on the context where is used:
  • In a semantic table. 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. This operator generates an entry in the semantic table for each member of the Cartesian product of the sets in its right side.
  • In an automaton's edge. 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 (for instance, the behaviour label in the edge/vertex, reference the behaviour table of the net). The right side contains 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 entry in the table should be also parameterized by x or equivalent) for each instantiation of x.
  • In a synchronisation vector. When it is present at the left side of the $ operator, it semantic is the same that when is inside an automaton's edge (defined above). When is in the right side of the $ operator is analogous to the edge case, but it references to an evaluation of a net instead of a semantic table.
  • In the struct label of a net. In this case the & operator indicates the number of instantiations to be done for a net. In its left side is the referenced net, and in its right side a set. The number of instantiations of the nets will be the same as the number of elements of the set. For instance 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 (consumers is a variable encoding a set) and #producers instances of the network 3.
• $\$ : Exp × Exp \to Exp$, where Exp is an FC2 expression. In the synchronisation vectors, the $ operator is used to indicate which of the instances of a network is being referenced.
• $when : boolean$ is used in a hook to indicate a condition. When the condition is not true, the instantiation stops for the vertex/edge holding the hook.
• $= : varName × Set$ is for assignment of values to a variable. When instantiating, the variable on the left side will be assigned to each element in the set of the right side.

Set operators

• $set : List(any) \to Set$. This operator receives a list of elements and constructs an ordered set containing them. Ex: var=set("a",3,"b","other") ( $var = \{''a'', 3, ''b'', ''other''\}$).
• $in : int × int \to Set$. The operator receives two integers and generates the set of all the integers between them inclusive. Ex: var=in(2,5) ( $var = \{2, 3, 4, 5\}$).
• $size : Set \to int$. The size operator receives a set and returns the number of elements in it. Ex: size(var)=4 ( $var = \{''a'', 3, ''b'', ''other''\}$).
• $merge : Set × Set \to Set$. The merge operator receives two sets and returns an unique set with the disjoint union of elements in both sets. Ex: merge(set("a","b"),merge(in(1,2),set("b"))) ( $= \{''a'', ''b'', 1, 2,''b''\}$).

Queue Operators

Often in distributed systems, because their asynchronous communication nature, it is needed to model queues, sometimes named channels. FC2Parameterized provides the following set of queue manipulation:

• $instantiateQueue : Set × int \to queue$. This operator receives a set of the potentially elements that could be added to the queue, and a maximal capacity of the queue. It generates the queue (queue is an internal type for FC2Parameterized). Ex: queue=instantiateQueue(var,6) ( $var = \{''a'', 3, ''b'', ''other''\}$).
• $putQueue : queue × any \to queue$. This operator receive a queue and an element to be added at the end of the queue. It returns the queue with the element already added. Ex: queue=putQueue(queue,"newElement").
• $getFirst : queue \to any$. This operator returns the first element of a queue. Ex: var=getFirst(queue).
• $getFirstFilter : queue × Set \to any$. This operator returns the first element of a queue that is in the set $Set$. Ex: var=getFirstFilter(queue,set("a",2)).
• $removeFirst : queue \to queue$. This operator returns the queue $queue$ without it first element. Ex: queue=removeFirst(queue).
• $removeFirstFilter : queue × Set \to queue$. This operator returns the queue $queue$ without the first element in the queue which is also in the set $Set$. Ex: queue=removeFirstFilter(queue,set("a",2)).
• $fullQueue : queue \to boolean$. This operator checks whether the queue has reach the maximal capacity. Ex: fullQueue(queue).
• $emptyQueue : queue \to boolean$. This operator checks whether the queue is empty. Ex: emptyQueue(queue).
• $emptyQueueFilter : queue × Set \to boolean$. This operator returns true if the queue has no elements from the set $Set$. It returns false otherwise. Ex: emptyQueueFilter(queue,set("a",1)).
• $hasElement : queue × any \to boolean$. This operator returns true if the element $any$ is in the queue $queue$. It returns false otherwise.

Arithmetic operators

• $+ : int × int \to int$. Addition between integers. Ex: var=3+var.
• ^ $: int × int \to int$. Power. Ex: var^3 ($= var^3$).
• $- : int × int \to int$. Subtraction between integers.
• $× : int × int \to int$. Multiplication between integers.
• $/ : int × int \to int$. Integer division between integers. The result is the integer part of the division.
• $mod : int × int \to int$. It gives the common residue of the arguments.
• $greaterThan : int × int \to boolean$. It returns true if the first argument is greater than the second one, false otherwise.
• $lessThan : int × int \to boolean$. It returns true if the first argument is less than the second one, false otherwise.
• $equal : int × int \to boolean$. It returns true if the first argument is equal than the second one, false otherwise.