Errata and remarks for
AsmBook
|
Page |
Description |
|
178 |
In rule COLLECTSEQFAIL replace Ï by Î and place the update under the guard “If not consistent label(child(n))”. |
|
229 |
In rule RINGBUFFERINPUT replace “First-Last ¹N” by “not full(Buffer)”. |
|
349 |
In line 20 from the top read: the work on this program |
|
116 |
As conservative extension of the standard return for unmarked queue elements, the refined return_ref contains also the rule: If not head(queue).mark then return(head(queue)), besides If head(queue).mark then skip or return(head(queue)). |
|
94 |
In the middle of the page, read: To model requirement Op3 an additional MONITORED function is needed… |
|
97 |
In line 4 from the top, instead of CurrIn read: In |
|
102 |
In the rule for CONNECT the second guard CorrectNr(DialedSofar(s)) is not needed if one assumes that it is implied by t=subscriber(DialedSofar(s)) being true (which appears as first guard). |
|
93 |
Line 12 from the top, read: … intended sequencing of user operations, ONE RECTANGLE PER STEP. Line 15 from the top, read: This leads to the compact use case description in Fig.3.1, which will become a control state ASM through the definition of the macros given below. |
|
218 |
In the definition of `propose’ replace `nearNeighb’ by `self’ |
|
242 |
Location `timeout’ is declared as monitored, but in the definition of Retransmit on pg.243 it is used as shared: set from fals to true by the environment and set from true to false by the sender. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
. |
|
AsmBook@di.unipi.it |
March 2003 |
|
