Third Assignment AES: Job Shop

Introduction

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.

Question 1

We may use Uppaal to find an optimal planning for this job shop. For this we introduce an extra clock x that is 0 initially and is never reset: this clock measures the total amount of time that has elapsed. With the Uppaal query de Uppaal query
  E<> Job1.Done && Job2.Done && x <= 7
one 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.

Question 2

Use Uppaal to determine the minimal time needed to process both orders. Visualize the planning found by Uppaal using a Gantt chart, as above.

Question 3

Suppose a third order Job3 arrives that first requires Machine2 for 2 hours, then Machine1 for 3 hours, and finally Machine3 for 2 hours. What is the minimal time required to process all three orders? Answer the question by extending the Uppaal model. Visualize the schedule found by Uppaal using a Gantt chart.

Question 4

You get another machine, which is exactly the same as Machine1. Adapt the Uppaal model and compute how much time is needed to complete the three orders, and visualize the solution using a Gantt chart.

Question 5

Real machines sometimes break down! Assume that each time when a machine is used, there is a probability p that the machine doesn't work due to some mechanical problem. In this case a mechanic has to fix the machine and for this y hours are needed. Translate your Uppaal model to PRISM and add the possibility of machine failures in PRISM. (Hint: PRISM does not have clock variables, but since in this case study events only take place at integer times, you may use integer variables instead of real-valued clocks.)

Question 6

Compute the expected completion times for the schedules found for Question 2, 3 and 4 in a setting with machine failures (assume p=0.1 and y= 1).

Question 7

Describe a variation of the scenario of Question 4 in which (sometimes) it is better to change the schedule when it is discovered that a machine is broken. Prove (using PRISM) that the expected waiting time for the adaptive schedule is less than the expected waiting time for the scenario that is computed using Uppaal (and which is optimal under the assumption that no machine failures occur).