FC2 Format

The FC2 format allows for description of labelled transition systems and networks of such. Automata are tables of states, states being each in turn a table of outgoing transitions with target indexes; networks are vectors of references to subcomponents (i.e., to other tables), together with synchronisation vectors (legible combinations of subcomponent behaviours acting in synchronised fashion). Subcomponents can be networks themselves, allowing hierarchical description.

It is important to note that this format was created as a mean of communication between several software tools in the process algebra area. The format specification defines only the syntax, and it is up to the tools to define a compatible semantics for the different format's entities. Indeed, it has been used with success in tools dealing with quite different flavours of process algebras, included timed ones.

In the following we introduce the syntax of FC2 format.

Structure of an FC2 file

An FC2 object (usually found in a file) consists of:

[optional]  Declarations of expression operators,
A table of nets, containing:
  the number of nets,
  global semantic tables,
  a global label,
  the nets.
  Each net (or graph) containing:
    [optional] its number,
    local semantic tables,
    the net label,
    The vertice table [optional], composed of:
      the number of vertices,
      the vertices.
      Each vertex contains:
        [optional] its number,
        the vertex label,
        The edges table [optional], composed of:
          the number of edges,
          the edges.
          Each edge contains:
            [optional] its number,
            the edge label,
            the index(es) of the resulting state(s).

nets 1 hook "main">0 net 0 struct "t1" logic "initial">0 hook"automaton" vertice 2 vertex0 struct"v0" edges2 behav"a" result 0 behav"b" result 1 v1s"v1"E2 b"a"r0 b"b"r1

For example, this FC2 object contains a single net (indeed an automaton, as indicated in the net hook). The automaton has two vertices with two edges each. All information attached appears here directly in place, though it could have been tabulated. The text for the first vertex appears in long form (more readable), while the second vertex is in short, compact, form.

FC2 Objects

Expressions

exp : CONSTANT                     ref :  INT 
    | UNARY exp                              |  GLOBAL INT
    | exp INFIX exp                          |  BQUOTE INT
    | PREFIX OP exp CP                  ;
    | OP exp CP
    | STRING 
    | STAR 
    | ref              
    ;

An expression represents an algebraic term. Some of the operators are predefined, some are user-defined, and declared in the file header. The basic bricks are the constant operators, the strings, and integers used as references in the semantic tables.

The ``*'' character has a special syntax (token STAR), used for specifying idle arguments in synchronisation vectors:

* is the constant expression ``idle''

*i with i a positive integer, is equivalent to the sequence of i idle constants, ``*,*,...,*''.

Types

Operators are typed, and the types are used to determine in which table a reference is to be searched. Possible types are: behav, struct, logic, hook, int, any. The type any is used as a type variable.

The following table lists the predefined operators. There is no predefined PREFIX.

Constant:  "t" : behav    (long form "tau")          Binary:    "^" : any * int -> any
           "q" : behav    (long form "quit")                    "+" : any * any -> any
           "_" : any                                            "<" : any * any -> any
Unary:     "!" : any -> any                                     ">" : any * any -> any
           "?" : any -> any                                     "," : any * any -> any
           "~" : any -> any                                     ";" : any * any -> any
           "#" : any -> any                                     "." : any * any -> any

All infix operators have priorities and they are left associative (e.g. x.y.z means (x.y).z). User-defined operators will be assigned a priority in the declarations as shown later.

In the following we list the priorities of predefined operators. The priorities range from 0 to 50, the lower the number, the strongest the priority.

Operator	Priority
+	50
> <	40
,	30
;	20
. ^	10

tau     % the constant "tau", usually interpreted as the internal action
q       % the special action "quit" (or the "delta" of Lotos)
3       % a reference to the entry number 3 in the corresponding semantic table
!"s"    % the application of the unary operator "!" to the string "s",
        % e.g. the emission of signal "s"
1+2     % the sum of the expressions referenced 1 and 2

(t<1,!(3,?(11,1)))+(t<2,!(10,?(0)))
        % a big expression

Labels

Labels are used to store all kind of information attached to FC2 objects (nets, vertice, edges). They are records with 3 specific fields: struct, behav, logic, plus an additional field, hook, gathering all kind of extra information. All fields are optional. When a field is present, it contains a single expression.

Hooks will usually contain information private to a tool, or to a small set of tools. In addition, some of the conventions defined in this document also make use of hooks. Hook information need not be defined by the format, so it will not be parsed: it appears as mere strings in the hook value. Each tool will decide whether or not to decode this value, depending on the name of the hook. On the other hand, some tools may agglomerate hooks when building new objects, so hook values (with same name) will be composed from string with the usual expression operators.

struct "name0"
behav "act1"+"act2"
                        % value can be explicite expressions
logic "initial"
logic (~0 + 1).2        % or use references

                        % To give a hook a name, one usually use the ">" operator
hook "colour">"red"
hook "coord">"x=134,y=24"+"x=35,y=124"

Convention

: In a given label, the Struct, Behav, and Logic fields should appear at most once. There can be several Hook fields, though, and multiple hooks will be interpreted as conjunctions (as if connected by a "." operator).

