Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:transitions [2015/12/12 23:55]
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)\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=====
-**I1. An active agent initialises a blocking communication with another active agent.**
-If $X$ is an active agent, $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 |
-**I2. An active agent initialises a non-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 agent, $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 |
-**I3. 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 agent, $X$ calls 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 added 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$.
-**I4. An active agent calls an inaccessible procedure of a passive agent (blocking version).**
-The result is the same as for the case I1.
-**I5. An active agent calls an inaccessible procedure of a passive agent (non-blocking version).**
-The result is the same as for the case I2.
-**I6. An active agent finishes a communication with another active agent.**
-The result is the same for both blocking and non-blocking communication. In case of the non-blocking communication the **success** section is executed next (if defined).
-If $X$ is an active agent, $X$ finishes a communication with agent $Y$ (port $Y.q$), parameter $v$ is the second argument of the **in** statement, $S-in(X.p)\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 | updated parameter $v$* |
-| $nextpc(S(X)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | updated parameter $v$* |
-* or **unchanged** in case of a valueless communication.
-^ ^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $nextpc(S(X)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | $out(q)$ removed from $ci(Y)$ | unchanged |
-| $nextpc(S(Y)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | unchanged |
-**I7. A passive agent collects input parameter of a procedure.**
-If $X$ is a passive agent performing procedure $p$, $v$ is the second argument of the corresponding **in** statement, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | $nextpc(S(X))$ | unchanged | updated parameter $v$* |
-* or **unchanged** in case of a valueless communication.
-**I8. A passive agent calls an accessible procedure of another passive agent.**
-The result is the same for both blocking and non-blocking communication. In case of the non-blocking communication the **success** section is executed after the procedure end (if defined).
-If $X$ is a passive agent, $X$ calls an accessible procedure $Y.q$ via its non-procedural port $X.p$, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | unchanged | $proc(Y.q,p)$ entry added to $ci(X)$ | unchanged |
-^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $\mathsf{T}$ | $procpc(q)$ | $[\;]$ | unchanged |
-**I9. A passive agent calls an inaccessible procedure of another passive agent (blocking version).**
-If $X$ is a passive agent, $X$ calls an inaccessible procedure via its non-procedural port $X.p$, $Y = context(X)$, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | unchanged | $in(p)$ entry added to $ci(X)$ | unchanged |
-^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $\mathsf{W}$ | unchanged | unchanged | unchanged |
-**I10. A passive agent calls an inaccessible procedure of another passive agent (non-blocking version).**
-If $X$ is a passive agent, $X$ calls an inaccessible procedure via its non-procedural port $X.p$, $S-in(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | $nextpc(S(X))$ | unchanged | unchanged |
-=====out=====
-**O1. An active agent initialises a blocking communication with another active agent.**
-If $X$ is an active agent, $S-out(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{W}$ | unchanged | $out(p)$ entry add to $ci(X)$ | unchanged |
-**O2. An active agent initialises a non-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 agent, $S-out(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 |
-**O3. An active agent calls an accessible procedure of a passive agent.**
-The result is the same as for the case I3.
-**O4. An active agent calls an inaccessible procedure of a passive agent (blocking version).**
-The result is the same as for the case O1.
-**O5. An active agent calls an inaccessible procedure of a passive agent (non-blocking version).**
-The result is the same as for the case O2.
-**O6. An active agent finishes a communication with another active agent.**
-The result is the same for both blocking and non-blocking communication. In case of the non-blocking communication the **success** section is executed next (if defined).
-If $X$ is an active agent, $X$ finishes a communication with agent $Y$ (port $Y.q$), parameter $v$ is the second argument of the **in** statement ($Y$ agent), $S-out(X.p)\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)$ ^
-| $nextpc(S(Y)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | $in(q)$ removed from $ci(Y)$ | updated parameter $v$* |
-| $nextpc(S(Y)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | updated parameter $v$* |
-* or **unchanged** in case of a valueless communication.
-**O7. A passive agent sends the result of a procedure.**
-If $X$ is a passive agent performing procedure $p$, $Y$ is the agent that called the procedure, $v$ is the second argument of the corresponding **in** statement ($Y$ agent), $S-out(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | $nextpc(S(X))$ | unchanged | unchanged |
-^ ^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| active agent  | $\mathsf{X}$ | unchanged | unchanged | updated parameter $v$* |
-| passive agent | $\mathsf{T}$ | unchanged | unchanged | updated parameter $v$* |
-* or **unchanged** in case of a valueless communication.
-**O8. A passive agent calls an accessible procedure of another passive agent.**
-The result is the same as for the case I8.
-**O9. A passive agent calls an inaccessible procedure of another passive agent (blocking version).**
-If $X$ is a passive agent, $X$ calls an inaccessible procedure via its non-procedural port $X.p$, $Y = context(X)$, $S-out(X.p)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{T}$ | unchanged | $out(p)$ entry added to $ci(X)$ | unchanged |
-^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $\mathsf{W}$ | unchanged | unchanged | unchanged |
-**O10. A passive agent calls an inaccessible procedure of another passive agent (non-blocking version).**
-The result is the same as for the case I10.
-=====exit=====
-The **exit** statement always finishes the corresponding procedure. It cannot be placed before the procedure **in** (**out**) statement used to collect the procedure argument (return result).
-Suppose, $Y$ is directly performing a procedure $X.p$ via port $q$ and $S-exit(X)\to S'$, then $S'$ is defined as follows:
-^ $am(X)$ ^  $pc(X)$ ^  $ci(X)$ ^  $pv(X)$ ^
-| $\mathsf{W}$ | 0 | list of accessible procedures | unchanged |
-If $Y$ is an active agent then:
-^ ^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $nextpc(S(Y)) \ne 0$ | $\mathsf{X}$ | $nextpc(S(X))$ | $proc(Y.q,p)$ removed from $ci(Y)$ | unchanged |
-| $nextpc(S(Y)) = 0$   | $\mathsf{F}$ | 0 | $[\;]$ | unchanged |
-If $Y$ is a passive agent then:
-^ $am(Y)$ ^  $pc(Y)$ ^  $ci(Y)$ ^  $pv(Y)$ ^
-| $\mathsf{T}$ | $nextpc(S(Y))$ | $proc(Y.q,p)$ removed from $ci(Y)$ | unchanged |
-After finishing a procedure a passive agent $X$ comes back to the waiting mode. However, it is possible that an agent $Z$ already called a procedure $X.p'$ that is now accessible. In such a case, in the next state **system** wakes up $Z$ and starts the procedure $X.p$.
-**See also:** [[:alvis:ltsgraphs|LTS graphs]]
-**[[:alvis:manual|Go back]]**