The production rules can be annotated with one class of invariant directives for mutual exclusion: exclhi and excllo. These check at run-time that mutual exclusion among rings of nodes is maintained throughout execution. They assume that X values of nodes are safe and do not cause violations. (Implementation note: each ring's exclusion state is actually a single boolean value, one bit of a long bit-field.) A violation of exclusion will result in the following message:
ERROR: exclhi/lo violation detected!
ring-state:
node1 : val1
node2 : val2
...
but node `$1' tried to become $2.
The simulator's excl-check-lock state is no longer coherent;
do not bother trying to continue the simulation,
but you may further inspect the state.
You probably want to disable excl-checking with `nocheckexcl'
if you wish to continue the simulation.
This just identifies participants of the ring that is violated, and the last member that tried to fire. Since the data structure for the ring locks does not support counting, you will have to disable exclusion checking with nocheckexcl to continue. Debugging the state of the simulation at the time of violation is highly recommended. (Use backtrace and why.)