Corrigenda

If  you detect in the book a mistake that is not mentioned below, we would appreciate if you let us know (Contact). Under Remarks, besides additional information, provided to correct encountered misunderstandings, we also list minor incoherences or flaws (to avoid annoying misunderstandings).

p. 121

In line 19 from top replace `at least one' by `the greatest' and in line 17 from top read: An example of a diffusing system is an appropriately refined version (see below p. 125) of GRAPH_LEAD_ELECT...

p. 125

To make GRAPH_LEAD_ELECT diffusing, it has to be guaranteed that any component that is enabled (via START), initially by the environment, will also START_NEIGHBors, which in turn have to PROPAGATE_START so that eventually the greatest component Max is put into mode=send. Therefore:

• on pg.125, line 1, refine START(self) by adding to mode:=send the rule START_NEIGHB(self) where START_NEIGHB(m) is defined as

  Forall q in Neighb(m) SEND(Start,to q)
  

• refine LEAD_ELECT (Fig.3.2) by adding the rule PROPAGATE_START where PROPAGATE_START is defined as

  IF Received(Start,from p) and p in Process THEN
    IF mode = terminated THEN START(self)
    CONSUME(Start,from p)

  Here Start messages are treated as GRAPH_LEAD_ELECT-internal msg so that all Neighbors of p MONITOR_RECEIVED_MSG(Start,FROM p).

  To re-initialize LEAD_ELECT for the next diffusing run, one can add analogous termination rules handling termination messages Stop (which are treated as GRAPH_LEAD_ELECT-internal msgs) as follows:

• refine REPORT_RESULT_{Diffuse} as follows:

  IF status=master AND quiescent AND AllAcksArrived THEN
    IF mode=check THEN
      TERMINATE
    IF mode=terminated THEN
      status:=idle
      SEND(computationResult,TO env)
  
  WHERE
    TERMINATE =
       TERMINATE_NEIGHB
       mode:=terminated
    TERMINATE_NEIGHB =
       Forall q in Neighb SEND(Stop,to q)

• refine LEAD_ELECT (Fig.3.2) by adding the rule PROPAGATE_TERMINATE where PROPAGATE_TERMINATE is defined as

  IF Received(Stop,from p) THEN
    IF not(mode=terminated) THEN
      TERMINATE
    CONSUME(Stop,from p)

For a detailed explanation see the slides CommunicatingAsms under Teaching Material.

p. 219 (same on p. 326)

In the GenerateRouteReply rule, the first argument of PrecursorInsertion should be the same as the seond argument of Send, namely nextHop(entryFor(origin(rreq),RT))).

We had the argument sender(rreq) in our preliminary models of AODV, where to be faithful to the requirements formulated in the given AODV document [201], we directly transcribed what is stated there, see Sect. 6.6.2. Only later we realized that this must be a mistake in the AODV document [201], but we forgot to insert the change into the rule.

The same observation has been made by the authors of reference [108], see there footnote 31 on pg.35.

p. 227:

In line 7-8 from bottom: the equivalence intends to formalize that `replicas of a same fragment may differ through their values', so that it should read:

    IF HoldsReplica(j',d,j,i) AND HoldsReplica(j*,d*,j,i) THEN
       p_{i,j,d,j'}(k) is defined IFF p_{i,j,d*,j*}(k) is defined

p. 228:

The elements of ReplicaNodes_{i,j} are declared as `pairs for given Frag_{j,i}', i.e. they satisfy HoldsReplica(j',d',j,i). This condition has been forgotten to be inserted into the formal definition of ReplicaNodes_{i,j} (first line from top).

p.237:

In SendRead/WriteResponse the implicit parameter `count' need not to be made explicit.