uppaaltutorial (Uppaal - описание), страница 5

1.14 Model of jobber extended with a clock.Figure 1.14 shows a model of the jobber that has been extended with the newsynchronization channels jobE?, jobA? and jobH?, and also with a clock variablex. Clock x has been declared by adding the following line to the local Declarationssection of template Jobber:clock x;When a jobber moves from location easy to location work easy, that is, startsto work on an easy job, clock x is reset to 0 via an update x := 0. Subsequently,the guard of the outgoing transition of work easy tests whether x >= 5. In thisway, we enforce that this transition may only occur once the automaton has beenin location work easy for at least 5 time units. This corresponds to our assumptionthat a jobber needs at least 5 time units to complete a simple job.

In a similar waywe model that the automaton spends at least 10, 15 and 20 time units in locationswork av hammer, work av mallet and work hard, respectively.In the resulting model, Jobber1 and Jobber2 both have a local clock variablex that records how long they have been working on a certain job. Each time whena jobber starts with a new job its local clock is reset to 0. In order to record thetotal amount of time that has elapsed, we also introduce a global clock now, whichis never reset.

As a result, the global declarations look as follows:chan jobE, jobA, jobH,get_mallet, get_hammer, put_mallet, put_hammer;clock now;22Frits VaandragerWe can ask Uppaal whether there exists a state in which all the 10 jobs have beendelivered and both jobbers have returned to their initial state (that is, all the jobshave been completed):E<> (Belt.end && Jobber1.begin && Jobber2.begin)When Uppaal computes a diagnostic trace which demonstrates that this propertyis satisfied, this will, in general, not be the shortest trace.

After all, we have onlyspecified lower bounds for the timing in our model and no upper bounds. Thus thebelt may wait indefinitely before delivering a job, a jobber may dawdle for daysbefore he starts with the job, and for years before completing it. However, if weselect in the menu Options under Diagnostic Trace the option Fastest, then Uppaalwill produce the fastest execution that leads to the specified state. In the simulatorwe can see that in the final state of this execution now >= 100.

This means thatthe jobbers need at least 100 time units to complete the 10 jobs. The easiest wayto understand the schedule that has been computed by Uppaal is via the so-called“message sequence chart” in the lower right window of the simulator: here we seewhich jobber handles which job. Figure 1.15 visualizes this fastest schedule in anFig. 1.15 Fastest schedule for completing the 10 jobs.even more compact way as a “Gantt chart”.4 We see that one jobber is permanentlybusy with the hammer, whereas the other jobber has a relaxed schedule in whichhe is idling most of the time but also completes some jobs with his hands or withthe mallet.

It is easy to come up with an equally fast schedule in which the workload is more evenly distributed. We may decide, for instance, to give the third job toJobber2.4Figure 1.15 was constructed manually. Effort is underway to extend Uppaal with a feature forautomatic visualization of traces using Gantt charts.1 A First Introduction to Uppaal231.8.3 Upper bounds on timingWe have seen that lower bounds on timing can be specified with the help of clockconstraints in guards. For example, the constraint x >= 5 in the guard of the transition from work easy to begin indicates that this transition can only be taken oncethe jobber has spent at least 5 time units in location work easy.

In practice, we oftenneed to prove upper bounds on timing: an airbag needs to inflate within a few microseconds after a collision has been detected, a soccer playing robot must quicklyreact when the ball is nearby, etc. In our jobshop example, the following questionmay arise:We suppose that a jobber needs at most 7 seconds for an easy job, 12 secondsfor an average job with the hammer, 17 seconds for an average job with themallet, and 22 seconds for a hard job.How much time do the two jobbers need at most to complete the 10 jobs,assuming that a jobber picks a new job from the belt as soon as he is ready towork on it, and that he grabs a tool that allows him to do a job as soon as itbecomes available?In Uppaal we can specify upper bounds on timing, using so-called “invariants”.When we double click the location work easy, a window appears with a field Invariant.

