Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:transitions [2015/12/12 22:27]
marcin [Communication]
+++ — (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)\to S'$, $S-out(X.p)\to S'$, where $X.p$ is the port used for the 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.
-**in**
-**1. An active agent initialises a non-blocking communication with another active agent.**
-If $X$ is an active agents, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{W}$ | unchanged | $in(p)$ entry add to $ci(X)$ | unchanged |
-**2. An active agent initialises a blocking communication with another active agent.**
-In such a case the communication always fails and the **fail** section is executed next (if defined).
-If $X$ is an active agents, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{X}$ | $nextpc(S(X))$ | unchanged | unchanged |
-**3. An active agent calls an accessible procedure of a passive agent.**
-The result is the same for both blocking and non-blocking communication.
-If $X$ is an active agents, $X$ callas an accessible procedure $Y,q$, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{X}$ | unchanged | $proc(Y.q,p)$ entry add to $ci(X)$ | unchanged |
-^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $\mathsf{T}$ | $procpc(q)$ | $[\;]$ | unchanged |
-where $procpc(q)$ denotes the number of the first step of procedure $q$.
-**4. An active agent calls an inaccessible procedure of a passive agent (blocking version).**
-The result is the same as for the case 1.
-**5. An active agent calls an inaccessible procedure of a passive agent (non-blocking version).**
-The result is the same as for the case 2.
-FIXME
-**[[:alvis:manual|Go back]]**