Specification and Verification Tools Seminar
			      Homework 3
		     $Date: 2008/10/03 18:32:42 $

For October 8, 2008.

Download and install UPPAAL from http://www.uppaal.com/ .
You can run it by simply double clicking on the jar file inside the
download if you have Java 5 or Java 6 installed.

Read the UPPAAL tutorial from

 http://www.eecs.ucf.edu/~leavens/spec-tools-seminar/UPPAAL/tutorials/tutorial.pdf 

While reading, play with UPPAAL to test out questions you have.
(You can also bring questions to the seminar.)

Then, use UPPAAL to model an alarm clock and its surrounding
environment (i.e., the user).

The alarm-clock template itself should have two input channels,
WakeMe(t) and Reset, and one output channel, Wakeup. Hint: use one
template to model the alarm clock and another to model the user, the
two template communicate with each other using channels and global
variables.