deadlocksobs: find dead- or live-locked states with observations

deadlocksobs A;


A state is deadlocked if after reaching it no observable action will ever be possible. This definition follows Milner's book, but includes what is often known as livelock.

For each such state, we give one sequence of observable actions by which it may be reached (just one, even if there are many ways of reaching that state).



See also

  • deadlocks
  • findinit
  • findinitobs
    Edinburgh Concurrency Workbench (v7.1). Page generated: Sun Jul 18 11:46:51 BST 1999