{"id":360,"date":"2013-08-07T09:47:04","date_gmt":"2013-08-07T07:47:04","guid":{"rendered":"https:\/\/altarica.labri.fr\/wp\/?page_id=360"},"modified":"2013-10-16T16:38:40","modified_gmt":"2013-10-16T14:38:40","slug":"leaf-nodes","status":"publish","type":"page","link":"https:\/\/altarica.labri.fr\/wp\/?page_id=360","title":{"rendered":"AltaRica : Specification of leaf nodes"},"content":{"rendered":"<p>An AltaRica <em>node<\/em> is a component of the system. Its interface with its environment is divided in two parts: <a href=\"#Events\"><em>events<\/em><\/a> and <a href=\"#Variables\"><em>flow variables<\/em><\/a>. The first ones represent actions of the environment or of the component itself, in fact any phenomenon that can change the state of the component. Second ones are shared variables that can be used to model data circulating into the system.<\/p>\n<p>Events may change the state of the component; this one is described by the mean of <em>state variables<\/em>. While flow variables may evolve according to modifications of the environment, <em>state variables <\/em>change only on occurrence of events; this means that between two events of a node the value of its state variables do not change. In the sequel, an assignment of state and flow variables is called a <em>configuration<\/em>.<\/p>\n<p>The changes of state variables on event occurrence is described using <a href=\"#Transitions\">transitions<\/a>. The relationship between flow and state variables is described by means of <a href=\"#Assertions\">assertions<\/a>.<\/p>\n<p>The description of a node starts with the keyword <code>node<\/code> and terminates with <code>edon<\/code>. The name of the node is given after the <code>node<\/code> keyword. Since a node may occur several times in a system (e.g. a switch), each <code>node<\/code> description defines a type of nodes. Actual instantiation of nodes is done in the <em>sub<\/em> section of <a title=\"AltaRica: Introducing Hierarchy\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=373\">hierarchical nodes<\/a>.<\/p>\n<pre>1 node Component \r\n2   ...\r\n3   ...\r\n4 edon<\/pre>\n<h1>Variables<\/h1>\n<p>Declarations of variables are introduced by the keywords <code>state<\/code> or <code>flow<\/code> according to the kind of declared variables. Declarations consist in a comma-separated list of identifiers followed by a colon (<code>:<\/code>) and the domain of the variables. Each declaration is terminated by a semi-colon (optional for the last one).<\/p>\n<pre>1 node A\r\n2   flow input : bool\r\n3   state memory, status : bool;\r\n4   flow output : bool\r\n5 edon<\/pre>\n<p>Generic attributes can be attached to variables. Theses attributes are simply labels that are interpreted by tools; they are given after the domain (a colon separates the domain and the list of attributes). The following example associates <em>orientation<\/em> attributes, <code>in<\/code> and <code>out<\/code> to flow variables. Remember that <code>in<\/code> and <code>out<\/code> are just labels and have no particular meaning here; the semantics of these labels is specific to each tool (e.g. the translator to the Lustre language).<\/p>\n<pre>1 node A\r\n2   flow\r\n3    a : bool : in;\r\n4    b : bool : out;\r\n5    ..\r\n6 edon<\/pre>\n<p>The <code>init<\/code> keyword introduces the initialization part of the node. Only state variables can be initialized. Remember that flow variables are shared variables thus their initial valuation can not be specified by a simple assignment. As explained below the value of flow variables depends on state variables and the environment of the node; this is also the case for their initial values. <code>init<\/code> is followed by a comma-separated list of assignments (<code>:=<\/code>) of state variables. The semantics of AltaRica nodes considers that not initialized variables may take any possible value in their domain (up to <a href=\"#Assertions\">assertions<\/a> satisfaction) at the initial state.<\/p>\n<pre>1 node Gate\r\n2   flow in, out : bool\r\n3   state closed : bool;\r\n4   init closed := true;\r\n5 edon<\/pre>\n<h1>Events<\/h1>\n<p>Events are labels used to represent state changes. The declaration of events is introduced by the keyword <code>event<\/code> followed by a comma-separated list of identifiers. Like <a href=\"#Variables\">variables<\/a> attributes can be attached to event. The following example presents a <code>switch<\/code> node with three events: <code>open<\/code>, <code>close<\/code> and <code>stuck.<\/code> Two attributes can be used to indicate that <code>open<\/code> and <code>close<\/code> are normal actions and that <code>stuck<\/code> models a failure.<\/p>\n<pre>1 node Switch\r\n2   event\r\n3     open, close : action;\r\n4     stuck : failure\r\n5 edon<\/pre>\n<p>Each node is equipped with an implicit event called \u03b5 (<em>epsilon)<\/em>. This event denotes the idleness of the node and is always possible\/enabled (see <a href=\"#Transitions\">transitions<\/a>).<\/p>\n<h1>Assertions<\/h1>\n<p>Assertions are Boolean <a title=\"AltaRica: Basics\" href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=333#Expressions\">expressions<\/a> used to describe invariants on variables. All configurations of a node must satisfy specified assertions. They are introduced by the keyword <code>assert. A<\/code>ssertions are listed using a semi-colon as separator.<\/p>\n<p>These invariants can be used to describe relations between flow variables as a transfer-function but also they model relationship between states of the node and the value of its flows. The following example describes a node that simply translates some Boolean &#8220;<code>input<\/code>&#8221; into an integer &#8220;<code>output<\/code>&#8220;.<br \/>\nThe translation of the Boolean &#8220;<code>input<\/code>&#8221; is written using an assertion that specifies that when <code>input<\/code> is true then <code>output<\/code> is 1 and 0 in the other case.<\/p>\n<pre>1 node Translate\r\n2   flow\r\n3    input : bool;\r\n4    output : [0,1];\r\n5   assert \r\n6    output = (if input then 1 else 0);\r\n7 edon<\/pre>\n<p>In the previous example, the syntax used to describe the value of <code>output<\/code> according to the one of <code>input<\/code> is quiet intuitive but it can make readers think that <code>output<\/code> is assigned the value of the <em>If-Then-Else<\/em> expression. This is not the case; assertions are just Boolean expression thus the previous assertion can be rewritten by inverting operands of the equality:<\/p>\n<pre>(if input then 1 else 0) = output;<\/pre>\n<p>or by incorporating <code>output<\/code> variable into the If-Then-Else:<\/p>\n<pre>(if input then output=1 else output=0);<\/pre>\n<p>and even by splitting the constraint in two implications:<\/p>\n<pre>input =&gt; (output=1);\r\nnot input =&gt; (output=0);<\/pre>\n<h1>Transitions<\/h1>\n<p>Transitions describe state changes. Each transition is composed by:<\/p>\n<ul>\n<li>a Boolean expression called a <em>guard<\/em> that represents a necessary condition to make the transition enabled;<\/li>\n<li>the name of the event that induces the state change;<\/li>\n<li>a list of assignments of state variables.<\/li>\n<\/ul>\n<p>Transitions are introduced by the keyword <code>trans<\/code>.<\/p>\n<p>On the occurrence of an event <em>e <\/em>in configuration<em> c<\/em>, a transition <em>t<\/em> labelled by <em>e<\/em> is said to be <em>enabled<\/em> if its <em>guard<\/em> is satisfied by <em>c<\/em> and if all <a href=\"#Assertions\">assertions<\/a> are satisfiable after the assignment of state variables. In a given configuration if a transition <em>t<\/em> is enabled then it can be triggered and the node enters some new configuration computed as follows:<\/p>\n<ol>\n<li>State variables are modified according to the transition <em>t<\/em> and not assigned state variables keep their current value;<\/li>\n<li>Assignments of flow variables are those ones that satisfies assertions.<\/li>\n<\/ol>\n<p>This semantics implies that values of flow variables only depend on state variables and not events. In the sequel remember that:<\/p>\n<ul>\n<li>state variables are modified by transitions according to the current configuration;<\/li>\n<li>flow variables are computed according to state variables and assertions.<\/li>\n<\/ul>\n<p>Below we give an example of a node that models a counter. The value of the counter is memorized into a state variable <code>counter_<\/code> and is shared with the environment using a flow variable <code>value<\/code>. The environment can modify the value of the counter using three events, <code>inc<\/code>, <code>dec<\/code> and <code>reset<\/code> that respectively increment, decrement and reset the counter.<\/p>\n<pre> 1 const CMAX = 5;\r\n 2 domain COUNTER = [0, CMAX];\r\n 3 \r\n 4 node Counter\r\n 5   flow value : COUNTER;\r\n 6   state counter_ : COUNTER;\r\n 7   event inc, dec, reset;\r\n 8   trans \r\n 9     true |- reset -&gt; counter_ := 0;\r\n10     counter_ &lt; CMAX |- inc -&gt; counter_ := counter_ + 1;\r\n11     counter_ &gt; 0 |- dec -&gt; counter_ := counter_ - 1;\r\n12   assert \r\n13     counter_ = value\r\n14 edon<\/pre>\n<p>The transitions for <code>inc<\/code> and <code>dec<\/code> are guarded in order to prevent the <code>counter_<\/code> to go out of its domain. In fact these guards are redundant with assertions implicitly introduced by the domains of variables. Since the semantics of the language enforce the new assignment of state variables to satisfy assertions the new values of state variables remain in their domain.<\/p>\n<p>An event may labels zero, one or several transitions:<\/p>\n<ul>\n<li>If no transition is specified we consider that the event can not occur (implicitly a transition guarded by <code>false<\/code> is added to the model). A tool should notify the user about such situation;<\/li>\n<li>If several transitions are specified then it is simply a non-deterministic model. For instance to model a buggy counter one can add the transition\n<pre>true |- inc -&gt; counter_ := 0<\/pre>\n<p>that resets the counter instead of increment it. Note that from a syntactic point of view the transition labelled by <code>inc<\/code> and <code>reset<\/code> can be merged as follows:<\/p>\n<pre>true |- inc, reset -&gt; counter_ := 0<\/pre>\n<\/li>\n<\/ul>\n<p>In order to handle the event \u03b5, an implicit transition is add to the node; its guard is <code>true<\/code> and it does not change state variables.<\/p>\n<h1>Examples<\/h1>\n<p>Here we give some example of AltaRica nodes and their semantics expressed as a transition system <em>&lt;S,E,T,I&gt;<\/em> where:<\/p>\n<ul>\n<li><em>S<\/em> is the set of states and contains all configurations that satisfy the assertions.<\/li>\n<li><em>E<\/em> is the set of events of the node (containing the event \u03b5).<\/li>\n<li><em>T<\/em> is the transition relation that defines configuration changes according to events. Each element of <em>T<\/em> is a vector <em>&lt;s,e,t&gt;<\/em> where <em>s<\/em> and <em>t<\/em> elements of <em>S<\/em> (i.e. they are configurations) and <em>e<\/em> is an event in <em>E<\/em>. <em>&lt;s,e,t&gt;<\/em> belongs to <em>T<\/em> iff\n<ul>\n<li>there exists a transition in the node labeled by <em>e<\/em><\/li>\n<li>this transition is enabled in the configuration <em>s<\/em><\/li>\n<li><em>t<\/em> is a valid configuration computed from the transition specification.<\/li>\n<\/ul>\n<\/li>\n<li><em>I<\/em> is the subset of initial states. A configuration belongs to <em>I<\/em> if it satisfies both the assertions and the initial assignment of state variables specified in the <code>init<\/code> section.<\/li>\n<\/ul>\n<p>We refer the reader to following papers to a formal description of the semantics:<\/p>\n<ul>\n<li>G\u00e9rald Point. <a href=\"http:\/\/tel.archives-ouvertes.fr\/tel-00353284\/fr\/\">AltaRica: Contribution \u00e0 l&#8217;unification des m\u00e9thodes formelles et de la S\u00fbret\u00e9 de fonctionnement<\/a>. Th\u00e8se de l&#8217;Universit\u00e9 Bordeaux I, 2000.<\/li>\n<li>A. Arnold, A. Griffault, G. Point and A. Rauzy. <a href=\"http:\/\/altarica.labri.fr\/pub\/publications\/altarica.pdf\">The AltaRica formalism for describing concurrent systems<\/a>. Fundam. Inf. 40, issue 2-3, pages 109-124, IOS Press, 2000.<\/li>\n<li>G. Point and A. Rauzy. AltaRica. <a href=\"http:\/\/altarica.labri.fr\/pub\/publications\/PR99b.pdf\">Constraint automata as a description language<\/a>. European Journal on Automation, 33(8-9):1033-1052, Hermes, 1999.<\/li>\n<\/ul>\n<h2>Example 1<\/h2>\n<p>The following example is the one used in <a href=\"#Assertions\">Assertions<\/a> section. It models a transfer-function translating a Boolean value into an integer one; the semantics of the node is depicted after its description. The event \u03b5 has an empty label.<\/p>\n<pre>1 node Translate\r\n2   flow\r\n3    input : bool;\r\n4    output : [0,1];\r\n5   assert \r\n6    output = (if input then 1 else 0);\r\n7 edon<\/pre>\n<p><img loading=\"lazy\" decoding=\"async\" alt=\"example1\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example1.png\" width=\"165\" height=\"120\" \/><\/p>\n<h2>Example 2<\/h2>\n<p>Here we come back on the example of a counter given in the <a href=\"#Transitions\">previous section<\/a>. In this version we have mixed the normal counter and the buggy one. The erroneous behaviour is enabled by a global Boolean constant called <code>BUGGY_COUNTER<\/code>. Below we give the semantics of the node for both values of the constant.<\/p>\n<pre> 1 const BUGGY_COUNTER = false;\r\n 2 \r\n 3 const CMAX = 5;\r\n 4 domain COUNTER = [0, CMAX];\r\n 5 \r\n 6 node Counter\r\n 7   flow value : COUNTER;\r\n 8   state counter_ : COUNTER;\r\n 9   event inc, dec, reset;\r\n10   trans \r\n11     true |- reset -&gt; counter_ := 0;\r\n12     BUGGY_COUNTER |- inc -&gt; counter_ := 0;\r\n13     counter_ &lt; CMAX |- inc -&gt; counter_ := counter_ + 1;\r\n14     counter_ &gt; 0 |- dec -&gt; counter_ := counter_ - 1;\r\n15   assert \r\n16     counter_ = value\r\n17 edon<\/pre>\n<table>\n<tbody>\n<tr>\n<td><strong>BUGGY_COUNTER=false<\/strong><\/td>\n<td><strong>BUGGY_COUNTER=true<\/strong><\/td>\n<td><\/td>\n<\/tr>\n<tr>\n<td><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-medium wp-image-449\" alt=\"example2-1\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-1-197x300.png\" width=\"197\" height=\"300\" srcset=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-1-197x300.png 197w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-1.png 215w\" sizes=\"auto, (max-width: 197px) 100vw, 197px\" \/><\/td>\n<td><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-medium wp-image-448\" alt=\"example2-2\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-2-282x300.png\" width=\"282\" height=\"300\" srcset=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-2-282x300.png 282w, https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example2-2.png 308w\" sizes=\"auto, (max-width: 282px) 100vw, 282px\" \/><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<h2>Example 3<\/h2>\n<p>The following example is a switch that directs an &#8220;<code>input<\/code>&#8221; stream to one way or another. An event called <code>push<\/code> is used to describe the action of a user. The event changes the current position <code>pos<\/code> of the switch. The assertion describes where the stream is connected. As previously the semantics of the node is given after the AltaRica code below; this time we gather all configurations that correspond to a position of the switch (i.e. <code>pos<\/code> = 0 or 1). The semantics of arrows between bundles of configurations mean that there exists a transition between each configuration of both bundles. In particular the reader should notice that transitions labelled by\u00a0\u03b5 (i.e. without label on the picture) make a loop, that means that flows of the node can change without any modification of the internal state (i.e. position) of the switch.<\/p>\n<pre> 1 node Switch\r\n 2   flow\r\n 3     i : bool;\r\n 4     o : bool[2];\r\n 5   state\r\n 6     pos : [0, 1];\r\n 7   event\r\n 8     push;\r\n 9   trans\r\n10     true |- push -&gt; pos := (pos + 1) mod 2;\r\n11   assert\r\n12     i = (if pos = 0 then o[0] else o[1]);\r\n13 edon<\/pre>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"alignnone size-full wp-image-447\" alt=\"example-3\" src=\"https:\/\/altarica.labri.fr\/wp\/wp-content\/uploads\/2013\/08\/example-3.png\" width=\"216\" height=\"188\" \/><\/p>\n","protected":false},"excerpt":{"rendered":"<p>An AltaRica node is a component of the system. Its interface with its environment is divided in two parts: events and flow variables. The first ones represent actions of the environment or of the component itself, in fact any phenomenon &hellip; <a href=\"https:\/\/altarica.labri.fr\/wp\/?page_id=360\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":25,"menu_order":3,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-360","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/360","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=360"}],"version-history":[{"count":27,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/360\/revisions"}],"predecessor-version":[{"id":572,"href":"https:\/\/altarica.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/360\/revisions\/572"}],"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=360"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}