title: Dijkstra's token termination algorithm in Promela
body: <p>My teacher has assigned us to program Dijkstra's token termination algorithm in Promela. Here is the algorithm:</p>
  
  <p>"Every node maintains a counter c. Sending a message increases c by one; the receipt of a message decreases c by one. The sum of all counters thus equals the number of messages pending in the network.
  When node 0 initiates a detection probe, it sends a token with a value 0 to node N-1. Every node i keeps the token until it becomes passive; it then forwards the token to node i-1 increasing the token value by c.
  Every node and also the token has a color (initially all white). When a node receives a message, the node turns black. When a node forwards the token, the node turns white. If a black machine forwards the token, the token turns black; otherwise the token keeps its color.
  When node 0 receives the token again, it can conclude termination, if
  node 0 is passive and white,
  the token is white, and
  the sum of the token value and c is 0.
  Otherwise, node 0 may start a new probe."</p>
  
  <p>I somewhat get the idea, but I am having trouble really understanding what is going on. If someone could help explain exactly what the algorithm is doing step-by-step, that would be great. Also, while I don't want anyone writing the code for me, any tips on how to get started would be helpful. </p>