# 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)

- 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
- 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.