Semantic Tables

Expressions may appear at many places in the file, but usually their values are tabulated, both for compact and semantic reasons. Thus, expressions are gathered in tables, sorted by type; there are four semantic table types, corresponding to the four label fields:

behavs, structs, logics, hooks

A semantic table has a type, a size, and a number of entries. Each entry has an optional index, and contains an expression. The size is a positive integer, bigger than all entry indexes. An entry without an index gets its index from the preceding entry, plus one.

behavs 3
:0 tau
:1 "a1"
:2 !1

logics 2
:0 "initial">0
:1 may (1)      % refers to behav :1, if "may" is behav -> logic
:2 diverge . must (2)

Tables can be found either inside a net (local table), or attached to the top level FC2 object (global table, shared by all nets)

Semantic interpretation:

The size indication is intended to ease the creation/filling of tables at parse time: the "size" specified is the effective size of the table, and not the number of entries. Indexes start at 0. Indexes appearing explicitly in entries are -real- indexes; this implies that there can be holes in a table.

Nets

The nets table is the top level structure of an FC2 file.

net\_table :  /* EMPTY */
           |  NETS INT tables labels net\_list
     ;

The integer following the nets (or N) keyword is the number of nets in the file (mandatory). The "table" and "labels" non-terminals contain the global tables, and the global label (information concerning the whole network).

Convention:

When needed, the root of the nets tree is indicated by a conventional hook of the form: hook "main">0, in which the right hand side argument of > is of type net

Each individual net contains local tables, a label, and a vertice table:

net :   NET opt\_index tables labels vertice\_table

The index of the net (integer immediately following the net keyword) is optional.

Convention:

The hook of the net usually contains an indication of its kind. The kinds currently foreseen are: "transducer", "synch_vector", "partition", "automaton" The kind of a net carries information needed to resolve some ambiguities. The default kind is "automaton".

Convention:

The initial vertex (or vertice) of an automaton or of a transducer may be indicated either in the logic field of the net label, or in the logic field of the vertex (resp. vertice) itself. Some tools (e.g. FC2Tools) require a single initial vertex to be defined.

... 
net 0 hook "automaton" struct "foo"
      logic "initial">1
      vertice 3
v s"st_0" edges 1
b"a" r1
v s"st_1" edges 1
b"b" l"initial" r2
v s"stop"

The struct field of the net label is used to encode the structure of the network (which net contains which other nets), using a "<" operator, with the name of the node as first argument, and a comma-separated list of net references as second argument:

nets 2
hook "main" "0"

net 0 hook "transducer" struct "system"<1,1,1
vertices ... 
                     % the main net is called "system", and has
                     % three identical sons, copies of net 1. 

net 1 hook "automaton" struct "cell"
                     % this one is a simple automaton named "cell"
                     % (a net with no argument)

Vertice and Edges

A vertice table is the main component of a net. The number of vertice in the table is mandatory.

vertice\_table : /* Empty */
               | VERTICE INT vertex_list
               ;
\ldots
vertex : VERTEX opt\_index label edge_table

A Vertex contains an optional index, a label, and an edges table. The number of edges in the edges table is mandatory.

edge_table : /* Empty */
           | EDGES INT edges
           ;
\ldots
edge : EDGE opt\_index label target_vertice
           | label target_vertice
           ;
target_vertice : result
           | result exp
               ;
result : ARROW | RESULT /* -> or r */
       ;

In each edge entry:

• The edge (or e) keyword is optional.
• The edge index is optional.
• The result keyword is mandatory (either r, result, or ->), and is followed by an expression of type vertex, usually a single vertex index, or a "+"-separated list of vertex indexes (e.g. ``1+2+5+6'').
• When a net has only one vertex (usual for synchronisation vectors) this index (but not the preceding result keyword) can be omitted.

v s"state1" E2       % vertex with 2 edges
e0 b?0 r1            % edge 0 has behaviour ?0 and one target vertex (number 1)
e1 b?1 r 1+2+3       % edge 1 has 3 target vertice, number 1, 2, and 3
                     %
vertex 2 struct "state2" edges 2    % another vertex, in expanded syntax
edge 0 behav ?0 -> 1
edge 1 behav !1 result 1+2+3

Declarations

The declaration section allows a specific tool to use more operators than those predefined in FC2. The syntactic class, the lexical representation, and the type of the operator must be specified.

The syntax class is one of constant, unary, prefix, infix. The difference between unary and prefix is that the latter requires parenthesis surrounding its arguments. Locally-declared infix operators should be assigned to a priority between 0 and 50.

The lexical representation must be a legal token for the FC2 scanner, that is either a SYMBOL (single character symbol) or an IDENT (fully alphabetic identifier).

The type must be coherent with the syntactic class.

declaration : decl_class decl_token decl_type
            ;
decl_class : PREFIX_DECL | UNARY_DECL | INFIX_DECL priority INT | CONSTANT_DECL
          ;
decl_token : IDENT | SYMBOL
           ;
decl_type : OP types CP ARROW type
          ;

constant diverge () -> logic
infix $ (logic logic) -> logic priority 45
prefix & (struct behav behav) -> struct