General system properties and design flaws

We consider the following Offer-Take example where the described system has two interfaces:

Case-1: Properties: There is a single initial state and a final state, and the final state will always be reached from the initial state. Note: We always assume basic liveness, that is, if some transition is possible, some transition will be executed (after finite amount of time).


Case-2: Properties: As above, however, there is the possibility of entering a deadlock state (from which no further transition is possible), and an infinite loop without exit to the final state. Note: We assume that we want the Progress Property (also called liveness property) that the final state is always reached.


Case-3: Properties: As Case-1, however there are two loops that may be executed infinitely often, in which case the final state will not be reached.


Case-4: Properties: Similar to above, but there is no final state - instead the behavior loops back to the initial state. The behavior never stops.


Case-5: Properties: There are two loops from the initial state - in this case one may what fairness between these two possible behaviors, that is, both have always the chance to be executed again in the future. Note: This property is not implied by this state diagram.


Summary: Desired properties: Termination (final state will always be reached), infinite looping back to initial state, fairness (among different alternatives - in case of infinite looping)

Summary: Undesired properties: Deadlock, livelock (loop without any useful progress)