Open the model below in Uppaal:
This model describes a simple job shop. We leave it open what is being produced here, but you may think of a copy shop, a factory for engine parts, or a workshop for clothing. Two orders have arrived, Job1 and Job2. In order to produce the ordered products, three machines are available, Machine1, Machine2 and Machine3. For order Job1 we first need Machine3 for 2 hours, then Machine2 for 2 hours, and finally Machine1 for 4 hours.. For order Job2 we first need Machine2 for 3 hours and then Machine3 for 1 hour.In the model there is for each machine a separate automaton. The basic idea is simple.. A MachineN starts when a startN? transition occurs. A clock xN is then reset to 0 and starts running. When clock xN has reached value timeN then the machine is ready and a transition endN occurs. Hence the machine is being used exactly timeN hours. Variabele timeN can be set by a user at the moment a machine is started.
For each order there is also an automaton. In order to execute Job1 we first start Machine3 with a start3! transition and indicate that we need the machine for 2 hours (time3 := 2). We then wait until Machine3 is finished (end3?). Next we start Machine2 with a start2! transition and indicate that we also need this machine for 2 hours (time2 := 2). We wait until Machine2 is finished (eid2?) and finally start Machine1 with a start1! transition. We need this machine for 4 hours (time1 := 4). When Machine1 is ready (end1?) the job is finished. The automaton for Job2 looks similarly.
Observe that in this model each machine can be used by at most one job at the time. At the beginning of the day we therefore have to make a planning in which we indicate at which times which job may use which machine. Below we give a possible planning in which altogether 9 hours are needed to process both jobs.
E<> Job1.Done && Job2.Done && x <= 7one may ask Uppaal whether a planning exists in which both orders are completed within 7 hours. Check using Uppaal that this property does not hold. Explain why it is impossible to complete both orders within 7 hours.