{"id":373,"date":"2013-08-07T10:25:20","date_gmt":"2013-08-07T08:25:20","guid":{"rendered":"https:\/\/altarica.labri.fr\/wp\/?page_id=373"},"modified":"2013-08-08T09:30:17","modified_gmt":"2013-08-08T07:30:17","slug":"altarica-introducing-hierarchy","status":"publish","type":"page","link":"https:\/\/altarica.labri.fr\/wp\/?page_id=373","title":{"rendered":"AltaRica: Specification of hierarchical models"},"content":{"rendered":"<p>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 <a title=\"AltaRica : Specification of leaf nodes\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=360\">previous section<\/a>) but they are allowed to declare <em>subnodes<\/em> and to control interactions of their interfaces i.e. interactions between their <a href=\"#Connecting_flows\">flows<\/a> and between their <a href=\"#Synchronization_of_events\">events<\/a>.<\/p>\n<h1 id=\"Subnodes\">Subnodes<\/h1>\n<p>A compound node declares its components using the <code>sub<\/code> 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:<\/p>\n<pre> 1 node A ... edon\r\n 2 \r\n 3 node B \r\n 4   sub \r\n 5     a : A;\r\n 6 edon\r\n 7 \r\n 8 node C\r\n 9   sub\r\n10     a0, a1, a2 : A;\r\n11     b, bb : B;\r\n12 edon<\/pre>\n<p>The array notation can be used to declare vectors of the same node type; for instance the node <code>C<\/code> above could be rewritten as follows:<\/p>\n<pre>1 node C\r\n2   sub\r\n3     a : A[3];\r\n4     b : B[2];\r\n5 edon<\/pre>\n<p>The size of the array must be a constant expression.<\/p>\n<h1 id=\"Initialization\">Initialization<\/h1>\n<p>A compound node can change the initial assignments of its sub-nodes; at any depth of the hierarchy. The dot notation (<code>.<\/code>) is used to specify state variables of sub-nodes. Example:<\/p>\n<pre> 1 domain D = [0,3];\r\n 2 \r\n 3 node A\r\n 4   state x : D;\r\n 5   init x := 0;\r\n 6 edon\r\n 7 \r\n 8 node B\r\n 9   sub a : A[2];\r\n10   state x : D;\r\n11   init x := 0, a[0].x := 1;\r\n12 edon\r\n13 \r\n14 node C \r\n15   sub b : B\r\n16   init b.x := 1, b.a[0].x := 3, b.a[1].x := 2;\r\n17 edon<\/pre>\n<h1 id=\"Connecting-flows\">Connecting flows<\/h1>\n<p>Flows of nodes can be <em>connected<\/em>. This concept is formalized by <code>assert<\/code>ions on flow variables of sub-nodes; by default only flows of direct sub-nodes are available. As others invariants, <em>connecting<\/em> constraints must be satisfied for all configurations of the node and its sub-nodes. The following example describe a compound node called <code>Main<\/code> that embeds 3 sub-nodes: a generator and two transfer functions. The system is represented graphically below. Assertions specified in the node <code>Main<\/code> enforces the &#8220;connection&#8221; of flows between nodes.<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"size-full wp-image-462 alignright\" style=\"background-color: #ffffff;\" alt=\"hierarchy-1\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-1.png\" width=\"250\" height=\"117\" \/><\/p>\n<pre> 1 node Generator\r\n 2   flow f : Data;\r\n 3   ...\r\n 4 edon\r\n 5 \r\n 6 node TrFunction\r\n 7   flow f : Data[2];  \r\n 8   ...\r\n 9 edon\r\n10\r\n11 node Main\r\n12   sub g : Generator\r\n13       tf : TrFunction[2];\r\n14   assert\r\n15     g.f = tf[0].f[0];\r\n16     tf[0].f[1] = tf[1].f[0];\r\n17 edon<\/pre>\n<p>As written above, compound nodes can constrain flows of sub-nodes using any kind of <a title=\"AltaRica: Basics\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=333#Expressions\">AltaRica expression<\/a>. Thus, <em>connections<\/em> are not restricted to simple equalities and even state variables of the compound node. As instance, consider a node <em>Component<\/em> having three running modes: <em>nominal<\/em>, <em>degraded<\/em> and <em>down<\/em>. Each mode can be described using a sub-component that has the same interface than the compound node.<\/p>\n<pre> 1 domain SomeDomain = ...;\r\n 2\r\n 3 node CompMode_Nominal\r\n 4 flow enabled : bool;\r\n 5      in, out : SomeDomain;\r\n 6 assert enabled =&gt; (in = out);\r\n 7 edon\r\n 8\r\n 9 node CompMode_Degraded\r\n10 flow enabled : bool;\r\n11      in, out : SomeDomain;\r\n12 ...\r\n13 edon\r\n14\r\n15 node CompMode_Down\r\n16 flow enabled : bool;\r\n17      in, out : SomeDomain;\r\n18 ...\r\n19 edon<\/pre>\n<p>Then <em>Component<\/em> enables each mode according to its own state variable <code>mode<\/code>. Finally interfaces of modes and <em>Component<\/em> are connected according to the value of the <code>mode<\/code> variable:<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-461 alignright\" style=\"background-color: #ffffff;\" alt=\"hierarchy-2\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-2-300x227.png\" width=\"300\" height=\"227\" srcset=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-2-300x227.png 300w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-2.png 390w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/p>\n<pre> 1 node Component\r\n 2   flow  in, out : SomeDomain;\r\n 3   event failure;\r\n 4   state mode : { nominal, degraded, down };\r\n 5   init  mode := nominal;\r\n 6   sub \r\n 7     nominalMode : CompMode_Nominal;\r\n 8     degradedMode : CompMode_Degraded;\r\n 9     downMode : CompMode_Down;\r\n10   trans \r\n11     mode = nominal |- failure -&gt; mode := degraded;\r\n12     mode = degraded |- failure -&gt; mode := down;\r\n13   assert\r\n14     nominalMode.enabled = (mode = nominal);\r\n15     degradedMode.enabled = (mode = degraded);\r\n16     downMode.enabled = (mode = down);\r\n17     case {\r\n18       mode = nominal  : \r\n19         in = nominalMode.in and out = nominalMode.out,\r\n20       mode = degraded  : \r\n21         in = degradedMode.in and out = degradedMode.out,\r\n22       else\r\n23         in = downMode.in and out = downMode.out\r\n24     };\r\n25 edon<\/pre>\n<h1 id=\"Synchronization-of-events\">Synchronization of events<\/h1>\n<p>The AltaRica semantics assumes the strict interleaving of events of nodes. For instance if<\/p>\n<p>we consider two nodes <em>N1<\/em> and <em>N2<\/em>, that are able to do an action <code>a<\/code> then the semantics of the system composed of <em>N1<\/em> and <em>N2<\/em> is depicted below. The interleaving is strict i.e <em>N1<\/em>.<code>a<\/code> and <em>N2<\/em>.<code>a<\/code> never occur simultaneously. One should note the presence of\u00a0\u03b5-transitions that model the fact that none of the nodes do an action.<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"size-full wp-image-460 alignright\" alt=\"hierarchy-3\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-3.png\" width=\"250\" height=\"166\" \/><\/p>\n<pre> 1 node N\r\n 2   event a;\r\n 3   state s : bool;\r\n 4   init s := true;\r\n 5   trans s |- a -&gt; s := not s;\r\n 6 edon\r\n 7 \r\n 8 node Main\r\n 9   sub \r\n10     N1, N2 : N;\r\n11 edon<\/pre>\n<p>It is possible to change the default semantics using synchronization vectors &#8220;\u00e0 la Arnold-Nivat&#8221;. 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 \u03b5. 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.<\/p>\n<p>Synchronization vectors are introduced using the <code>sync<\/code> keyword. Vectors are separated by semi-colons; each one starts with <code>&lt;<\/code> and end with <code>&gt;<\/code>. Between these delimiters events of the compound node or events of sub-nodes are given separated by commas.<\/p>\n<p>If we come back on the previous example, we can enforce the synchronism of <em>N1<\/em>.a and <em>N2<\/em>.a specifying the vector <code>&lt;<\/code> <em>N1<\/em>.a, <em>N2<\/em>.a <code>&gt;<\/code>. The semantics of the <em>synchronized<\/em> node <code>Main<\/code> is given below:<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"size-full wp-image-459 alignright\" alt=\"hierarchy-4\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/hierarchy-4.png\" width=\"130\" height=\"103\" \/><\/p>\n<pre>1 node Main\r\n2   sub \r\n3     N1, N2 : N;\r\n4   sync \r\n5     &lt;N1.a, N2.a&gt;;\r\n6 edon<\/pre>\n<p>The reader should note the non-causality between events involved in a synchronization. The intuitive semantics of <code>&lt;<\/code> <em>N1<\/em>.a, <em>N2<\/em>.a <code>&gt;<\/code> is that <em>N1<\/em>.a must occur when <em>N2<\/em>.a does but, conversely, <em>N2<\/em>.a must be present when <em>N1<\/em>.a occurs. If one of the synchronized event is impossible then the whole synchronization can not occur.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 &hellip; <a href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=373\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":25,"menu_order":4,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-373","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/373","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=373"}],"version-history":[{"count":14,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/373\/revisions"}],"predecessor-version":[{"id":486,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/373\/revisions\/486"}],"up":[{"embeddable":true,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/25"}],"wp:attachment":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=373"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}