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.

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).

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:

If $X$ is an active agent, $S-exit(X)\to S'$, then S' is defined as follows:

If $X$ is an active agent, $S-jump(X)\to S'$, then $S'$ is defined as follows:

If $X$ is an active agent, $S-t(X)\to S'$, $t \in \{loop, null, select \}$ then $S'$ is defined as follows:

If $X$ and $Y$ are active agents, $S-start(X,Y)\to S'$, then $S'$ is defined as follows:

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:

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).

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. 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:

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:

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:

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:

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:

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:

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:

If agent Y = context(X) directly called the procedure p using port q then:

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:

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 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:

For any such passive agent Z and the active agent Z' = context(Z) we have:

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:

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:

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:

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:

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:

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

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
  }
}

Go back