# AltaRica: Specification of hierarchical models

The AltaRica language permits to describe systems in a bottom-up manner. Elementary components can be composed to form complex equipments with their own interfaces and behaviours. The hierarchical nodes are described like the other ones (see the previous section) but they are allowed to declare subnodes and to control interactions of their interfaces i.e. interactions between their flows and between their events.

# Subnodes

A compound node declares its components using the `sub` keyword. The syntax is similar to the one used for the declaration of variables: a comma-separated list of subnodes identifiers followed by a semi-colon and a type of nodes. Subnodes can be hierachical ones. Example:

``` 1 node A ... edon
2
3 node B
4   sub
5     a : A;
6 edon
7
8 node C
9   sub
10     a0, a1, a2 : A;
11     b, bb : B;
12 edon```

The array notation can be used to declare vectors of the same node type; for instance the node `C` above could be rewritten as follows:

```1 node C
2   sub
3     a : A[3];
4     b : B[2];
5 edon```

The size of the array must be a constant expression.

# Initialization

A compound node can change the initial assignments of its sub-nodes; at any depth of the hierarchy. The dot notation (`.`) is used to specify state variables of sub-nodes. Example:

``` 1 domain D = [0,3];
2
3 node A
4   state x : D;
5   init x := 0;
6 edon
7
8 node B
9   sub a : A[2];
10   state x : D;
11   init x := 0, a[0].x := 1;
12 edon
13
14 node C
15   sub b : B
16   init b.x := 1, b.a[0].x := 3, b.a[1].x := 2;
17 edon```

# Connecting flows

Flows of nodes can be connected. This concept is formalized by `assert`ions on flow variables of sub-nodes; by default only flows of direct sub-nodes are available. As others invariants, connecting constraints must be satisfied for all configurations of the node and its sub-nodes. The following example describe a compound node called `Main` that embeds 3 sub-nodes: a generator and two transfer functions. The system is represented graphically below. Assertions specified in the node `Main` enforces the “connection” of flows between nodes.

``` 1 node Generator
2   flow f : Data;
3   ...
4 edon
5
6 node TrFunction
7   flow f : Data[2];
8   ...
9 edon
10
11 node Main
12   sub g : Generator
13       tf : TrFunction[2];
14   assert
15     g.f = tf[0].f[0];
16     tf[0].f[1] = tf[1].f[0];
17 edon```

As written above, compound nodes can constrain flows of sub-nodes using any kind of AltaRica expression. Thus, connections are not restricted to simple equalities and even state variables of the compound node. As instance, consider a node Component having three running modes: nominal, degraded and down. Each mode can be described using a sub-component that has the same interface than the compound node.

``` 1 domain SomeDomain = ...;
2
3 node CompMode_Nominal
4 flow enabled : bool;
5      in, out : SomeDomain;
6 assert enabled => (in = out);
7 edon
8
10 flow enabled : bool;
11      in, out : SomeDomain;
12 ...
13 edon
14
15 node CompMode_Down
16 flow enabled : bool;
17      in, out : SomeDomain;
18 ...
19 edon```

Then Component enables each mode according to its own state variable `mode`. Finally interfaces of modes and Component are connected according to the value of the `mode` variable:

``` 1 node Component
2   flow  in, out : SomeDomain;
3   event failure;
4   state mode : { nominal, degraded, down };
5   init  mode := nominal;
6   sub
7     nominalMode : CompMode_Nominal;
9     downMode : CompMode_Down;
10   trans
11     mode = nominal |- failure -> mode := degraded;
12     mode = degraded |- failure -> mode := down;
13   assert
14     nominalMode.enabled = (mode = nominal);
16     downMode.enabled = (mode = down);
17     case {
18       mode = nominal  :
19         in = nominalMode.in and out = nominalMode.out,
20       mode = degraded  :
21         in = degradedMode.in and out = degradedMode.out,
22       else
23         in = downMode.in and out = downMode.out
24     };
25 edon```

# Synchronization of events

The AltaRica semantics assumes the strict interleaving of events of nodes. For instance if

we consider two nodes N1 and N2, that are able to do an action `a` then the semantics of the system composed of N1 and N2 is depicted below. The interleaving is strict i.e N1.`a` and N2.`a` never occur simultaneously. One should note the presence of ε-transitions that model the fact that none of the nodes do an action.

``` 1 node N
2   event a;
3   state s : bool;
4   init s := true;
5   trans s |- a -> s := not s;
6 edon
7
8 node Main
9   sub
10     N1, N2 : N;
11 edon```

It is possible to change the default semantics using synchronization vectors “à la Arnold-Nivat”. Elements of these vectors are events and its semantics enforces all its components to occur at the same time. Subnodes that are not listed in a vector are assumed to be synchronized using the event ε. Several vectors can be specified and an event can occur in several vectors. If a vector is specified then the default semantics for listed events is replaced by the semantics of the vector.

Synchronization vectors are introduced using the `sync` keyword. Vectors are separated by semi-colons; each one starts with `<` and end with `>`. Between these delimiters events of the compound node or events of sub-nodes are given separated by commas.

If we come back on the previous example, we can enforce the synchronism of N1.a and N2.a specifying the vector `<` N1.a, N2.a `>`. The semantics of the synchronized node `Main` is given below:

```1 node Main
2   sub
3     N1, N2 : N;
4   sync
5     <N1.a, N2.a>;
6 edon```

The reader should note the non-causality between events involved in a synchronization. The intuitive semantics of `<` N1.a, N2.a `>` is that N1.a must occur when N2.a does but, conversely, N2.a must be present when N1.a occurs. If one of the synchronized event is impossible then the whole synchronization can not occur.