General system properties and design flaws

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

• At the Offer interface, the following actions may occur: offer, give, drop
• At the Take interface, the following actions may occur: thanks, take
• For the order in which these actions may occur, we consider different cases described the different LTS state diagrams below.

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)