- under which circumstances the sorter misbehaves?
Use the functionalities
of UPPAAL to explain what happens when the sorter misbehaves.
Change the model
of the controlling tasks in order to ensure correct sorting of 2 bricks.
Exercise 2
In this exercise you are asked to design the control of a Machine (the control program) which will serve a coffee craving Person (the environment). As you can see (click here for a better view) above the person repeatedly (tries to) insert a coin, (tries to) extract coffee after which (s)he will make a publication. Between each action the person requires a suitable time-delay before being ready to participate in the next one.
The machine takes some time for brewing the coffee and will time-out if coffee has not been taken before a certain upper time-limit.
As a requirement we want the overall behaviour to ensure that the indicated Observer experiences a constant flow of publications from the system. In particular we want the Observer to complain if at any time more than 8 time-units elapses between two consecutive publications. Model the Machine and Observer in UPPAAL and analyse the behaviour of the system. Try to determine the maximum brewing time allowed by the Machine in order that the above requirement is met.