Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- alvis:transitions [2015/12/12 22:00]
marcin
+++ — (current)
@@ Line 1: / Line 1: @@
-====== Steps (transitions) ======
-The set of all possible steps for untimed models with $\alpha^0$ system layers contains the following elements:
-  * //exec// -- performs an evaluation and assignment;
-  * //exit// -- terminates an agent or a procedure,
-  * //in// -- performs communication (input side),
-  * //jump// -- jumps to a label,
-  * //loop// -- enters a loop,
-  * //null// -- performs an empty statement,
-  * //out// -- performs communication (output side),
-  * //select// -- enters a select statement,
-  * //start// -- starts an inactive agent.
-====== Enable steps (active agents) ======
-**Definition 1.** Assume $\mathbf{A} = (D, B, \alpha^0)$ is an Alvis model with the current state $S$ and $X$ be an active agent. A step $t$ is **enable** in the state $S$ **with respect to** $X$ (denoted as $S-t(X)\to$) iff:
-  * $X$ is in the **running** mode;
-  * the program counter points out step $t$;
-  * $X$ has not called a procedure.
-Sometimes, an extended version of this notation is used:
-  * $S-start(X,Y)\to S'$, where $Y$ is the argument of the corresponding **start** statement.
-  * $S-in(X.p,T)\to S'$, $S-out(X.p,T)\to S'$, where $X.p$ is the port used for the communication and $T$ is the type of send/collected value (the special **Empty** type is used to denote a valueless communication).
-===== exec =====
-If $X$ is an active agent, $S-exec(X)\to S'$, and a parameter $v$ is assigned a value $a$ with the corresponding //exec// statement, then $S'$ is defined as follows:
-^ ^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $nextpc(S(X)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | unchanged | updated parameter $v$ |
-| $nextpc(S(X)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | updated parameter $v$ |
-===== exit =====
-If $X$ is an active agent, $S-exit(X)\to S'$, then //S//' is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{F}$ | 0 | $[\;]$ | unchanged |
-===== jump =====
-If $X$ is an active agent, $S-jump(X)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{X}$ | $nextpc(S(X))$ | unchanged | unchanged |
-===== loop, null, select =====
-If $X$ is an active agent, $S-t(X)\to S'$, $t \in \{loop, null, select \}$ then $S'$ is defined as follows:
-^ ^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $nextpc(S(X)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | unchanged | unchanged |
-| $nextpc(S(X)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | unchanged |
-===== start =====
-If $X$ and $Y$ are active agents, $S-start(X,Y)\to S'$, then $S'$ is defined as follows:
-^ ^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $nextpc(S(X)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | unchanged | unchanged |
-| $nextpc(S(X)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | unchanged |
-^ ^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $Y$ in //init// mode | $\mathsf{X}$ | 1 | $[\;]$ | unchanged |
-| $Y$ not in //init// mode | unchanged | unchanged | unchanged | unchanged |
-====== Enable steps (passive agents) ======
-**Definition 2.** Assume $\mathbf{A} = (D, B, \alpha^0)$ is an Alvis model with the current state $S$, $X$ is an agent (active or passive) and $Y$ is a passive agent.
-  * We say that $X$ is **directly performing input procedure** $Y.q$ via  port $X.p$ iff $(X.p, Y.q) \in \mathcal{C}$ and $proc(Y.q, p) \in ci_S(X)$.
-  * We say that $X$ is **directly performing output procedure** $Y.q$ via  port $X.p$ iff $(Y.q, X.p) \in \mathcal{C}$ and $proc(Y.q, p) \in ci_S(X)$.
-  * We say that $X$ is **indirectly performing input procedure** $Y.q$ iff exist agents $Y_1,\dots,Y_m$, $m > 1$ such that $X$ is performing a procedure of $Y_1$, $Y_1$ is performing a procedure of $Y_2$,..., $Y_m$ is performing input  procedure $Y.q$ via one of its ports.
-  * We say that $X$ is **indirectly performing output procedure** $Y.q$ iff exist agents $Y_1,\dots,Y_m$, $m > 1$ such that $X$ is performing a procedure of $Y_1$, $Y_1$ is performing a procedure of $Y_2$,..., $Y_m$ is performing output  procedure $Y.q$ via one of its ports.
-  * For any passive agent $Y$ performing one of its procedures, $context(Y)$ denotes the active agent $X$ that is performing the procedure directly or indirectly.
-**Definition 3.** Assume $\mathbf{A} = (D, B, \alpha^0)$ is an Alvis model with the current state $S$, $X$ is an active agent, $Y$ is a passive agent, $am_S(Y) = \mathsf{T}$ and $context(Y) = X$. A step $t$ is **enable** in the state $S$ **with respect to** $Y$ iff:
-  * $X$ is in the **running** mode;
-  * the program counter of $Y$ points out step $t$;
-  * $Y$ has not called a procedure.
-Results of steps performing for passive agents are defined similarly as for active ones. For example, if $X$ is a passive agent, $S-exec(X)\to S'$,  a parameter $v$ is assigned a value $a$ with the **exec** statement, then the state $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | $nextpc(S(X))$ | unchanged | updated parameter $v$ |
-The **exec** statement cannot be the last one in the corresponding procedure block, so we do not need to consider two cases as previously.
-The **exit** statement always finishes the corresponding procedure. It cannot be placed before the procedure **in** or **out** statement used to collect the procedure argument (return result).
-====== Communication ======
-A communication between two active agents can be initialised by any of them. The agent that initialises it, performs the **out** statement to provide some information and waits for the second agent to take it, or performs the **in** statement to express its readiness to collect some information and waits until the second agent provides it.
-A communication with a passive agent is treated as a procedure call. It can be initialised either by an active agent or by a passive one from inside of its procedure. In case of an input procedure (a parameter is sent to the corresponding passive agent), it is called with the **out** statement. After a procedure is started, its performs its statements. It is necessary to put the **in** statement as one of them - the statement is used to collect the parameter, but it is not necessary to put the statement as the first procedure step.
-Similarly, in case of an output procedure, it is called with the **in** statement. It is necessary to put the **out** statement as one of its statements. It is used to provide the result, but it is not necessary to put the statement at the end of the procedure. In any case, a procedure is finished if the **exit** statement has been performed. The **exit** statement can be used only after the **in/out** statement that corresponds to the procedure call.
-FIXME
-**in**
-**1.** If //X// is an active agent, //Y// is a passive agent, //S//--//in//(//X.p//, //T//)->//S//' and the accessible procedure //Y.q// is called, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **X** | unchanged | add //proc//(//Y.q//, //p//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **T** | //procpc//(//q//) | [] | unchanged |
-**2.** If //X// and //Y// are passive agents, //S//--//in//(//X.p//, //T//)->//S//' and the accessible procedure //Y.q// is called, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **T** | unchanged | add //proc//(//Y.q//, //p//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **T** | //procpc//(//q//) | [] | unchanged |
-**3.** If //X// and //Y// are active agents, //S//--//in//(//X.p//, //T//)->//S//' to finish the communication with //Y// (i.e. //Y// has already executed the //out// step using port //q// and is in the //waiting// mode), and a parameter //v// of //X// is assigned a value //a// (sent from //Y//), then //S//' is defined as follows:
-^ ^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| //nextpc//(//S//(//X//)) ≠ 0 | **X** | //nextpc//(//S//(//X//)) | unchanged | updated parameter //v// |
-| //nextpc//(//S//(//X//)) = 0 | **F** | 0 | [] | updated parameter //v// |
-^ ^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| //nextpc//(//S//(//Y//)) ≠ 0 | **X** | //nextpc//(//S//(//Y//)) | remove //out//(//q//%%|%%//T//) entry | unchanged |
-| //nextpc//(//S//(//Y//)) = 0 | **F** | 0 | [] | unchanged |
-**4.** If //X// is an active agent, //S//--//in//(//X.p//, //T//)->//S//' and there is no other agent (active or passive) to finish the communication, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **W** | unchanged | add //in//(//p//%%|%%//T//) entry | unchanged |
-In any considered case, if the port //p// is used to collect values of one type only, then the //in//(//p//) entry is used instead of //in//(//p//|//T//).
-**5.** If //X// is a passive agent, //Y// = //context//(//X//), //S//--//in//(//X.p//, //T//)->//S//', //p// is not a procedural port i.e. //X// calls a procedure of another passive agent, and the procedure is not accessible, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **T** | unchanged | add //in//(//p//%%|%%//T//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **W** | unchanged | unchanged | unchanged |
-**6.** Suppose //X// is a passive agent, //Y// = //context//(//X//), //S//--//in//(//X.p//, //T//)->//S//', //p// is the procedural port i.e. the procedure collects its input parameter. Let //v// be the second argument of the corresponding **in** statement and a value //a// was sent while the procedure call. If the **in** statement is not the last procedure statement then:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **T** | //nextpc//(//S//(//X//)) | unchanged | updated parameter //v// |
-//S//'(//Y//) = //S//(//Y//)
-If the **in** statement is the last procedure statement then the procedure is finished. Thus the new state //S//' for //X// should be defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **W** | 0 | list of accessible procedures | updated parameter //v// |
-If agent //Y// = //context//(//X//) directly called the procedure //p// using port //q// then:
-^ ^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| //nextpc//(//S//(//Y//)) ≠ 0 | **X** | //nextpc//(//S//(//Y//)) | remove //proc//(//X.p//, //q//) entry | unchanged |
-| //nextpc//(//S//(//Y//)) = 0 | **F** | 0 | [] | unchanged |
-If agent //Y// = //context//(//X//) indirectly called the procedure //p//, a passive agent //Y//' directly called the procedure //p// using port //q//, and calling //p// was not the last step of the corresponding //Y//' procedure then:
-^ //am//(//Y//') ^  //pc//(//Y//') ^  //ci//(//Y//') ^  //pv//(//Y//') ^
-| **T** | //nextpc//(//S//(//Y//')) | remove //proc//(//X.p//, //q//) entry | unchanged |
-//S//'(//Y//) = //S//(//Y//)
-If calling //p// was the last step of the corresponding //Y//' procedure then the procedure is finished and the new state for //Y//' is generated in similar way as for //X//.
-However, there may exist another agents that //potentially called// a procedure of //X// that is now accessible in //S//'.
-The term //potentially called// means that it is possible that port //Z.q// is connected with a few ports and the communication via this port can be finalised as a communication with another active agent or another passive one (different than //X//). When performing of a procedure //X.p// is finished, guards of all procedures of //X// are evaluated and a set of available procedures is received. If at least one of them has been already potentially called i.e. then //X// starts another procedure immediately.
-For more details see: Szpyrka M., Matyasik P., Mrówka R., Kotulski L.: //Formal description of Alvis language with α^0 system layer//. Fundamenta Informaticae, vol. 129, 2014, pp. 161-176 [[:alvis:bibtex|bibtex]]
-Besides agents that potentially called one of //X// accessible procedures, there may exist agents that are waiting for accessibility of //X// procedures in order to fulfil their **select** statements guards. Thus, if the set of potentially called procedures is empty, them we consider states of agents that are waiting due to their select guards and the accessibility of //X// procedures in //S//'
-makes at least one branch of the corresponding **select** statement open.
-For any such active agent //Z// we have:
-^ //am//(//Z//) ^  //pc//(//Z//) ^  //ci//(//Z//) ^  //pv//(//Z//) ^
-| **X** | //nextpc//(//S//(//Z//)) | remove //guard// entry | unchanged |
-For any such passive agent //Z// and the active agent //Z//' = //context//(//Z//) we have:
-^ //am//(//Z//) ^  //pc//(//Z//) ^  //ci//(//Z//) ^  //pv//(//Z//) ^
-| **T** | //nextpc//(//S//(//Z//)) | remove //guard// entry | unchanged |
-^ //am//(//Z//') ^  //pc//(//Z//') ^  //ci//(//Z//') ^  //pv//(//Z//') ^
-| **X** | unchanged | unchanged | unchanged |
-**out**
-**1.** If //X// is an active agent, //Y// is a passive agent, //S//--//out//(//X.p//, //T//)->//S//' and the accessible procedure //Y.q// is called, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **X** | unchanged | add //proc//(//Y.q//, //p//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **T** | //procpc//(//q//) | [] | unchanged |
-**2.** If //X// and //Y// are passive agents, //S//--//out//(//X.p//, //T//)->//S//' and the accessible procedure //Y.q// is called, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **T** | unchanged | add //proc//(//Y.q//, //p//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **T** | //procpc//(//q//) | [] | unchanged |
-**3.** If //X// and //Y// are active agents, //S//--//out//(//X.p//, //T//)->//S//' to finish the communication with //Y// (i.e. //Y// has already executed the //in// step using port //q// and is in the //waiting// mode), and a parameter //v// of //Y// is assigned a value //a// (sent from //X//), then //S//' is defined as follows:
-^ ^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| //nextpc//(//S//(//X//)) ≠ 0 | **X** | //nextpc//(//S//(//X//)) | unchanged | unchanged |
-| //nextpc//(//S//(//X//)) = 0 | **F** | 0 | [] | unchanged |
-^ ^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| //nextpc//(//S//(//Y//)) ≠ 0 | **X** | //nextpc//(//S//(//Y//)) | remove //in//(//q//%%|%%//T//) entry | updated parameter //v// |
-| //nextpc//(//S//(//Y//)) = 0 | **F** | 0 | [] | updated parameter //v// |
-**4.** If //X// is an active agent, //S//--//out//(//X.p//, //T//)->//S//' and there is no other agent (active or passive) to finish the communication, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **W** | unchanged | add //out//(//p//%%|%%//T//) entry | unchanged |
-In any considered case, if the port //p// is used to send values of one type only, then the //out//(//p//) entry is used instead of //out//(//p//|//T//).
-**5.** If //X// is a passive agent, //Y// = //context//(//X//), //S//--//out//(//X.p//, //T//)->//S//', //p// is not a procedural port i.e. //X// calls a procedure of another passive agent, and the procedure is not accessible, then //S//' is defined as follows:
-^ //am//(//X//) ^  //pc//(//X//) ^  //ci//(//X//) ^  //pv//(//X//) ^
-| **T** | unchanged | add //out//(//p//%%|%%//T//) entry | unchanged |
-^ //am//(//Y//) ^  //pc//(//Y//) ^  //ci//(//Y//) ^  //pv//(//Y//) ^
-| **W** | unchanged | unchanged | unchanged |
-**6.** Suppose //X// is a passive agent, //Y// = //context//(//X//), //S//--//out//(//X.p//, //T//)->//S//', //p// is the procedural port i.e. the procedure sends its result. Let //v// be the second argument of the corresponding **out** statement and a value //a// is sent. This case is similar to the case **6** of **in**, but the parameters value list that is updated belongs to the agent that called the corresponding procedure.
-**Example**
-{{:alvis:alvis2.png|}}
-<code>
-agent X1 {
-  loop {          -- 1
-    out p;        -- 2
-  }
-}
-agent X2 {
-  proc q1 {
-    in q1;        -- 1
-    out q2        -- 2
-  }
-}
-agent X3 {
-  proc r {
-    in r;         -- 1
-    null;         -- 2
-  }
-}
-</code>
-{{:alvis:alvis2lts.png|}}
-**[[:alvis:manual|Go back]]**