Module dev.civl.mc
Package dev.civl.mc.predicate.IF

Interface Deadlock

All Superinterfaces:
CIVLStatePredicate, dev.civl.gmc.StatePredicateIF<State>
public interface Deadlock extends CIVLStatePredicate
An absolute deadlock occurs if all of the following hold:
  1. not every process has terminated
  2. no process has an enabled statement (note that a send statement is enabled iff the current number of buffered messages is less than the buffer bound).
It is to be contrasted with a "potentially deadlocked" state, i.e., one in which there may be send transitions enabled, but the send transitions can only execute if buffering is allowed, i.e., no matching receives are currently posted. Every absolutely deadlocked state is potentially deadlocked, but not necessarily vice-versa.