previous up next
Go backward to A.3 The Proof
Go up to A Proving Assertions
RISC-Linz logo

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.


Maintainer: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next