Let us focus on the step idea. It is necessary to distinguish between code statements and steps. Most of the Alvis statements e.g. exec, exit, etc. are single-step statements. On the other hand, loop and select are multi-step statements. We use recursion to count the number of steps for multi-step statements. For each of them, the first step enters the statement interior. Then, we count steps of statements put inside curly brackets.

For a given statement $s$, let $stepno(s)$ denote the number of the step related to $s$. For multi-step statements, $stepno(s)$ denotes the number of the step connected with entering the statement interior.

Let us consider the piece of code shown in Listing 1. The steps number are put inside comments. For example, the step 7 denotes entering the select statement, while the step 8 denotes the out statement.

agent A {
  i :: Int = 0;
  loop {                            -- 1
    select {                        -- 2
      alt (i == 0) { 
        in p;                       -- 3 
        i = 1;                      -- 4
      }  
      alt (i == 1) { 
        in q;                       -- 5
        i = 0;                      -- 6
      }
    }
    select {                        -- 7
      alt(i == 1) {                 
        out p;                      -- 8
      }    
    }  
  }
}  

Listing 1. Steps counting in Alvis code.

To simplify the formal description of transitions, we use a function that determines the next program counter for an agent. The $nextpc$ (next program counter) function determines the number of the next step (the next program counter for an agent). The function takes an agent $X$ state as an argument and returns an integer in the range of 0 to $card(B(X))$, where $card(B(X))$ denotes the number of steps in the agent $X$ code definition ($B(X)$).

The $nextpc$ returns 0 if there is no next step.

For passive agents an auxiliary function $procpc$ will be used. The function takes a name of a procedure and returns the number of the first step of the procedure.

Go back