Sidebar

Main

Internal

Trace:

Differences

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

--- alvis:stepscounting [2013/12/31 10:58]
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, **if**, **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 **if** 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
-      }
-    }
-    if(i == 1) {                    -- 7
-      out p;                        -- 8
-    }
-    else {
-      null;                         -- 9
-    }
-  }
-}
-</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//)).
-**[[:alvis:manual|Go back]]**