Scheduling with operations
Lax434175.Operations · concepts/Lax434175/Operations.lean · lax-434175
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
An instance has jobs and machines. Every job consists of a sequence of operations, and an operation needs time on machine ; when it occupies a set of machines, it needs the largest of these times. Every job has a release date. Parallel machines are the case of one operation per job, and shops the case in which the time of an operation does not depend on the machine.
A schedule is a finite list of pieces. A piece processes one operation on a nonempty set of machines during an interval given by a start time and a length, both nonnegative rational numbers. A schedule is feasible for the kernel if two different pieces that belong to the same job or share a machine are disjoint in time. An operation starts when its first piece starts and completes when its last piece ends; a job starts when its first piece starts and completes when its last piece ends.
The fields are those of parallel machines and of shops, read per operation:
- interruption, per operation: none (one full piece starting at an integral time), restarts, preemption (the fractions of its pieces sum to , or a piece is on machines on which it needs time ), or preemption without migration (preemption, and all its pieces occupy the same set of machines);
- job structure: one operation per job, or the open, flow, job and two-stage flexible flow shop;
- machine environment and processing times, over the times ;
- machines: the values of the machine-set field of parallel machines, which restrict every operation of a job alike, and those of the machine field of shops, which restrict every operation separately; a value of the first kind is a special case of the second kind where the second kind can express it;
- numbers of machines and of jobs, release dates, deadlines, precedence constraints, communication delays, forbidden times and the input encoding, as for parallel machines;
- server, no-wait, transportation delays, no-idle and batch setups, as for shops.
Theorem. The fields are sound, and every job starts no later than it completes.
Concept map
Evidence
This concept declares 11 statements. Each proof establishes one of them relative to its assumptions.
1 batchSetups_sound proven
2 environment_sound proven
3 interruption_sound proven
4 jobStructure_sound proven
5 machineSets_sound proven
6 noIdle_sound proven
7 noWait_sound proven
8 processingTimes_sound proven
9 server_sound proven
10 startsBeforeCompletion proven
11 transportation_sound proven
Lean source view on GitHub
| 1 | import Lax434175.ParallelMachines |
| 2 | import Lax434175.Interruption |
| 3 | import Lax434175.MachineSets |
| 4 | import Lax434175.ShopFamily |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Scheduling with operations |
| 9 | type: theorem |
| 10 | --- |
| 11 | An instance has jobs and machines. Every job consists of a sequence |
| 12 | of operations, and an operation needs time on machine ; when |
| 13 | it occupies a set of machines, it needs the largest of these times. Every job |
| 14 | has a release date. Parallel machines are the case of one operation per job, |
| 15 | and shops the case in which the time of an operation does not depend on the |
| 16 | machine. |
| 17 | |
| 18 | A schedule is a finite list of pieces. A piece processes one operation on a |
| 19 | nonempty set of machines during an interval given by a start time and a |
| 20 | length, both nonnegative rational numbers. A schedule is feasible for the |
| 21 | kernel if two different pieces that belong to the same job or share a |
| 22 | machine are disjoint in time. An operation starts when its first piece |
| 23 | starts and completes when its last piece ends; a job starts when its first |
| 24 | piece starts and completes when its last piece ends. |
| 25 | |
| 26 | The fields are those of parallel machines and of shops, read per operation: |
| 27 | |
| 28 | - interruption, per operation: none (one full piece starting at an integral |
| 29 | time), restarts, preemption (the fractions of its pieces sum to , or a |
| 30 | piece is on machines on which it needs time ), or preemption without |
| 31 | migration (preemption, and all its pieces occupy the same set of |
| 32 | machines); |
| 33 | - job structure: one operation per job, or the open, flow, job and two-stage |
| 34 | flexible flow shop; |
| 35 | - machine environment and processing times, over the times ; |
| 36 | - machines: the values of the machine-set field of parallel machines, which |
| 37 | restrict every operation of a job alike, and those of the machine field of |
| 38 | shops, which restrict every operation separately; a value of the first kind |
| 39 | is a special case of the second kind where the second kind can express it; |
| 40 | - numbers of machines and of jobs, release dates, deadlines, precedence |
| 41 | constraints, communication delays, forbidden times and the input encoding, |
| 42 | as for parallel machines; |
| 43 | - server, no-wait, transportation delays, no-idle and batch setups, as for |
| 44 | shops. |
| 45 | |
| 46 | **Theorem.** The fields are sound, and every job starts no later than it |
| 47 | completes. |
| 48 | -/ |
| 49 | |
| 50 | namespace Lax434175.Operations |
| 51 | open Lax434175.Kernels Lax434175.Modules Lax434175 |
| 52 | |
| 53 | structure Inst where |
| 54 | jobs : ℕ |
| 55 | machines : ℕ |
| 56 | /-- The number of operations of a job. -/ |
| 57 | ops : Fin jobs → ℕ |
| 58 | /-- The time an operation needs on a machine. -/ |
| 59 | p : (j : Fin jobs) → Fin (ops j) → Fin machines → ℕ |
| 60 | /-- The release date of a job. -/ |
| 61 | r : Fin jobs → ℕ |
| 62 | |
| 63 | /-- An operation: a job and a position in its sequence. -/ |
| 64 | abbrev Op (x : Inst) := (j : Fin x.jobs) × Fin (x.ops j) |
| 65 | |
| 66 | /-- The time an operation needs when it occupies a set of machines. -/ |
| 67 | def duration (x : Inst) (o : Op x) (S : Finset (Fin x.machines)) : ℕ := |
| 68 | S.sup (x.p o.1 o.2) |
| 69 | |
| 70 | /-- The shop instance with the jobs, machines and operations of an instance. -/ |
| 71 | abbrev Inst.toShop (x : Inst) : Shops.Inst := ⟨x.jobs, x.machines, x.ops, fun _ _ => 0, x.r⟩ |
| 72 | |
| 73 | /-- The parallel-machine instance with the jobs and machines of an instance. -/ |
| 74 | abbrev Inst.toPar (x : Inst) : ParallelMachines.Inst := ⟨x.jobs, x.machines, fun _ _ => 0, x.r⟩ |
| 75 | |
| 76 | /-- An operation is processed on a set of machines from `start` for `length` |
| 77 | time units. -/ |
| 78 | structure Piece (x : Inst) where |
| 79 | op : Op x |
| 80 | machines : Finset (Fin x.machines) |
| 81 | start : NNRat |
| 82 | length : NNRat |
| 83 | |
| 84 | /-- The time at which a piece ends. -/ |
| 85 | def Piece.finish {x : Inst} (q : Piece x) : NNRat := q.start + q.length |
| 86 | |
| 87 | structure Sched (x : Inst) where |
| 88 | pieces : List (Piece x) |
| 89 | |
| 90 | /-- The pieces of an operation. -/ |
| 91 | def piecesOf {x : Inst} (σ : Sched x) (o : Op x) : List (Piece x) := |
| 92 | σ.pieces.filter (fun q => decide (q.op = o)) |
| 93 | |
| 94 | /-- The pieces of a job. -/ |
| 95 | def piecesOfJob {x : Inst} (σ : Sched x) (j : Fin x.jobs) : List (Piece x) := |
| 96 | σ.pieces.filter (fun q => decide (q.op.1 = j)) |
| 97 | |
| 98 | /-- Two pieces do not overlap in time. -/ |
| 99 | def Apart {x : Inst} (a b : Piece x) : Prop := |
| 100 | a.finish ≤ b.start ∨ b.finish ≤ a.start |
| 101 | |
| 102 | /-- The start of the first piece of an operation. -/ |
| 103 | def opStart {x : Inst} (σ : Sched x) (o : Op x) : NNRat := |
| 104 | (((piecesOf σ o).map Piece.start).min?).getD 0 |
| 105 | |
| 106 | /-- The end of the last piece of an operation. -/ |
| 107 | def opFinish {x : Inst} (σ : Sched x) (o : Op x) : NNRat := |
| 108 | (((piecesOf σ o).map Piece.finish).max?).getD 0 |
| 109 | |
| 110 | /-- The fraction of an operation that a schedule completes. -/ |
| 111 | def fraction (x : Inst) (σ : Sched x) (o : Op x) : NNRat := |
| 112 | ((piecesOf σ o).map (fun q => q.length / (duration x o q.machines : NNRat))).sum |
| 113 | |
| 114 | /-- Every piece occupies some machine, and two different pieces that belong to |
| 115 | the same job or share a machine do not overlap. -/ |
| 116 | def feasible {x : Inst} (σ : Sched x) : Prop := |
| 117 | (∀ q ∈ σ.pieces, q.machines.Nonempty) ∧ |
| 118 | σ.pieces.Pairwise (fun a b => (a.op.1 = b.op.1 ∨ ¬ Disjoint a.machines b.machines) → Apart a b) |
| 119 | |
| 120 | /-- The kernel of scheduling with operations. -/ |
| 121 | def kernel : Kernel where |
| 122 | Inst := Inst |
| 123 | jobs := Inst.jobs |
| 124 | release := Inst.r |
| 125 | Sched := Sched |
| 126 | feasible _ σ := feasible σ |
| 127 | start _ σ j := (((piecesOfJob σ j).map Piece.start).min?).getD 0 |
| 128 | completion _ σ j := (((piecesOfJob σ j).map Piece.finish).max?).getD 0 |
| 129 | |
| 130 | /-- The number of machines, a parameter of the kernel. -/ |
| 131 | def machines : kernel.Inst → ℕ := Inst.machines |
| 132 | |
| 133 | -- Interruption |
| 134 | |
| 135 | /-- A piece processes its operation entirely. -/ |
| 136 | def Complete {x : Inst} (q : Piece x) : Prop := |
| 137 | q.length = (duration x q.op q.machines : NNRat) |
| 138 | |
| 139 | /-- The schedules that respect a way of interruption. -/ |
| 140 | def holds : Interruption.Mode → (x : Inst) → Sched x → Prop |
| 141 | | .none, x, σ => ∀ o : Op x, ∃ q, piecesOf σ o = [q] ∧ |
| 142 | q.length = (duration x o q.machines : NNRat) ∧ ∃ n : ℕ, q.start = (n : NNRat) |
| 143 | | .restarts, _, σ => ∀ o, ∃ q ∈ piecesOf σ o, Complete q ∧ |
| 144 | ∀ q' ∈ piecesOf σ o, q'.finish ≤ q.finish ∧ (Complete q' → q'.finish = q.finish) |
| 145 | | .pmtn, x, σ => ∀ o, fraction x σ o = 1 ∨ ∃ q ∈ piecesOf σ o, duration x o q.machines = 0 |
| 146 | | .pmtnNoMigration, x, σ => ∀ o, |
| 147 | (fraction x σ o = 1 ∨ ∃ q ∈ piecesOf σ o, duration x o q.machines = 0) ∧ |
| 148 | ∀ q ∈ piecesOf σ o, ∀ q' ∈ piecesOf σ o, q.machines = q'.machines |
| 149 | |
| 150 | /-- The interruption field. -/ |
| 151 | def interruption : Module kernel where |
| 152 | Value := Interruption.Mode |
| 153 | Data _ _ := Unit |
| 154 | admits _ _ _ := True |
| 155 | constraint v x _ σ := holds v x σ |
| 156 | le v w := decide (v = w) |
| 157 | embed _ _ _ := () |
| 158 | |
| 159 | -- Job structure |
| 160 | |
| 161 | inductive Structure |
| 162 | | single |
| 163 | | open |
| 164 | | flow |
| 165 | | job |
| 166 | | flexibleFlow |
| 167 | deriving DecidableEq |
| 168 | |
| 169 | /-- The instances of a job structure. -/ |
| 170 | def Structure.holds : Structure → Inst → Prop |
| 171 | | .single, x => ∀ j, x.ops j = 1 |
| 172 | | .open, x => ∀ j, x.ops j = x.machines |
| 173 | | .flow, x => ∀ j, x.ops j = x.machines |
| 174 | | .job, _ => True |
| 175 | | .flexibleFlow, x => ∀ j, x.ops j = 2 |
| 176 | |
| 177 | /-- The operations of every job are processed in their given order. -/ |
| 178 | def InOrder (x : Inst) (σ : Sched x) : Prop := |
| 179 | ∀ j (k k' : Fin (x.ops j)), k < k' → opFinish σ ⟨j, k⟩ ≤ opStart σ ⟨j, k'⟩ |
| 180 | |
| 181 | /-- The order a job structure imposes on the operations of a job. -/ |
| 182 | def Structure.ordered : Structure → (x : Inst) → Sched x → Prop |
| 183 | | .single, _, _ => True |
| 184 | | .open, _, _ => True |
| 185 | | .flow, x, σ => InOrder x σ |
| 186 | | .job, x, σ => InOrder x σ |
| 187 | | .flexibleFlow, x, σ => InOrder x σ |
| 188 | |
| 189 | def Structure.le : Structure → Structure → Bool |
| 190 | | .single, .job | .flow, .job | .flexibleFlow, .job => true |
| 191 | | v, w => decide (v = w) |
| 192 | |
| 193 | /-- The job-structure field. -/ |
| 194 | def jobStructure : Module kernel where |
| 195 | Value := Structure |
| 196 | Data _ _ := Unit |
| 197 | admits v x _ := v.holds x |
| 198 | constraint v x _ σ := v.ordered x σ |
| 199 | le := Structure.le |
| 200 | embed _ _ _ := () |
| 201 | |
| 202 | -- Machine environment and processing times |
| 203 | |
| 204 | /-- The instances of a machine environment. -/ |
| 205 | def environmentHolds : ParallelMachines.Environment → Inst → Prop |
| 206 | | .identical, x => ∀ (o : Op x) i i', x.p o.1 o.2 i = x.p o.1 o.2 i' |
| 207 | | .uniform, x => ∃ (q : Op x → ℕ) (s : Fin x.machines → ℕ), |
| 208 | ∀ (o : Op x) i, 0 < s i ∧ x.p o.1 o.2 i * s i = q o |
| 209 | | .unrelated, _ => True |
| 210 | |
| 211 | /-- The machine-environment field. -/ |
| 212 | def environment : Module kernel := |
| 213 | Module.ofRestriction ParallelMachines.Environment (fun v x => environmentHolds v x) |
| 214 | (fun v w => decide (v.rank ≤ w.rank)) |
| 215 | |
| 216 | /-- The instances of a processing-time restriction. -/ |
| 217 | def processingTimesHolds : ParallelMachines.ProcessingTimes → Inst → Prop |
| 218 | | .unit, x => ∀ (o : Op x) i, x.p o.1 o.2 i = 1 |
| 219 | | .equal, x => ∃ p, ∀ (o : Op x) i, x.p o.1 o.2 i = p |
| 220 | | .oneOrTwo, x => ∀ (o : Op x) i, x.p o.1 o.2 i = 1 ∨ x.p o.1 o.2 i = 2 |
| 221 | | .arbitrary, _ => True |
| 222 | |
| 223 | /-- The processing-time field. -/ |
| 224 | def processingTimes : Module kernel := |
| 225 | Module.ofRestriction ParallelMachines.ProcessingTimes (fun v x => processingTimesHolds v x) |
| 226 | ParallelMachines.ProcessingTimes.le |
| 227 | |
| 228 | -- Machines |
| 229 | |
| 230 | /-- A value of the machine field: a machine-set value of parallel machines, |
| 231 | which restricts every operation of a job alike, or a machine value of shops. -/ |
| 232 | inductive Machines |
| 233 | | par (v : MachineSets.Value) |
| 234 | | shop (v : Shops.Machines) |
| 235 | |
| 236 | /-- The data of a value. -/ |
| 237 | def Machines.Data : Machines → Inst → Type |
| 238 | | .par v, x => MachineSets.Data v x.toPar |
| 239 | | .shop v, x => Shops.Machines.Data v x.toShop |
| 240 | |
| 241 | /-- Whether an operation may occupy a set of machines. -/ |
| 242 | def Machines.view {x : Inst} : (v : Machines) → v.Data x → Op x → Finset (Fin x.machines) → Prop |
| 243 | | .par v, d => fun o S => MachineSets.view (x := x.toPar) v d o.1 S |
| 244 | | .shop v, d => fun o S => Shops.Machines.view (x := x.toShop) v d o.1 o.2 S |
| 245 | |
| 246 | /-- The condition on the data. -/ |
| 247 | def Machines.admits {x : Inst} : (v : Machines) → v.Data x → Prop |
| 248 | | .par _, _ => True |
| 249 | | .shop v, d => Shops.Machines.admits (x := x.toShop) v d |
| 250 | |
| 251 | /-- Which machine-set values of parallel machines are special cases of which |
| 252 | machine values of shops. -/ |
| 253 | def crossLe : MachineSets.Value → Shops.Machines → Bool |
| 254 | | .none, .sets | .sets, .sets | .fix, .fix => true |
| 255 | | _, .general => true |
| 256 | | _, _ => false |
| 257 | |
| 258 | def Machines.le : Machines → Machines → Bool |
| 259 | | .par v, .par w => MachineSets.le v w |
| 260 | | .shop v, .shop w => Shops.Machines.le v w |
| 261 | | .par v, .shop w => crossLe v w |
| 262 | | .shop _, .par _ => false |
| 263 | |
| 264 | /-- Machine-set data of parallel machines read as machine data of shops. -/ |
| 265 | def crossEmbed : (v : MachineSets.Value) → (w : Shops.Machines) → crossLe v w = true → |
| 266 | (x : Inst) → MachineSets.Data v x.toPar → Shops.Machines.Data w x.toShop |
| 267 | | .none, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 268 | | .none, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 269 | | .none, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 270 | | .none, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 271 | | .none, .sets, _, _, _ => fun _ _ _ => True |
| 272 | | .none, .fix, h, _, _ => absurd h Bool.false_ne_true |
| 273 | | .none, .general, _, _, M => fun j _ S => MachineSets.view .none M j S |
| 274 | | .sets, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 275 | | .sets, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 276 | | .sets, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 277 | | .sets, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 278 | | .sets, .sets, _, _, M => fun j _ i => M j i |
| 279 | | .sets, .fix, h, _, _ => absurd h Bool.false_ne_true |
| 280 | | .sets, .general, _, _, M => fun j _ S => MachineSets.view .sets M j S |
| 281 | | .fix, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 282 | | .fix, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 283 | | .fix, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 284 | | .fix, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 285 | | .fix, .sets, h, _, _ => absurd h Bool.false_ne_true |
| 286 | | .fix, .fix, _, _, M => fun j _ => M j |
| 287 | | .fix, .general, _, _, M => fun j _ S => MachineSets.view .fix M j S |
| 288 | | .sizeOneOrAll, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 289 | | .sizeOneOrAll, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 290 | | .sizeOneOrAll, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 291 | | .sizeOneOrAll, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 292 | | .sizeOneOrAll, .sets, h, _, _ => absurd h Bool.false_ne_true |
| 293 | | .sizeOneOrAll, .fix, h, _, _ => absurd h Bool.false_ne_true |
| 294 | | .sizeOneOrAll, .general, _, _, M => fun j _ S => MachineSets.view .sizeOneOrAll M j S |
| 295 | | .size, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 296 | | .size, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 297 | | .size, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 298 | | .size, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 299 | | .size, .sets, h, _, _ => absurd h Bool.false_ne_true |
| 300 | | .size, .fix, h, _, _ => absurd h Bool.false_ne_true |
| 301 | | .size, .general, _, _, M => fun j _ S => MachineSets.view .size M j S |
| 302 | | .general, .byPosition, h, _, _ => absurd h Bool.false_ne_true |
| 303 | | .general, .dedicated, h, _, _ => absurd h Bool.false_ne_true |
| 304 | | .general, .recirculation, h, _, _ => absurd h Bool.false_ne_true |
| 305 | | .general, .stages, h, _, _ => absurd h Bool.false_ne_true |
| 306 | | .general, .sets, h, _, _ => absurd h Bool.false_ne_true |
| 307 | | .general, .fix, h, _, _ => absurd h Bool.false_ne_true |
| 308 | | .general, .general, _, _, M => fun j _ S => MachineSets.view .general M j S |
| 309 | |
| 310 | def Machines.embed : {v w : Machines} → Machines.le v w = true → (x : Inst) → |
| 311 | v.Data x → w.Data x |
| 312 | | .par _, .par _, h, x, d => MachineSets.embed h x.toPar d |
| 313 | | .shop _, .shop _, h, x, d => Shops.Machines.embed h x.toShop d |
| 314 | | .par v, .shop w, h, x, d => crossEmbed v w h x d |
| 315 | | .shop _, .par _, h, _, _ => absurd h Bool.false_ne_true |
| 316 | |
| 317 | /-- The machine field. -/ |
| 318 | def machineSets : Module kernel where |
| 319 | Value := Machines |
| 320 | Data := Machines.Data |
| 321 | admits v _ d := v.admits d |
| 322 | constraint v _ d σ := ∀ q ∈ σ.pieces, v.view d q.op q.machines |
| 323 | le := Machines.le |
| 324 | embed := Machines.embed |
| 325 | |
| 326 | -- Fields of parallel machines read per job |
| 327 | |
| 328 | /-- Scheduling with operations as a machine model on parallel machines: a job |
| 329 | occupies a set of machines if one of its pieces does. -/ |
| 330 | def model : ParallelMachines.Model where |
| 331 | kernel := kernel |
| 332 | inst x := x.toPar |
| 333 | jobs_eq _ := rfl |
| 334 | uses _ σ j S := ∃ q ∈ piecesOfJob σ j, q.machines = S |
| 335 | |
| 336 | -- Fields of shops |
| 337 | |
| 338 | /-- A piece of one operation and a piece of another share a machine. -/ |
| 339 | def Shares {x : Inst} (σ : Sched x) (a b : Op x) : Prop := |
| 340 | ∃ qa ∈ piecesOf σ a, ∃ qb ∈ piecesOf σ b, ¬ Disjoint qa.machines qb.machines |
| 341 | |
| 342 | /-- The server field: every operation needs a setup. -/ |
| 343 | def server : Module kernel where |
| 344 | Value := Servers.Value |
| 345 | Data v x := Servers.Data (Op x) v |
| 346 | admits v _ d := Servers.Admits v d |
| 347 | constraint v x d σ := ∀ s, Servers.view v d = some s → |
| 348 | Servers.Served (fun o : Op x => (opStart σ o : ℚ)) (fun o => (opFinish σ o : ℚ)) |
| 349 | (Servers.setupRelease (fun o : Op x => (opStart σ o : ℚ)) |
| 350 | (fun o => (kernel.start x σ o.1 : ℚ)) (fun o => (x.r o.1 : ℚ))) |
| 351 | (Shares σ) s |
| 352 | le := Servers.le |
| 353 | embed h _ d := Servers.embed h d |
| 354 | |
| 355 | /-- The time an operation needs on the first machine; for shops, where the |
| 356 | time does not depend on the machine, its processing time. Without machines no |
| 357 | operation can be processed, and the time is taken to be `1`. -/ |
| 358 | def opTime (x : Inst) (o : Op x) : ℕ := |
| 359 | if h : 0 < x.machines then x.p o.1 o.2 ⟨0, h⟩ else 1 |
| 360 | |
| 361 | /-- The no-wait field. -/ |
| 362 | def noWait : Module kernel where |
| 363 | Value := Shops.NoWait |
| 364 | Data _ _ := Unit |
| 365 | admits _ _ _ := True |
| 366 | constraint v x _ σ := v = .noWait → |
| 367 | ∀ j, kernel.completion x σ j = kernel.start x σ j + ∑ k, (opTime x ⟨j, k⟩ : NNRat) |
| 368 | le v w := decide (v = w) |
| 369 | embed _ _ _ := () |
| 370 | |
| 371 | /-- Of two operations of a job, the later one waits for the delay, unless both |
| 372 | delays between them are `0`. -/ |
| 373 | def Delayed (x : Inst) (t : Transportation.Delays x.toShop) (σ : Sched x) : Prop := |
| 374 | ∀ j (k l : Fin (x.ops j)), k ≠ l → (t j k l = 0 ∧ t j l k = 0) ∨ |
| 375 | opFinish σ ⟨j, k⟩ + (t j k l : NNRat) ≤ opStart σ ⟨j, l⟩ ∨ |
| 376 | opFinish σ ⟨j, l⟩ + (t j l k : NNRat) ≤ opStart σ ⟨j, k⟩ |
| 377 | |
| 378 | /-- The machines that the pieces of an operation occupy. -/ |
| 379 | def opMachines {x : Inst} (σ : Sched x) (o : Op x) : Finset (Fin x.machines) := |
| 380 | ((piecesOf σ o).map Piece.machines).foldr (· ∪ ·) ∅ |
| 381 | |
| 382 | /-- A single robot carries every job from each operation to the next, and |
| 383 | between two transports it travels empty from the machines where it delivers |
| 384 | the one to the machines where it picks up the other. -/ |
| 385 | def Carried (x : Inst) (t : Transportation.Delays x.toShop) |
| 386 | (e : Transportation.EmptyMoves x.toShop) (σ : Sched x) : Prop := |
| 387 | ∃ depart : (j : Fin x.jobs) → Fin (x.ops j) → ℕ, |
| 388 | (∀ j (k l : Fin (x.ops j)), l.val = k.val + 1 → |
| 389 | opFinish σ ⟨j, k⟩ ≤ (depart j k : NNRat) ∧ |
| 390 | ((depart j k + t j k l : ℕ) : NNRat) ≤ opStart σ ⟨j, l⟩) ∧ |
| 391 | ∀ j (k l : Fin (x.ops j)) j' (k' l' : Fin (x.ops j')), l.val = k.val + 1 → |
| 392 | l'.val = k'.val + 1 → (⟨j, k⟩ : Op x) ≠ ⟨j', k'⟩ → |
| 393 | depart j k + t j k l + |
| 394 | Transportation.emptyTime e (opMachines σ ⟨j, l⟩) (opMachines σ ⟨j', k'⟩) ≤ |
| 395 | depart j' k' ∨ |
| 396 | depart j' k' + t j' k' l' + |
| 397 | Transportation.emptyTime e (opMachines σ ⟨j', l'⟩) (opMachines σ ⟨j, k⟩) ≤ |
| 398 | depart j k |
| 399 | |
| 400 | /-- The field of transportation delays. -/ |
| 401 | def transportation : Module kernel where |
| 402 | Value := Transportation.Value |
| 403 | Data _ x := Transportation.Data x.toShop |
| 404 | admits v _ d := v.admits d |
| 405 | constraint v x d σ := Delayed x d.1 σ ∧ (v.robot = true → Carried x d.1 d.2 σ) |
| 406 | le := Transportation.Value.le |
| 407 | embed _ _ d := d |
| 408 | |
| 409 | /-- A piece of an operation occupies a machine. -/ |
| 410 | def Occupies {x : Inst} (σ : Sched x) (o : Op x) (i : Fin x.machines) : Prop := |
| 411 | ∃ q ∈ piecesOf σ o, i ∈ q.machines |
| 412 | |
| 413 | /-- Every operation on a machine is immediately followed by another one on |
| 414 | that machine, unless none completes later. -/ |
| 415 | def Contiguous (x : Inst) (σ : Sched x) : Prop := |
| 416 | ∀ i (a : Op x), Occupies σ a i → |
| 417 | (∃ b : Op x, b ≠ a ∧ Occupies σ b i ∧ opStart σ b = opFinish σ a) ∨ |
| 418 | ∀ b : Op x, Occupies σ b i → opFinish σ b ≤ opFinish σ a |
| 419 | |
| 420 | /-- The no-idle field. -/ |
| 421 | def noIdle : Module kernel where |
| 422 | Value := ShopExtras.NoIdle |
| 423 | Data _ _ := Unit |
| 424 | admits _ _ _ := True |
| 425 | constraint v x _ σ := v = .noIdle → Contiguous x σ |
| 426 | le v w := decide (v = w) |
| 427 | embed _ _ _ := () |
| 428 | |
| 429 | /-- On some machine, operation `b` follows operation `a`: `b` starts after `a` |
| 430 | completes, and no other operation on that machine lies in between. -/ |
| 431 | def Follows {x : Inst} (σ : Sched x) (a b : Op x) : Prop := |
| 432 | opFinish σ a ≤ opStart σ b ∧ ∃ i, Occupies σ a i ∧ Occupies σ b i ∧ |
| 433 | ∀ c : Op x, c ≠ a → c ≠ b → Occupies σ c i → |
| 434 | ¬ (opFinish σ a ≤ opStart σ c ∧ opFinish σ c ≤ opStart σ b) |
| 435 | |
| 436 | /-- The batch-setup field. -/ |
| 437 | def batchSetups : Module kernel where |
| 438 | Value := ShopExtras.BatchSetups |
| 439 | Data v x := ShopExtras.BatchSetups.Data v x.toShop |
| 440 | admits _ _ _ := True |
| 441 | constraint v x d σ := ∀ a b : Op x, |
| 442 | v.batch (x := x.toShop) d a.1 ≠ v.batch (x := x.toShop) d b.1 → |
| 443 | (Shares σ a b → opFinish σ a ≤ opStart σ b ∨ opFinish σ b ≤ opStart σ a) ∧ |
| 444 | (Follows σ a b → opFinish σ a + (v.setup (x := x.toShop) d (v.batch (x := x.toShop) d a.1) |
| 445 | (v.batch (x := x.toShop) d b.1) : NNRat) ≤ opStart σ b) |
| 446 | le := ShopExtras.BatchSetups.le |
| 447 | embed h x d := ShopExtras.BatchSetups.embed h x.toShop d |
| 448 | |
| 449 | axiom interruption_sound : interruption.Sound |
| 450 | axiom jobStructure_sound : jobStructure.Sound |
| 451 | axiom environment_sound : environment.Sound |
| 452 | axiom processingTimes_sound : processingTimes.Sound |
| 453 | axiom machineSets_sound : machineSets.Sound |
| 454 | axiom server_sound : server.Sound |
| 455 | axiom noWait_sound : noWait.Sound |
| 456 | axiom transportation_sound : transportation.Sound |
| 457 | axiom noIdle_sound : noIdle.Sound |
| 458 | axiom batchSetups_sound : batchSetups.Sound |
| 459 | axiom startsBeforeCompletion : kernel.StartsBeforeCompletion |
| 460 | |
| 461 | end Lax434175.Operations |
| 462 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments