uppaaltutorial (1158492), страница 4
Текст из файла (страница 4)
For instance, if we modify our jobshop model and increase the number of jobbers to 100, then the size ofthe state space becomes in the order of 8100 and too big for Uppaal.2Unfortunately, the regular version of Uppaal has no option to count the number of reachablestates in a model. Such an option is present however in the command line version of the verifier:verifyta -u.1 A First Introduction to Uppaal171.7 VariablesWe will now describe how one can add integer variables to Uppaal models.
The values of these variables can be tested and updated in transitions, and thus influence thebehavior. State variables are indispensable for modeling nontrivial systems and givethe Uppaal modeling language an expressive power that is comparable to simpleprogramming languages. To illustrate the use of state variables, we discuss a smallmodification of the jobshop model:We suppose that the jobbers stop with their work as soon as they have completed 10 jobs together.In order to capture this additional requirement in our model, we add an integerstate variable that records how many jobs have been taken from the belt. This isachieved by adding the following lines in the global project Declarations in thewindow on the left in the Editor:const int J = 10;int[0,J] jobs;In the first line, we declare an integer constant with value 10.
As suggested by theirname, the value of constants always remains the same. In the second line an integervariable jobs is declared with minimum value 0 and maximum value J. The valueof variables can be modified when transitions occur. By default, the initial value ofa variable is 0. The domain of integer variables in Uppaal is always bounded. If wespecify no bounds and simply declareint jobs;then implicitly the minimum value is −32768 and the maximum value is 32768.3Whenever during exploration of the state space — either in the simulator or in theverifier — a variable gets assigned a value outside its domain, this is referred to asa “run time error” and an error message is generated.Figure 1.12 shows an extension of the jobber model in which the variable jobsis used.
In the location begin, a jobber only accepts a new job when jobs < J.In this case, the value of jobs is incremented by 1. We can implement this changeof the model by double clicking the transition from begin to easy, and then writejobs < J in the field Guard of the resulting menu. In Uppaal, a transition can onlybe taken if its guard evaluates to true (if no guard is specified then we assume itequals true). In the field Update of the transition, we specify that the value ofjobs must be incremented by 1 whenever the transition is taken. This is done bywriting jobs + +, using syntax that has been taken from the programming languageC.
Alternatively, we can also write jobs = jobs + 1 or jobs := jobs + 1 (this allmeans the same). We also add an extra location done to the model, and a transition3Like in C, Uppaal uses 16-bit int’s, including 1 bit to represent the sign.18Frits Vaandragerfrom begin to done, which is taken whenever jobs has reached the value J and alljobs are done.easywork_easywork_av_malletjobs<Jjobs++put_mallet!get_mallet!averagebeginjobs<Jjobs++work_av_hammerjobs==Jget_hammer!jobs<Jjobs++put_hammer!work_harddoneget_hammer!put_hammer!hardFig. 1.12 Model of jobber in which exactly J jobs are carried out.When we now start the simulator, we see a separate window in which, for eachstate, the value of the state variable jobs is listed. Using the verifier, we can establish that the model of Figure 1.12 satisfies exactly the same correctness propertiesas the model of Figure 1.9, except for the propertyA[] not deadlockwhich is no longer satisfied.
When the jobbers have finished J jobs and have movedto location done, no further transitions are possible and therefore a deadlock statehas been reached.Observe that in the modified model, both jobbers together perform J jobs. Thisis because jobs is a global variable that can be tested and updated by both jobbers.In Uppaal, we can also declare local variables, which can only be used by oneautomaton. When in the Editor we click on the “+” symbol at the left of the templateJobber, a new line Declarations appears below Jobber. When we select this line,we can declare local variables for the template.
For instance, by moving the lineint[0,J] jobs;from the global declarations section to the local declarations section of templateJobber, we give Jobber1 and Jobber2 each their own, local copy of variablejobs. The result is that both Jobber1 and Jobber2 have to perform J jobs, insteadof J jobs together.1 A First Introduction to Uppaal19Uppaal has a rather extensive syntax for the expressions in guards and updates. Itis possible to declare arrays and Boolean variables, and a user can even define new“record” types and new functions.
The syntax for doing this is very similar to thesyntax of programming languages such as C and Java. For an overview of the syntaxwe refer to Chapter 2 of this handbook Add ref and to the help menu of Uppaal:click on Language Reference and then on Expressions.1.8 Time and clocksIn the design and analysis of real systems, timing aspects often play a role.
Sometimes we may abstract from quantitative timing, and only consider the ordering ofevents, but often timing information has to be included in the model in order to beable to answer certain questions. For instance, we may need to establish not onlythat a certain location can be reached, but also how fast. In the case of our jobshop,the following question could arise. Uppaal has been more or less designed to answerthis type of questions.We suppose that a jobber needs (at least) 5 seconds for an easy job, 10 secondsfor an average job using the hammer, 15 seconds for an average job using themallet, and 20 seconds for a hard job.
We suppose that the jobs arrive in thefollowing order: H, A, H, H, H, E, E, A, A, A, where E denotes an easy job, Aan average job, and H a hard job. How much time do the two jobbers need (atleast) to complete the 10 jobs?1.8.1 Modeling the conveyor beltBefore we add timing to our model, we first add an automaton that describes thebehavior of the conveyor belt. The belt was not included in our first model (therewas no reason for adding it) but in order to answer the question about timing, theorder in which jobs arrive appears to be relevant.
In order to model incoming jobs,we declare three new channels jobE, jobA en jobH, which correspond to the arrivalof easy, average, and hard jobs, respectively. The automaton Belt, which is depictedin Figure 1.13, describes the behavior of the conveyor belt that delivers the 10 jobs inthe specified order. By adding automaton Belt to the model in System declarationsand by labeling the outgoing transitions of location begin of the jobber automatonof Figure 1.9 in the obvious way with the synchronization channels jobE?, jobA?en jobH?, we model that the jobbers have to deal with the specified sequence of 10jobs.20Frits VaandragerjobA!jobA!endjobH!jobH!jobA!startjobH!jobH!jobA!jobE!jobE!Fig.
1.13 Model of conveyor belt that delivers 10 jobs.1.8.2 Clocks and lower bounds on timingIn the models that we have constructed thus far, time is not modeled explicitly. InUppaal we assume that transitions occur instantaneously and do not take time. Timemay only elapse when all automata in the model are waiting in a location.
Whenever we want to model an activity that takes time, we can do this by introducing twoconsecutive transitions, one corresponding to the start of the activity, and anothercorresponding to the end of it. Often, models only contain transitions that correspond to either the beginning or the end of an activity that has a duration. If we wantto be really precise then, for instance, we could say that the jobH! transition corresponds to the moment when a jobber starts to pick a hard job from the conveyor belt,the get mallet transition corresponds to the moment when a jobber starts grabbing the mallet and the put mallet transition corresponds to the moment when ajobber ends the activity of putting the mallet back on the table again.If we want to specify lower and upper bounds on the time that an automaton maystay in a certain location, we can do this in Uppaal using so-called clocks.
A clockis a special type of variable, whose domain consists of the set of nonnegative realnumbers. Just like other variables, clocks can be declared either as a global variable(which can be tested and updated by all automata) or as a local variable (which canonly be used by one automaton). In the initial state, all clocks have value 0. Whenan automaton is waiting in a location and time elapses then the values of its clocksincrease. More precisely, when t time units pass then the values of all clocks in themodel increase with t. Thus, all clocks are “perfect” and increase at exactly the samerate as real-time. In reality, of course, no clock is 100% perfect, but in our modelinglanguage it is convenient to use the idealization of perfect clocks to specify upperand lower bounds on the timing of transitions.1 A First Introduction to Uppaal21x>=5easywork_easyx:=0jobE?beginjobA?work_av_malletget_mallet!averagex:=0put_mallet!x>=15x:=0work_av_hammerget_hammer!put_hammer!x>=10jobH?x:=0get_hammer!hardwork_hardput_hammer!x>=20Fig.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
