0.5 Using temporal logic to specify properties  (Page 9/11)

For our simple producer/consumer model, what is the basic property we'd like to guarantee?Roughly, ``each product is consumed exactly once''. That is, Produce and Consume are called alternatingly,starting with Produce. (In particular, as stated this precludes modeling``produce twice and queue the results''.)

Expressing this actually requires several clauses. Give colloquial English translations of the followingLTL formulas. We can make the generic model a bit concrete byinterpreting $\mathrm{startProduce}$ and $\mathrm{finishProduce}$ as starting and finishing the production of a fine, hand-craftedale, with $\mathrm{startConsume}$ , $\mathrm{finishConsume}$ corresponding to enjoying such an ale. (The more health-concious reader might preferto instead interpret these as start/finish the training for a marathon,and start/finish running a marathon, respectively.)

• $\square (\mathrm{finishProduce}◇\mathrm{startConsume})$
• $\square (\mathrm{finishProduce}(\mathrm{startProduce}U\mathrm{finishConsume}))$
• $(\mathrm{startConsume}W\mathrm{finishProduce})$
• $\square (\mathrm{finishConsume}(\mathrm{startConsume}W\mathrm{finishProduce}))$

In the previous exercise , the formulas entailed that production of an item could noteven begin until the previous object had been entirely consumed. This requirement might make sense forthe interpretation of marathon training/running, but it doesn't seem essential to theproduction of hand-crafted ale, even if we do want to preserve the policy of never queuing up products.

Suppose we have a computer network port whose buffer can store only one web page's data at a time.The producer could correspond to some server sending a web page to that computer,and the consumer might be a browser which processes the data being received.

• Do we want to allow the producer to be producingthe next product before the consumer finishes thecurrent one?
• What change would you make to the formulas if you did want to allow this produce-while-consuming behavior(as in the ale interpretation)?