$6$ Modelling Using State Transition Systems

In this exercise you will model an important ingredient of university life in Iowa City: the tortilla

press. Read the following description, and then solve the tasks listed below.

$$ tortilla press can either be open or closed and the plates of the press are either hot or cold.

Furthermore, the press can be empty, contain dough, or contain a fresh tortilla. Right after the

press is turned on it is open, empty, and cold. The press has a safety mechanism that ensures that

the press only heats up if it is closed. If the press contains dough, and it is closed and hot, it turns

the dough into a fresh tortilla. $$ chef can only add dough or remove a tortilla if the press is open.

List the PLFD variables needed to model such a tortilla press and give their domain. Also

define a state variable that denotes the next transition.

Give a PLFD formula that denotes the initial states of a tortilla press.

Provide PLFD formulas to symbolically describe the following transitions:

$($a$)$ chef opens the press.

$($b$)$ chef closes the press.

$($c$)$ The press heats up$.$

$($d$)$ chef adds dough to the press.

$($e$)$ chef removes a tortilla from the press.

$($f$)$ Dough turns into a tortilla.

Provide an LTL formula that expresses the statement: "Between making two tortillas, a

tortilla press must be open and empty at the same time." Describe in English if your formula

holds in all computations of your state transition system.