Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:stepscounting [2015/12/01 13:13]
marcin
+++ — (current)
@@ Line 1: / Line 1: @@
-====== Steps counting ======
-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.
-<code>
-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
-      }
-    }
-  }
-}
-</code>
-**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.
-**[[:alvis:manual|Go back]]**