Hello Students,
This note is in reference to the microwave example, which can be found
in these lecture notes:
http://www.cs.utexas.edu/users/browne/uvvf2008/IntroductiontoModelsandAbstractions.pdf
If one scrolls to slide 38, it seems that the diagram can only be
valid if the start "button" is literally a push/pop button that pops
out when the door is closed in the transition from S4 to S2. Also, as
Dr. Browne pointed out in class, it might make more sense to assume
that S2 is the start state (although it doesn't really matter).
Under this definition of the start button, the quote "The user can
stop the cooking by opening the door. Once the door is opened, the
timer resets to zero." on slide 36 could be more specific by reading
"The user can stop the cooking by opening the door. Once the door is
opened, the timer resets to zero, and the start button pops out."
If you look at slide 6, you can kind of see the thoughts behind the
state diagram on slide 38, but if slide 6 is truly implemented, an
extra state must exist between S4 and S2 to show (start ^ close ^
~power). The state would need to go to S2 (where start is disabled)
before going to S3. In my mind, it's easier to just think of the
start button as a push/pop button that pops out whenever the door
closes.
Feel free to correct or just discuss.
David