Practical stuff
- Due Date: 23 November 2025, before 23:59 (Blackboard's clock).
- Team Size: 2 (pair design/programming)!
Note that as of the 2017-2018 Academic Year, each International student should team up with "local" (i.e., whose Bachelor degree was obtained at the University of Antwerp). - Assignment overview:
- Review the exercises
- Implement Statechart
- Write report
- Submitting your solution:
- Only one member of each team submits a full solution. Either a ZIP-archive if you have multiple files, or just a PDF containing your report.
- The other team member must submits a single (plain text or HTML) file containing only the names of both team members. This will allow us to put in grades for both team members in BlackBoard.
- Submission Medium: BlackBoard.
- Contact / TA: Joeri Exelmans.
Goals
The goal of this assignment is to familiarize yourself with Statechart modeling, simulation, debugging and, to a lesser extent, automatically checking requirements -specified as temporal logic formulas over behaviour traces- on your solution.
Getting Started
We will use the brand-new Statechart editor, simulation and testing environment StateBuddy, created by yours truly.
No need to install anything. StateBuddy runs in the browser.
StateBuddy was tested in Firefox 144.0 and Chromium 141.0.7390.107.
Problems? Please use the GitHub issue tracker.
Exercises
Before we start working on this assignment, we will solve 5 small exercises. Each exercise shows you a small Statechart model, and asks a question about its behavior. If you can solve the exercises, you will have a good (enough) understanding of the precise semantics of StateBuddy.
The exercises can be opened by clicking on their respective links:
- nested timed transitions
- parent-first
- order of orthogonal regions
- crossing orthogonal regions
- internal events
- The execution of a Statechart is a sequence of Run-To-Completion (RTC) steps
- An RTC-step can only triggered by:
- An input event
- A timer that elapses (actually, an elapsing timer generates an input event behind the scenes)
- An RTC-step is instanteneous: it takes zero time.
- In between RTC-steps, the Statechart is idle (it will not change its state), and time may pass.
- An RTC-step consists of one or more fair-steps:
- During the first fair-step, only the input event (or timer event) that triggered the RTC-step is active.
- During a fair-step, orthogonal regions are visited in lexicographical order. For instance, if you have regions labeled A and B, then A will be visited before B.
- Within one fair step, every (orthogonal / non-overlapping) region is allowed to fire at most one transition. A region will fire a transition only if it has an enabled transition (wrt. the currently active event, and the transition's guard condition).
- When a transition fires: first, all the exit actions of all the exited states are executed (in order: child to parent), then the action of the transition itself, followed by the enter actions of the entered states (in order: parent to child)
In this example, when firing the transition from A to F, first the exit actions of A, B, and C are executed, then the actions of the transition itself, and finally the enter actions of D, E and F (in that order). - Any internal events that are raised (as a result of firing transitions), are added to the internal event (FIFO) queue.
- When a fair-step has completed:
- if the internal event (FIFO) queue is not empty, then a new fair-step starts. The next event is popped from the queue, and it becomes the new active event.
- if the internal event queue is empty, then no more fair-steps are executed, and the RTC-step ends.
- Non-determinism (e.g., multiple enabled outgoing transitions of the same state) results in a run-time error!
Example:
Consider the linked Statechart.
After initialization, the current states are: OrthogonalState, A, C, E.
Then, the Statechart remains idle until it receives an input event. Suppose at time T=5s, the input event e is received. This triggers the execution of an RTC step.
The RTC step starts with a fair-step, where regions r1, r2 and r3 (in that order) are allowed to fire at most one transition each.
Only r1 has an enabled transition (because event e is active), so only r1 fires.
During the firing of that transition, the internal event f is raised, an appended to the internal event queue.
The fair-step ends, and one more fair-step is executed, because the internal event queue is not empty.
So again, r1, r2 and r3 are allowed to fire at most one transition.
This time, the regions r2 and r3 will fire, because event f is active.
The second fair-step ends, and since the internal event queue is empty, the RTC step also ends.
Even though all transitions fired in a certain order, all of it happened at the same point in (simulated) time.
Now, the Statechart will again remain idle until another input event occurs.
Time r1 r2 r3 =0 Initialization enter A enter C enter E >0 && <5s Idle =5s RTC step (input=e) Fair-step (event=e) fire (exit A, raise f, enter B) Fair-step (event=f) fire (exit C, enter D) fire (exit E, enter F) =5s End of RTC step
Introduction to Assignment
You will use the Statecharts formalism to model the controller of a classic digital watch (before smart watches existed).
All user input happens through 4 buttons (one in each corner).
The watch can display 6 numbers, in the form HH:MM:SS when displaying the current time, or the time of the alarm, or in the form MM:SS:HS (HS means hectoseconds) when displaying the chronometer.
The watch has a background light that can be on or off.
The watch can make a beep-sound.
The time can be edited.
An alarm can be turned on or off. The alarm time can also be edited.
The chronometer can be started, paused, and reset.
Interfaces
You will implement the plant (= digital watch) controller as a Statechart. The controller only talks to the plant via input-events and output-events. In StateBuddy, you can also interactively raise input events directly into the controller statechart (Debugger UI). Finally, the plant also has its own UI, which sends input events to the plant.
For the curious student: Yes, the (simulated) plant is also implemented as a (rather big) Statechart.
| Controller input event(s) | Received when... |
|---|---|
| topLeftPressed, topRightPressed, bottomLeftPressed, bottomRightPressed | one of the 4 buttons is pressed |
| topLeftReleased, topRightReleased, bottomLeftReleased, bottomRightReleased | one of the 4 buttons is released |
| alarm | the alarm should go off |
The controller can send the following events to the plant:
| Controller output event(s) | Effect |
|---|---|
| lightOn, lightOff | turns on / off the background light |
| beep | make a beep sound for 10ms |
| incTime | increment the watch's time by one second |
| incChrono | increment the watch's chrono by 1/100 second |
| resetChrono | sets the chronometer back to 00:00:00 |
| displayTime | puts the watch into a mode where it displays the current time |
| displayChrono | puts the watch into a mode where it displays the chronometer |
| displayAlarm | puts the watch into a mode where it displays the time of the alarm |
| setAlarm(boolean) | turns the alarm on (true) or off (false). if the alarm is on, and the plant detects that the current time is equal to the alarm time, then the plant will immediately send the 'alarm' event (explained above) to the controller. |
| beginEdit | puts the plant into 'edit mode'. if the plant was displaying the current time, you can now edit the current time. if the plant was dispalying the alarm time, then you can now edit the alarm time. After entering edit mode, the 'hours' part of the display will start blinking, indicating that the 'hours' can be edited. |
| endEdit | ends the 'edit mode'. |
| incSelection | when in 'edit mode', will increase the currently blinking part (i.e, hours, minutes or seconds) of the display by one |
| selectNext | when in 'edit mode', will select the next item (hours -> minutes -> seconds -> hours) to edit |
Behavioral Requirements
- You may assume that initially, the plant is displaying the current time, the light is off, the alarm is off, the speaker is not beeping, and we are not in 'edit mode'. The chrono is zero and not running.
- For as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds.
- When displaying the time, or displaying the chrono, pressing the top-left button toggles between time and chrono mode.
- When in chrono mode, pressing the bottom-right button toggles the chrono between 'paused' and 'running'.
- When in chrono mode, pressing the bottom-left button resets the chronometer to zero.
- When the chrono is running, the chronometer value is incremented by 1/100 second 100 times per second. The chronometer remains running until it is paused, even if we leave the chrono mode.
- The current time is incremented (ticks) by 1 second every second, even when we are not displaying the current time, except when we are editing the current time: then the time should not tick.
- Pressing the bottom-left button when the time is being displayed (not in edit mode) will show the alarm time and toggle the alarm (on/off).
- If then, the bottom-left button is held pressed for 2 seconds, we go into alarm edit mode.
- Likewise, when displaying the current time (not in edit mode), and pressing and holding the bottom-right button for 2 seconds, we go into time edit mode.
- In edit mode, pressing the bottom-left button will immediately increment the current selected (blinking) numbers.
- In edit mode, holding the bottom-left button has the additional effect incrementing the current selected numbers every 100ms.
- In edit mode, pressing the bottom-right button will select the next numbers (hours -> minutes -> seconds -> hours).
- Not pressing the bottom left or bottom right buttons in edit mode for 5 seconds, will end the edit mode, and go back to displaying the current time.
- When the alarm goes off, the light should start blinking, meaning 500 ms on, then 500 ms off, repeatedly. The blinking ends on its own after 4-seconds.
- During the blinking, a 'beep' must occur every time the screen turns on/off (for a total of 8 beeps if we let the blinking run its entire 4 seconds).
- If any button is pressed while the alarm is blinking, the blinking ends, and the alarm is turned off as well. (if the blinking ends on its own (after 4 seconds), the alarm remains on)
Starting point
Use this link to the starting point for this assignment.
Testing your solution
To test your solution, initialize the execution, and interact with the plant UI. The execution can run in (scaled) real-time, with the ability to pause/resume.
To gain more confidence that you correctly implemented the requirements, you can write Metric Temporal Logic (MTL) properties. An example of such a property is:
G ((topRightPressed -> lightOn) & ((topRightPressed & (X ~topRightPressed)) -> (G[0,2000] (lightOn))))meaning: "as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds" AKA Requirement 1.
Note that none of these testing approaches are exhaustive (unlike model checking, which is exhaustive). Any property you write will only be checked on the current simulation trace.
Report
You are also required to write a small(*) (HTML or PDF) report.
(*) I don't have time to read 100 pages!
It must include the following:
- The names and student IDs of the team members
- The amount of time spent working on the project: Please be honest, this helps us estimate the workload for future assignments.
- Your workflow: How did you work together? (pair programming / divided the work / ...) In what order did you implement different features? Encountered any difficulties?
- A link to your solution (just copy the big URL including the hashtag when you're done).
- If there are non-trivial parts in your solution that require explanation, then include this explanation either in the model itself (as comments (starting with '//')), or in your report, whatever you prefer.
What is expected
Your solution needs to be precisely correct: superficially correct behavior when interacting with the Plant UI is not enough: the timing-related requirements are exact.
The assignment has been designed specifically to encourage use of as many Statechart features as possible:
- composite states
- orthogonal states
- timed transitions
- internal events
- guard conditions
- transition actions
- enter/exit actions
- (variables)
- (history)
Make sure you understand these features, and use them, where you think they are appropriate.
To give you an indication of the complexity, my own solution consists of 19 AND-states, 10 OR-states, and 36 transitions.