By entering x <= 7 in this field, we specify that in this location the valueof x will always be at most 7. In other words, a jobber needs at most 7 time unitsto complete a simple job. If more than 7 time units have elapsed then the jobberhas left location work easy. In Figure 1.16 upper bounds of 7, 12, 17 and 22have been added for locations work easy, work av hammer, work av mallet andwork hard, respectively.

In addition, an upper bound of 0 has been added for location easy. This models the assumption that when a jobber has picked an easy jobfrom the belt he starts working on it right away. We could have enforced this upperbound by resetting clock x upon entering location easy, in combination with aninvariant x <= 0 for this location. But Uppaal supports a simpler way of specifyingthe same requirement: if we double clock the location easy we can check the fieldUrgent. If a location is Urgent then this means that time can not elapse within thislocation, and hence a transition to another location will occur immediately.After all these modifications of the model, it is still not possible to infer an upperbound on the time need to complete all jobs.

The reason is that workers may waitindefinitely before picking the next job from the belt, and they may wait indefinitelybefore grabbing a tool. We have not yet modelled the requirement that jobbers grabjobs and tools as soon as they can. A convenient way to eliminate idling is by makingthe synchronizations for grabbing a job or tool “urgent”. When a synchronizationchannel is urgent, this means that whenever a synchronization with this channel isenabled, time can not advance and a transition has to be taken immediately.

We canspecify this in Uppaal by changing the declarations of the channels as follows:24Frits Vaandragerx>=5easyx<=7work_easyx:=0x<=17jobE?beginjobA?work_av_malletput_mallet!x>=15get_mallet!averagex:=0x:=0work_av_hammerget_hammer!jobH?x<=12x:=0put_hammer!x>=10work_hardget_hammer!put_hammer!x<=22x>=20hardFig. 1.16 Model of jobber with upper bounds on timing.urgent chan jobE, jobA, jobH, get_mallet, get_hammer;chanput_mallet, put_hammer;Note that there exists a subtle difference between the use of urgent locations andurgent synchronizations. If we would make location begin of the jobber templateurgent rather than channels jobE, jobA and jobH, a problem would arise in a statewhere a jobber is in location begin but no further jobs are on the belt and hence nojobE, jobA or jobH synchronizations are offered: in such a state there would be nopossibility for time to progress and there would be a “time deadlock”.

Clearly, sucha model is not realistic. Likewise, a time deadlock would arise if we would makelocation hard urgent rather than channel get hammer.Observe that in the model of Figure 1.16, a jobber may spend in between 5 and 7time units in location work easy. We have not specified in our model any furtherinformation about the time needed to complete an easy job: this choice is fullynondeterministic. Maybe a jobber usually completes an easy job within 6 time unitsbut sometimes needs more time when he is tired. Maybe one jobber always completea job within 5.731 time units, whereas another jobber always needs at least 6.194time units. Maybe jobbers will always complete easy jobs within 5.5 and 5.8 timeunits, but we have not carried out the exact measurements and want to be on the safeside.

The ability to have nondeterminism in the timing of transitions is an extremelyuseful feature of timed automata, which makes it possible to describe systems andreason about them at a high level of abstraction.Whereas the Verifier has an option to compute the fastest execution leading toa certain state, there is no corresponding option to compute the slowest execution.Nevertheless, we can compute this slowest execution via a few successive approx-1 A First Introduction to Uppaal25imations. Uppaal can conform our guess that after 200 time units all jobs will becompleted, that is, that the following property is satisfied:A[] now>=200 imply(Belt.end && Jobber1.begin && Jobber2.begin)We even haveA[] now>=150 imply(Belt.end && Jobber1.begin && Jobber2.begin)but notA[] now>=110 imply(Belt.end && Jobber1.begin && Jobber2.begin)So the jobbers need at most between 110 and 150 time units to complete all thejobs. By doing a “binary search” and reducing the size of the interval step by step,we may infer that the following property is satisfied:A[] now>=127 imply(Belt.end && Jobber1.begin && Jobber2.begin)but the next property is not:A[] now>=126 imply(Belt.end && Jobber1.begin && Jobber2.begin)Hence, the diagnostic trace for the last property gives the slowest possible schedule,which takes exactly 126 time units.