Go backward to A.3 The Proof Go up to A Proving Assertions

A.4 Termination

Since each program loops through a bounded number of iterations, it is clear that the execution of the network will not run forever. It is however less clear whether all node programs actually reach the termination state. In fact, this is not guaranteed: two network programs may terminate in a state where both messages are captured in the channels between them; the third node will thus wait forever on its input channels.