{"id":375,"date":"2013-08-07T10:26:06","date_gmt":"2013-08-07T08:26:06","guid":{"rendered":"https:\/\/altarica.labri.fr\/wp\/?page_id=375"},"modified":"2013-08-08T10:06:46","modified_gmt":"2013-08-08T08:06:46","slug":"altarica-advanded-topics","status":"publish","type":"page","link":"https:\/\/altarica.labri.fr\/wp\/?page_id=375","title":{"rendered":"AltaRica: Advanded topics"},"content":{"rendered":"<h1 id=\"Implicit-synchronizations-with-epsilon\">Implicit synchronizations with epsilon<\/h1>\n<p>Nodes that do not appear in a synchronization vector are synchronized with the event \u03b5 (<em>epsilon<\/em>). This implicit synchronization can transform events of a node <em>N<\/em> as <em>hidden<\/em> events in the ancestor of the parent of <em>N<\/em>. To illustrate this phenomenon, consider a system with 3 levels of nodes as given below.<\/p>\n<pre> 1 node A\r\n 2   event a;\r\n 3   state x : bool;\r\n 4   trans x |- a -&gt; x := not x;\r\n 5 edon\r\n 6 \r\n 7 node B\r\n 8   sub a : A;\r\n 9   event b;\r\n10   state x : bool;\r\n11   trans x |- b -&gt; x := not x;\r\n12 edon\r\n13 \r\n14 node C\r\n15   sub b : B;\r\n16   event c;\r\n17   state x : bool;\r\n18   trans x |- c -&gt; x := not x;\r\n19 edon<\/pre>\n<p>The semantics of nodes <code>A<\/code> is straightforward (see the figure below).<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"alignnone  wp-image-480\" alt=\"advanced-1\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-1.png\" width=\"155\" height=\"58\" \/><\/p>\n<p>As explained in previous sections, the semantics of <code>B<\/code> represents the interleaving of the event <code>a<\/code> of sub-node <code>a<\/code> and the event <code>b<\/code> of <code>B<\/code>. On the figure below, <em>epsilon<\/em> events are displayed as empty labels. Actually transitions of <code>B<\/code> should be labelled by synchronization vectors of the node i.e. <code>&lt;<\/code> \u03b5, a.\u03b5 <code>&gt;<\/code>, <code>&lt;<\/code> \u03b5, a.a <code>&gt;<\/code> and <code>&lt;<\/code> b, a.\u03b5 <code>&gt;<\/code>.<\/p>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-medium wp-image-479\" alt=\"advanced-2\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-2.png\" width=\"300\" height=\"90\" \/><\/p>\n<p>Now, consider the case of node <code>C<\/code>. Implicit vectors of <code>C<\/code> are analog to the ones of <code>B<\/code>: <code>&lt;<\/code> \u03b5, b.<em>\u03b5<\/em> <code>&gt;<\/code>, <code>&lt;<\/code> \u03b5, b.b <code>&gt;<\/code> and <code>&lt;<\/code> c, b.\u00a0\u03b5 <code>&gt;<\/code>. The transitivity of the synchronization implies that the actual synchronization vectors for the whole model are:<\/p>\n<ul>\n<li><code>&lt;<\/code> \u03b5, <code>&lt;<\/code> b.b, b.a.\u03b5 <code>&gt; &gt;<\/code><\/li>\n<li><code>&lt;<\/code> c, <code>&lt;<\/code> b.\u03b5, b.a.a <code>&gt; &gt;<\/code><\/li>\n<li><code>&lt;<\/code> c, <code>&lt;<\/code> b.\u03b5, b.a.\u03b5 <code>&gt; &gt;<\/code><\/li>\n<li><code>&lt;<\/code> \u03b5, <code>&lt;<\/code> b.\u03b5, b.a.a <code>&gt; &gt;<\/code><\/li>\n<li><code>&lt;<\/code> \u03b5, <code>&lt;<\/code> b.\u03b5, b.a.\u03b5 <code>&gt; &gt;<\/code><\/li>\n<\/ul>\n<p>These vectors yield to the following semantics of the node <code>C<\/code>:<br \/>\n<a href=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-3.png\"><img loading=\"lazy\" decoding=\"async\" width=\"600\" height=\"178\" class=\"alignnone size-medium wp-image-478\" alt=\"advanced-3\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-3.png\" srcset=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-3.png 600w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-3-300x89.png 300w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/advanced-3-500x148.png 500w\" sizes=\"auto, (max-width: 600px) 100vw, 600px\" \/><\/a><\/p>\n<h1 id=\"Visibility-attributes\">Visibility attributes<\/h1>\n<p>AltaRica descriptions must respect some visibility rules applied to variables and events. Default rules are given below:<\/p>\n<ul>\n<li>A subnode does not known events or variables existing in its parent node. This rule is guaranteed by the order of declaration of nodes.<\/li>\n<li>A compound node can constrain only flow variables and events of its declared subnodes.<\/li>\n<li>A compound node can change the initial values of all state variables at any depth in its hierarchy.<\/li>\n<\/ul>\n<p>Default rules can be bypassed using <em>visibility attributes<\/em> that can be applied to events or variables:<\/p>\n<ul>\n<li><code>private<\/code> means that the object is visible only by the node that has declared it.<\/li>\n<li><code>parent<\/code> means that the object is also visible by the parent node.<\/li>\n<li><code>public<\/code> means that the object is visible by all ancestors.<\/li>\n<\/ul>\n<p>Using these attributes, default visibility rules can be summarized as follows: state variables are assigned the <code>private<\/code> attribute (except for initialization), events and flow variables are assigned <code>parent<\/code>.<\/p>\n<p>While <code>public<\/code> variables are visible at the top-level of the AltaRica model hierarchy, the <code>public<\/code> attribute of events is removed at the level of the first explicit synchronization. Example:<\/p>\n<pre> 1 node A\r\n 2   event e : public;\r\n 3 edon\r\n 4 \r\n 5 node B\r\n 6   sub a : A;\r\n 7   event f;\r\n 8 edon\r\n 9 \r\n10 node C\r\n11   sub b1, b2 : B;\r\n12   sync &lt;b1.f, b2.a.e&gt;; \/\/ authorized\r\n13 edon<\/pre>\n<p>Synchronized events can not have a common prefix. For instance on the next example, the node <code>C<\/code> can not synchronize <code>b1.f<\/code> and <code>b1.a.e<\/code>; the following synchronization is thus forbidden:<\/p>\n<pre> 1 node A\r\n 2   event e : public;\r\n 3 edon\r\n 4 \r\n 5 node B\r\n 6   sub a : A;\r\n 7   event f;\r\n 8   sync &lt;f, a.e&gt;; \r\n 9 edon\r\n10 \r\n11 node C\r\n12   sub b1, b2 : B;\r\n13   sync &lt;b1.f, b2.a.e&gt;; \/\/ not authorized because 'a.e'\r\n14                        \/\/ is not an event of the interface of b2.\r\n15 edon<\/pre>\n<h1 id=\"Priorities\">Priorities<\/h1>\n<p>AltaRica language permits to specify priorities between events. In a given configuration, if two events are possible then only the one having the highest priority can actually occur. Priorities are locally defined in a node by a partial order on events. If two events are incomparable w.r.t the specification then they are both possible.<\/p>\n<p>The declaration of events and the specification of the partial order can be mixed; for the sake of clarity, one should prefer to define the order after the declaration of events.<\/p>\n<pre><code>1 node Component;\r\n2   event a, b;\r\n3         a &lt; b; \/\/ only this line is actually necessary to declare a and b\r\n4   ...\r\n5 edon\r\n<\/code><\/pre>\n<p>The syntax of partial order uses comparators <code>&lt;<\/code> and <code>&gt;<\/code>. Both sides of these comparators can be either simple events or sets of events enclosed between braces. The following specifications are equivalent:<\/p>\n<ul>\n<li><code>a &lt; c<\/code>, <code>a &lt; d<\/code>, <code>b &lt; c<\/code>, <code>b &lt; d<\/code><\/li>\n<li><code>{ a, b } &lt; c<\/code>, <code>{ a, b } &lt; d<\/code>,<\/li>\n<li><code>a &lt; { c, d }<\/code>, <code>b &lt; { c, d }<\/code><\/li>\n<li><code>{ a, b } &lt; { c, d }<\/code><\/li>\n<\/ul>\n<p>The partial order is applied to the <ins>semantics<\/ins> of the node i.e. it takes into account assertions and the hierarchy. Priorities are just a syntactic sugar for leaf nodes because the order can be integrated into guards of transitions. For compound nodes, the order is applied after synchronization of subnodes, thus priorities define in fact an order on<br \/>\nsynchronization vector based on events of the hierarchical node. Compound nodes can be viewed as controllers that constrain their subnodes using: assertions, synchronizations and priorities.<\/p>\n<h1 id=\"Weak-synchronizations\">Weak synchronizations<\/h1>\n<p><a title=\"AltaRica: Specification of hierarchical models\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=373#Synchronization_of_events\">Synchronization<\/a> vectors defined (implicitly or explicitly) in a node are allowed combination of events. A combination can occur in the system if all components of the vector are possible; thus, if just one of the component is inhibited for some reason the vector can not happen.<\/p>\n<p>Using this synchronization mechanism, the modelling of a broadcast phenomenon or a common failure mode becomes tricky and not natural because if some events are missing the synchronized event can not occur. For this reason, the AltaRica language permits to write <em>weak synchronization vectors<\/em> (usual vectors are called <em>strong<\/em>). Syntactically it just consists in adding question-marks (<code>?<\/code>) to events.<\/p>\n<p>The semantics of weak vectors is the following:<\/p>\n<ul>\n<li>each event marked with a question-mark is not mandatory for the synchronization;<\/li>\n<li>if a marked event is possible then it <span style=\"text-decoration: underline;\">should<\/span> participate to the synchronization;<\/li>\n<li>a marked event that does not participate to the synchronization is replaced by \u03b5.<\/li>\n<\/ul>\n<p>In a given configuration, the synchronizations that occur are those that maximize the number of enabled marked events. The way this semantics is formalized is to consider that each weak vector induces a set of <em>strong vectors<\/em> that encode all the possible combinations of marked events. This set is then partially ordered by the inclusion ordering. For instance,\u00a0the vector <code>&lt; a?, b?, c? &gt;<\/code> induces the following lattice:<\/p>\n<p><a href=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/lattice.png\"><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-488 aligncenter\" alt=\"lattice\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/lattice-300x201.png\" width=\"300\" height=\"201\" srcset=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/lattice-300x201.png 300w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/lattice-446x300.png 446w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/lattice.png 661w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a>Given this set of vectors and the partial order on this set the standard semantics with priorities is applied. Note that the order on vectors is applied prior to the order on local events of the compound nodes.<\/p>\n<p>The language proposes additional notations to manipulate the lattice.<\/p>\n<ul>\n<li>Constraints on the number of marked events can be specified (<em>&gt; n<\/em>, <em>&lt; n<\/em>, <em>&gt;= n<\/em>, <em>&lt;= n<\/em>, <em>= n<\/em>) to enforce a given cardinality of possible marked events. For instance if <em>&gt;= 1<\/em> means that at <em>least<\/em> one marked event has to participate to the synchronization.<\/li>\n<li><code>min<\/code> and <code>max<\/code> keywords specified at the end of the vector indicates that the synchronization has to use a minimal or a maximal number of marked events (by default <code>max<\/code> is used).<\/li>\n<\/ul>\n<h1 id=\"Abstract-data-types\">Abstract data types<\/h1>\n<p>Since <a href=\"http:\/\/www.labri.fr\/perso\/herbrete\/persee\/persee.php\">ACI Pers\u00e9e<\/a>, the language supports the use of <em>abstract<\/em> data types. These types are given after a <code>sort<\/code> keyword followed by a comma-separated list of type identifiers. Example:<\/p>\n<pre><code>1 sort MESSAGE, QUEUE;\r\n<\/code><\/pre>\n<p>Once declared, these types can be used as others; in particular abstract constants can be defined:<\/p>\n<pre><code>1 const ACK_OK : MESSAGE;\r\n2 const ACK_NOK : MESSAGE;\r\n3 const MSG_DATA : MESSAGE;\r\n<\/code><\/pre>\n<p>In order to manipulate variables and constants defined with an abstract type, signatures of functions can be declared. A signature is introduced by the <code>sig<\/code> keyword followed by the identifier of the function, a colon and input and output types of the function; the input type can be a Cartesian product given as star-separated list of types. Example:<\/p>\n<pre><code>1 sig push : QUEUE * MESSAGE -&gt; QUEUE;\r\n2 sig top : QUEUE -&gt; MESSAGE;\r\n3 sig pop : QUEUE -&gt; QUEUE;\r\n4 sig is_empty : QUEUE -&gt; bool;\r\n<\/code><\/pre>\n<p>Abstract types, constants and signatures can be used in any AltaRica expression. Up to now only <a title=\"ARC\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=32\">ARC<\/a> supports this extension and this support is limited to the flat semantics of nodes.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Implicit synchronizations with epsilon Nodes that do not appear in a synchronization vector are synchronized with the event \u03b5 (epsilon). This implicit synchronization can transform events of a node N as hidden events in the ancestor of the parent of &hellip; <a href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=375\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":25,"menu_order":5,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-375","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/375","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=375"}],"version-history":[{"count":9,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/375\/revisions"}],"predecessor-version":[{"id":489,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/375\/revisions\/489"}],"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=375"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}