← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2009/verbeek-schmaltz/verbeek/instantiations/scheduling/circuit-switching-global/circuit.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2009/verbeek-schmaltz/verbeek/instantiations/scheduling/circuit-switching-global/circuit.lisp
 
1
#|$ACL2s-Preamble$;
 
2
;; Julien Schmaltz
 
3
;; File: circuit-scheduling.lisp
 
4
;; here we define a function that realises a circuit switching
 
5
;; technique, we prove it correct and we prove that it is a valid
 
6
;; instance of the scheduling function of GeNoC.
 
7
;; Revised: Nov 13th 2005, JS
 
8
 
 
9
(begin-book);$ACL2s-Preamble$|#
 
10
 
 
11
(in-package "ACL2")
 
12
(include-book "../../../generic-modules/GeNoC-scheduling")
 
13
(include-book "intersect")
 
14
(include-book "../../ntkstate/simple/simple")
 
15
(include-book "../../synchronization/circuit-global/circuit")
 
16
(include-book "../../genoc/simple-ct-global/trlst-equal")
 
17
 
 
18
;;-----------------------------------------------------
 
19
;;
 
20
;; DEFINITION OF THE CIRCUIT SWITCHED SCHEDULING POLICY
 
21
;;
 
22
;;-----------------------------------------------------
 
23
 
 
24
 
 
25
(defun test_prev_routes (r? prev)
 
26
  ;; function that returns a route that uses nodes
 
27
  ;; that are not in prev or returns nil if there is no
 
28
  ;; such route. 
 
29
  (cond ((endp r?)
 
30
         nil)
 
31
        ((endp prev)
 
32
         t)
 
33
        ((no_intersectp r? (car prev))
 
34
         (test_prev_routes r? (cdr prev)))
 
35
        (t
 
36
         nil)))
 
37
 
 
38
(defun ct-scheduler (TrLst Scheduled Arrived prev measureAcc ntkstate)
 
39
  (if (endp trlst)
 
40
    (mv (rev Scheduled) (rev Arrived) (rev measureAcc) ntkstate)
 
41
    (let ((v (car TrLst)))
 
42
      (mv-let (newntkstate r?)
 
43
              (inst-test_routes ntkstate v)
 
44
              (if (test_prev_routes r? prev)
 
45
                ;; if there is a possible route, then remove
 
46
                ;; it and add it to to prev
 
47
                (ct-scheduler (cdr TrLst)
 
48
                              Scheduled
 
49
                              (cons v Arrived)
 
50
                              (cons r? prev)
 
51
                              (cons 0 measureAcc)
 
52
                              newntkstate)
 
53
                ;; otherwise the transaction is delayed
 
54
                (ct-scheduler (cdr TrLst)
 
55
                              (cons v Scheduled) 
 
56
                              Arrived
 
57
                              prev
 
58
                              (cons (len (car (RoutesV (car TrLst)))) measureAcc)
 
59
                              newntkstate))))))
 
60
 
 
61
;; returns t if there's no route possible in
 
62
;; the current ntkstate
 
63
(defun no-good-routes (TrLst ntkstate)
 
64
  (if (endp trlst)
 
65
    t
 
66
    (mv-let (newntkstate r?)
 
67
            (inst-test_routes ntkstate (car trlst))
 
68
            (if (not r?)
 
69
              (no-good-routes (cdr TrLst) newntkstate)
 
70
              nil))))
 
71
 
 
72
(defun sum-of-lst (lst)
 
73
  (if (endp lst)
 
74
    0
 
75
    (nfix (+ (car lst) (sum-of-lst (cdr lst))))))
 
76
 
 
77
;; returns a list of the lengths of the routes of the travels in TrLst
 
78
(defun RouteLengths-TrLst (TrLst)
 
79
  (if (endp TrLst)
 
80
    nil
 
81
    (cons (len (car (RoutesV (car TrLst)))) (RouteLengths-TrLst (cdr TrLst)))))
 
82
; the measure is a list of lengths of the routes
 
83
(defun ct-initial-measure (trlst nodeset ntkstate order)
 
84
  (declare (ignore nodeset ntkstate order))
 
85
  (sum-of-lst (RouteLengths-TrLst trlst)))
 
86
(defun ct-legal-measure (measure TrLst NodeSet ntkstate order)
 
87
  (declare (ignore nodeset ntkstate order))
 
88
  (equal measure (sum-of-lst (RouteLengths-Trlst trlst))))
 
89
(defun ct-get_next_priority (x)
 
90
  x)
 
91
 
 
92
; circuit scheduling assume that:
 
93
; 1.) the TrLst is not empty
 
94
; 2.) there is at least one route possible
 
95
; 3.) the current measure is a list with the lengths of the current routes
 
96
(defun ct-scheduling-assumptions (TrLst NodeSet ntkstate order)
 
97
  (declare (ignore NodeSet order))
 
98
 ; (and (not (endp TrLst))
 
99
       (not (no-good-routes TrLst ntkstate)))
 
100
 
 
101
 
 
102
;Scheduling:
 
103
; IN:  List of Travels
 
104
;      Measure
 
105
;      NodeSet
 
106
;      ntkstate
 
107
;     order
 
108
; OUT: List of En Route TMs
 
109
;      List of Arrived Travels
 
110
;      Valid networkstate
 
111
(defun ct-scheduling (TrLst NodeSet ntkstate order)
 
112
  (if (not (ct-scheduling-assumptions TrLst NodeSet ntkstate order))
 
113
    (mv (totmissives TrLst) nil nil ntkstate)
 
114
    ; otherwise: schedule the travels
 
115
    (mv-let (newTrlst Arrived newmeasure newntkstate)
 
116
            (ct-scheduler TrLst nil nil nil nil ntkstate)
 
117
            (mv (totmissives newTrlst)
 
118
                Arrived
 
119
                (sum-of-lst newmeasure)
 
120
                (update-ntkstate newntkstate newtrlst)))))
 
121
 
 
122
;-------------------------------------
 
123
; the instantiations used in this file
 
124
;------------------------------------
 
125
(defmacro inst-scheduling (TrLst NodeSet ntkstate order)
 
126
         (list 'ct-scheduling TrLst NodeSet ntkstate order))
 
127
(defmacro inst-scheduling-assumptions (TrLst NodeSet ntkstate order)
 
128
         (list 'ct-scheduling-assumptions TrLst NodeSet ntkstate order))
 
129
(defmacro inst-legal-measure (measure TrLst nodeset ntkstate order)
 
130
         (list 'ct-legal-measure measure TrLst nodeset ntkstate order))
 
131
(defmacro inst-initial-measure (TrLst nodeset ntkstate order)
 
132
         (list 'ct-initial-measure TrLst nodeset ntkstate order))
 
133
(defmacro inst-get_next_priority (order)
 
134
         (list 'ct-get_next_priority order))
 
135
 
 
136
 
 
137
;-----------------------------------------------
 
138
;
 
139
; PROVING COMPLIANCE TO GENERIC SCHEDULING
 
140
;
 
141
;
 
142
; The proof is completely equal to the proof
 
143
; of packet-scheduling.
 
144
;
 
145
;-----------------------------------------------
 
146
 
 
147
;-------------------------------
 
148
; non-tail recursive functions
 
149
; for ct-scheduler
 
150
;-------------------------------
 
151
(defun ct-scheduler-nt-car (TrLst prev ntkstate)
 
152
  ;; car is the first output and corresponds to the scheduled travels
 
153
  (if (endp TrLst)
 
154
    nil
 
155
    (let ((v (car TrLst)))
 
156
      (mv-let (newntkstate r?)
 
157
              (inst-test_routes ntkstate v)
 
158
              (if (test_prev_routes r? prev)
 
159
                  (ct-scheduler-nt-car (cdr TrLst) (cons r? prev) 
 
160
                                       newntkstate)
 
161
                  (cons v (ct-scheduler-nt-car (cdr TrLst) prev 
 
162
                                               newntkstate)))))))
 
163
(defthm ct-scheduler-nt-equal
 
164
  (equal (car (ct-scheduler TrLst Scheduled ArrivedAcc prev measureAcc ntkstate))
 
165
         (append (rev scheduled) (ct-scheduler-nt-car TrLst prev ntkstate)))
 
166
  :hints (("Goal" :in-theory (disable ct-test_routes))))
 
167
 
 
168
(defun ct-scheduler-nt-mv1 (TrLst prev ntkstate)
 
169
  (if (endp TrLst)
 
170
    nil
 
171
    (let ((v (car TrLst)))
 
172
      (mv-let (newntkstate r?)
 
173
              (inst-test_routes ntkstate v)
 
174
              (if (test_prev_routes r? prev)
 
175
                (cons v (ct-scheduler-nt-mv1 (cdr TrLst) (cons r? prev) 
 
176
                                             newntkstate))
 
177
                  (ct-scheduler-nt-mv1 (cdr TrLst) prev 
 
178
                                       newntkstate))))))
 
179
(defthm ct-scheduler-nt-mv1-equal
 
180
  (equal (mv-nth 1 (ct-scheduler TrLst Scheduled  ArrivedAcc prev measureAcc ntkstate))
 
181
         (append (rev ArrivedAcc) (ct-scheduler-nt-mv1 TrLst prev ntkstate)))
 
182
  :hints (("Goal" :in-theory (disable ct-test_routes))))
 
183
 
 
184
(defun ct-scheduler-nt-mv2 (TrLst prev ntkstate)
 
185
  (if (endp TrLst)
 
186
    nil
 
187
    (let ((v (car TrLst)))
 
188
      (mv-let (newntkstate r?)
 
189
              (inst-test_routes ntkstate v)
 
190
              (if (test_prev_routes r? prev)
 
191
                  (cons 0 
 
192
                        (ct-scheduler-nt-mv2 (cdr TrLst) (cons r? prev) 
 
193
                                             newntkstate))
 
194
                  (cons (len (car (RoutesV (car TrLst))))
 
195
                        (ct-scheduler-nt-mv2 (cdr TrLst) prev 
 
196
                                             newntkstate)))))))
 
197
(defthm ct-scheduler-nt-mv2-equal
 
198
  (equal (mv-nth 2 (ct-scheduler TrLst Scheduled ArrivedAcc prev measureAcc ntkstate))
 
199
         (append (rev measureAcc) (ct-scheduler-nt-mv2 TrLst prev ntkstate)))
 
200
  :hints (("Goal" :in-theory (disable ct-test_routes))))
 
201
(defthm ct-scheduler-nt-mv3-equal
 
202
  (equal (mv-nth 3 (ct-scheduler TrLst Scheduler ArrivedAcc prev measureAcc ntkstate))
 
203
         ntkstate))
 
204
 
 
205
(defthm ntkstate-test-routes-mv0
 
206
  (equal (mv-nth 0 (ct-test_routes ntkstate v)) ntkstate))
 
207
(defthm ntkstate-test-routes-car
 
208
  (equal (car (ct-test_routes ntkstate v)) ntkstate))  
 
209
 
 
210
 
 
211
 
 
212
;;---------------------------------------------------------------------
 
213
;;
 
214
;; PROOF OF DECREASING MEASURE
 
215
;;
 
216
;;---------------------------------------------------------------------
 
217
(defthm good_route-implies-smaller-routes
 
218
  (mv-let (newntkstate r?)
 
219
          (inst-test_routes ntkstate (car TrLst))
 
220
          (implies (test_prev_routes r? prev)
 
221
                   (< (car (ct-scheduler-nt-mv2 TrLst prev newntkstate))
 
222
                      (car (RouteLengths-TrLst TrLst))))))
 
223
 
 
224
(defun elts-<= (x y)
 
225
  (if (endp x)
 
226
      (endp y)
 
227
      (and (<= (car x) (car y))
 
228
           (natp (car x)) (natp (car y))
 
229
           (elts-<= (cdr x) (cdr y)))))
 
230
 
 
231
(defthm elts-<=-implies-sum-<=
 
232
  (implies (elts-<= x y)
 
233
           (<= (sum-of-lst x) (sum-of-lst y))))
 
234
 
 
235
(defthm plus-<
 
236
  (implies (and (< x1 y1)
 
237
                (<= x y))
 
238
           (< (+ x1 x)
 
239
              (+ y1 y))))
 
240
 
 
241
(defthm smaller-car-implies-smaller-sum
 
242
  (implies (and (< (car x) (car y))
 
243
                (elts-<= x y))
 
244
      (< (sum-of-lst x) (sum-of-lst y))))
 
245
 
 
246
(defthm scheduled-routes-<=-original
 
247
  (elts-<= (ct-scheduler-nt-mv2 TrLst prev ntkstate)
 
248
           (RouteLengths-TrLst TrLst)))
 
249
 
 
250
(defthm good-route-implies-smaller-measure
 
251
  (mv-let (newntkstate r?)
 
252
          (inst-test_routes ntkstate (car TrLst))
 
253
          (declare (ignore newntkstate))
 
254
          (implies (and (consp TrLst)
 
255
                        r?)
 
256
                   (< (sum-of-lst (ct-scheduler-nt-mv2 TrLst nil ntkstate))
 
257
                      (sum-of-lst (RouteLengths-TrLst TrLst)))))
 
258
  :hints (("Goal" :in-theory (disable get_buff orgv routesv
 
259
                                      sum-of-lst good_route-implies-smaller-routes))))
 
260
 
 
261
(defthm good-route-possible-implies-smaller-measure
 
262
  (implies (not (no-good-routes TrLst ntkstate))
 
263
           (< (sum-of-lst (ct-scheduler-nt-mv2 TrLst nil ntkstate))
 
264
              (sum-of-lst (RouteLengths-TrLst TrLst))))
 
265
  :hints (("Subgoal *1/3" :use (:instance good-route-implies-smaller-measure))
 
266
          ("Subgoal *1/2" :use (:instance good-route-implies-smaller-measure))
 
267
 
 
268
))
 
269
 
 
270
;;---------------------------------------------------------------------
 
271
;;
 
272
;; PROOF OF GeNoC CONSTRAINTS
 
273
;;
 
274
;;---------------------------------------------------------------------
 
275
;; 1/ proof that the measure decreases if assumptions are met
 
276
;; -----------------------------------
 
277
(defthm ct-measure-decreases
 
278
    (implies (and (ct-legal-measure measure trlst nodeset ntkstate order)
 
279
                  (ct-scheduling-assumptions trlst NodeSet ntkstate order))
 
280
             (O< (mv-nth 2 (ct-scheduling TrLst NodeSet ntkstate order))
 
281
                 (acl2-count measure))))
 
282
 
 
283
 
 
284
;;----------------------------------------------------------
 
285
 
 
286
;; 2/ we prove that the ids of the delayed and scheduled travels
 
287
;; are part of the initial travel list
 
288
;; -----------------------------------
 
289
(in-theory (disable update-ntkstate))
 
290
(defthm subsetp-scheduled-id-ct
 
291
  (subsetp (V-ids (ct-scheduler-nt-car TrLst prev ntkstate))
 
292
           (V-ids TrLst)))
 
293
(defthm subsetp-delayed-id-ct
 
294
  (subsetp (V-ids (ct-scheduler-nt-mv1 TrLst prev ntkstate))
 
295
           (V-ids TrLst)))
 
296
;------------------------------------------------------------------
 
297
 
 
298
;; 3/ we prove that the list of scheduled travels is a 
 
299
;; valid travel list
 
300
;; --------------------------------------------------
 
301
 
 
302
 
 
303
;; proof for the scheduled travels
 
304
;; -------------------------------
 
305
(local 
 
306
 (defthm validfields-trlst-ct-sched
 
307
   (implies (ValidFields-TrLst TrLst nodeset)
 
308
            (ValidFields-TrLst (ct-scheduler-nt-car TrLst prev ntkstate) nodeset))))
 
309
 
 
310
(local 
 
311
 (defthm not-member-V-ids-ct-sched
 
312
   (implies (not (member-equal e (V-ids TrLst)))
 
313
            (not 
 
314
             (member-equal 
 
315
              e 
 
316
              (V-ids 
 
317
               (ct-scheduler-nt-car TrLst prev ntkstate)))))))
 
318
 
 
319
(defthm no-duplicatesp-ct-sched
 
320
  (implies (no-duplicatesp-equal (V-ids TrLst))
 
321
           (no-duplicatesp-equal
 
322
            (V-ids (ct-scheduler-nt-car TrLst prev ntkstate)))))
 
323
 
 
324
(defthm cons-v-ids
 
325
  (equal (consp (v-ids TrLst))
 
326
         (consp TrLst)))
 
327
 
 
328
(defthm TrLstp-scheduled-ct
 
329
  (implies (TrLstp TrLst nodeset)
 
330
           (TrLstp (ct-scheduler-nt-car TrLst prev ntkstate) nodeset)))
 
331
 
 
332
;; proof for the delayed travels
 
333
;; -----------------------------
 
334
(local 
 
335
 (defthm validfields-trlst-ct-del
 
336
   (implies (ValidFields-TrLst TrLst nodeset)
 
337
            (ValidFields-TrLst 
 
338
             (ct-scheduler-nt-mv1 TrLst prev ntkstate) nodeset))))
 
339
 
 
340
(local 
 
341
 (defthm not-member-V-ids-ct-del
 
342
   (implies (not (member-equal e (V-ids TrLst)))
 
343
            (not 
 
344
             (member-equal 
 
345
              e 
 
346
              (V-ids 
 
347
               (ct-scheduler-nt-mv1 TrLst prev ntkstate)))))))
 
348
 
 
349
(local (defthm no-duplicatesp-ct-del
 
350
         (implies (no-duplicatesp-equal (V-ids TrLst))
 
351
                  (no-duplicatesp-equal
 
352
                   (V-ids (ct-scheduler-nt-mv1 TrLst prev ntkstate))))))
 
353
 
 
354
(defthm TrLstp-delayed-ct
 
355
  (implies (TrLstp TrLst nodeset)
 
356
           (TrLstp (ct-scheduler-nt-mv1 TrLst prev ntkstate) nodeset)))
 
357
;;--------------------------------------------------------------------
 
358
 
 
359
 
 
360
;; 4/ correctness of the scheduled travels
 
361
;; ------------------------------------------------------
 
362
 
 
363
(defthm extract-sublst-cons
 
364
  (implies (not (member-equal id Ids))
 
365
           (equal (extract-sublst (cons (list id org frm routes flit time) L) 
 
366
                                  Ids)
 
367
                  (extract-sublst L Ids))))
 
368
 
 
369
 
 
370
(defthm test_prev_routes-member-equal
 
371
  (mv-let (newntkstate r?)
 
372
          (inst-good_route? ntkstate org dest routes)
 
373
          (declare (ignore newntkstate))
 
374
          (implies r?
 
375
                   (member-equal r? routes))))
 
376
 
 
377
(defthm no-duplicatesp-equal-append
 
378
  ;; to move to misc
 
379
  (implies (no-duplicatesp-equal (append (list x) (v-ids y)))
 
380
           (not (member-equal x (v-ids y)))))             
 
381
 
 
382
 
 
383
(defthm ct-scheduled-correctness
 
384
  (let ((arrived (ct-scheduler-nt-mv1 TrLst prev st))) 
 
385
    (implies (TrLstp TrLst nodeset)
 
386
             (s/d-travel-correctness
 
387
              arrived
 
388
              (extract-sublst TrLst (V-ids arrived)))))
 
389
  :hints (("GOAL"
 
390
           :in-theory (disable len extract-sublst))
 
391
          ("Subgoal *1/9"
 
392
           :in-theory (disable len ct-test_routes))
 
393
          ("Subgoal *1/5"
 
394
           :in-theory (disable len ct-test_routes))))
 
395
 
 
396
 
 
397
 
 
398
;; 5/ We prove that Delayed is equal to filtering TrLst
 
399
;; according to the ids of Delayed
 
400
;; ----------------------------------------------------
 
401
(defthm ct-delayed-correctness
 
402
  (let ((traveling (ct-scheduler-nt-car TrLst prev st))) 
 
403
    (implies (TrLstp TrLst nodeset)
 
404
             (subsetp
 
405
              (V-ids traveling) (v-ids Trlst))))
 
406
  :hints (("GOAL" 
 
407
           :in-theory (disable len ct-test_routes)
 
408
           :do-not '(eliminate-destructors)))
 
409
  :rule-classes nil)
 
410
 
 
411
 
 
412
(defthm ct-delayed-correctness-org
 
413
  (let ((traveling (ct-scheduler-nt-car TrLst prev st))) 
 
414
    (implies (TrLstp TrLst nodeset)
 
415
             (subsetp (V-orgs traveling) (v-orgs Trlst))))
 
416
  :hints (("GOAL" 
 
417
           :in-theory (disable len ct-test_routes)
 
418
           :do-not '(eliminate-destructors)))
 
419
  :rule-classes nil)
 
420
 
 
421
 
 
422
(defthm ct-delayed-correctness-frm
 
423
  (let ((traveling (ct-scheduler-nt-car TrLst prev st))) 
 
424
    (implies (TrLstp TrLst nodeset)
 
425
             (subsetp
 
426
              (V-frms traveling) (v-frms Trlst))))
 
427
  :hints (("GOAL" 
 
428
           :in-theory (disable len ct-test_routes)
 
429
           :do-not '(eliminate-destructors)))
 
430
  :rule-classes nil)
 
431
 
 
432
 
 
433
(defthm ct-delayed-correctness-destination
 
434
  (let ((traveling (ct-scheduler-nt-car TrLst prev st))) 
 
435
    (implies (TrLstp TrLst nodeset)
 
436
             (subsetp
 
437
              (Tm-dests (totmissives traveling)) (Tm-dests (totmissives Trlst)))))
 
438
  :hints (("GOAL" 
 
439
           :in-theory (disable len ct-test_routes)
 
440
           :do-not '(eliminate-destructors))
 
441
          ("Subgoal *1/9" :in-theory (e/d (ct-test_routes)
 
442
                                          (ct-chk_avail))))
 
443
  :rule-classes nil)
 
444
 
 
445
 
 
446
(defthm ct-delayed-correctness-destination-m
 
447
  (let ((traveling (ct-scheduler-nt-car TrLst prev st))) 
 
448
    (implies (TrLstp TrLst nodeset)
 
449
             (subsetp
 
450
              (m-dests (tomissives(totmissives traveling))) 
 
451
              (m-dests (tomissives (totmissives Trlst))))))
 
452
  :hints (("GOAL" 
 
453
           :in-theory (disable len ct-test_routes ct-chk_avail)
 
454
           :do-not '(eliminate-destructors))
 
455
          ("Subgoal *1/9" :in-theory (e/d (ct-test_routes)
 
456
                                          (ct-chk_avail trlstp))))
 
457
  :rule-classes nil)
 
458
 
 
459
 
 
460
(defthm ct-delayed-correctness-ultime
 
461
  (implies (Trlstp trlst nodeset)
 
462
           (equal (tomissives (totmissives (ct-scheduler-nt-car TrLst prev st)))
 
463
                  (tomissives (totmissives (extract-sublst
 
464
                                            trlst
 
465
                                            (v-ids (ct-scheduler-nt-car TrLst prev st)))))))
 
466
  :hints (("GOAL" 
 
467
           :in-theory (disable len ct-test_routes))
 
468
          ("Subgoal *1/9" :in-theory (e/d (ct-test_routes)
 
469
                                          (ct-chk_avail)))))
 
470
 
 
471
(defthm equal-tmids-vids-pkttraveling
 
472
  (equal (v-ids (ct-scheduler-nt-car TrLst prev p)) 
 
473
         (tm-ids (totmissives (ct-scheduler-nt-car TrLst prev p))))
 
474
  :rule-classes nil)    
 
475
 
 
476
 
 
477
(defthm equal-mids-tmids-vids-pkttraveling
 
478
  (equal (v-ids (ct-scheduler-nt-car TrLst prev p)) 
 
479
         (m-ids (tomissives (totmissives (ct-scheduler-nt-car TrLst prev p)))))
 
480
  :hints (("Goal" :in-theory (disable ct-test_routes)))
 
481
  :rule-classes nil)
 
482
 
 
483
(defthm ct-delayed-correctness-ultime-totmissives
 
484
  (implies (Trlstp trlst nodeset)
 
485
           (equal (tomissives 
 
486
                   (totmissives (ct-scheduler-nt-car TrLst prev st)))
 
487
                  (tomissives 
 
488
                   (totmissives 
 
489
                    (extract-sublst trlst
 
490
                                    (tm-ids (totmissives (ct-scheduler-nt-car TrLst prev st))))))))
 
491
  :hints (("GOAL"
 
492
           :in-theory (disable trlstp len extract-sublst ct-test_routes))))
 
493
 
 
494
(defthm ct-delayed-correctness-ultime-totmissives-bis
 
495
  (implies (Trlstp trlst nodeset)
 
496
           (equal (tomissives (totmissives (ct-scheduler-nt-car TrLst prev p)))
 
497
                  (tomissives  (extract-sublst (totmissives trlst)
 
498
                                               (tm-ids (totmissives (ct-scheduler-nt-car TrLst prev p)))))))
 
499
  :hints (("Goal"   :do-not-induct t
 
500
                    :in-theory (disable trlstp len ct-test_routes))))
 
501
 
 
502
 
 
503
 
 
504
(defthm ct-delayed-correctness-ultime-totmissives-final
 
505
  (implies (Trlstp trlst nodeset)
 
506
           (equal (tomissives (totmissives (ct-scheduler-nt-car TrLst prev p)))
 
507
                  (extract-sublst (tomissives(totmissives trlst))
 
508
                                  (tm-ids (totmissives (ct-scheduler-nt-car TrLst prev p))))))
 
509
  
 
510
  :hints (("Goal"   :do-not-induct t
 
511
                    :use ((:instance ToTMissives-extract-sublst (L trslt) 
 
512
                           (ids (v-ids (ct-scheduler-nt-car TrLst prev p))))
 
513
                          (:instance ToMissives-extract-sublst (L (totmissives TRlst)) (ids (v-ids (ct-scheduler-nt-car TrLst prev p))))    
 
514
                          )
 
515
                    :in-theory (disable extract-sublst v-ids default-car assoc-equal
 
516
                                        nth-with-large-index nth-add1
 
517
                                        len ct-scheduler-nt-car trlstp))))
 
518
 
 
519
; -----------------------------------------------------------
 
520
 
 
521
;; -----------------------------------------------------------
 
522
;; 6/ we prove that the ids of the delayed travels are distinct
 
523
;; from those of the scheduled travels
 
524
;; ------------------------------------------------------------
 
525
 
 
526
(defthm not-in-cons
 
527
  (implies (and (not-in x y) 
 
528
                (not (member-equal e x)))
 
529
           (not-in x (cons e y))))
 
530
 
 
531
(defthm not-in-v-ids-ct
 
532
  (implies (trlstp trlst nodeset)
 
533
           (not-in (v-ids (ct-scheduler-nt-car TrLst prev ntkstate))
 
534
                   (v-ids (ct-scheduler-nt-mv1 TrLst prev ntkstate))))
 
535
  :hints (("Goal" :in-theory (disable ct-test_routes))))
 
536
(defthm not-in-v-ids-ct2
 
537
  (implies (trlstp trlst nodeset)
 
538
           (not-in (v-ids (ct-scheduler-nt-mv1 TrLst prev ntkstate))
 
539
                   (v-ids (ct-scheduler-nt-car TrLst prev ntkstate))))
 
540
  :hints (("Goal" :in-theory (disable ct-test_routes))))
 
541
(defthm subsetp-output-input
 
542
  (subsetp (append (V-ids (ct-scheduler-nt-car TrLst prev st))
 
543
                   (V-ids (ct-scheduler-nt-mv1 TrLst prev st )))
 
544
           (V-ids TrLst))
 
545
    :hints (("Goal" :in-theory (disable ct-test_routes))))
 
546
 
 
547
(defthm subsetp-input-output
 
548
  (subsetp (V-ids TrLst)
 
549
           (append (V-ids (ct-scheduler-nt-car TrLst prev st))
 
550
                   (V-ids (ct-scheduler-nt-mv1 TrLst prev st))))
 
551
    :hints (("Goal" :in-theory (disable ct-test_routes))))
 
552
 
 
553
 
 
554
(defthm input=output
 
555
  (let ((out (ct-scheduling trlst NodeSet ntkstate order)))
 
556
    (implies (true-listp trlst)
 
557
             (trlst-equal (append (mv-nth 0 out) (mv-nth 1 out))
 
558
                          trlst)))
 
559
  :hints (("Goal" :use ((:instance subsetp-input-output (prev nil) (st ntkstate))
 
560
                        (:instance subsetp-output-input (prev nil) (st ntkstate))))))
 
561
 
 
562
(defthm nil-trlstp
 
563
  (trlstp nil nodeset))
 
564
 
 
565
 
 
566
;; -----------------------------------------------------------
 
567
;; Compliance to generic model
 
568
;; ------------------------------------------------------------
 
569
 
 
570
(definstance genericscheduling check-compliance-ct-scheduling
 
571
  :functional-substitution
 
572
  ((scheduling ct-scheduling)
 
573
   (scheduling-assumptions ct-scheduling-assumptions)
 
574
   (legal-measure ct-legal-measure)
 
575
   (initial-measure ct-initial-measure)
 
576
   (get_next_priority ct-get_next_priority)
 
577
   (ValidParamsp 2DMesh-Validparamsp)
 
578
   (NodeSetGenerator 2DMesh-NodeSetGenerator)
 
579
   (loadbuffers inst-Loadbuffers)
 
580
   (readbuffers inst-Readbuffers)
 
581
   (StateGenerator inst-StateGenerator)
 
582
   (ValidstateParamsp inst-ValidStateParamsp)
 
583
   (req_trans inst-req_trans)
 
584
   (process_req inst-process_req)
 
585
   (chk_avail inst-chk_avail)
 
586
   (good_route? inst-good_route?)
 
587
   (test_routes inst-test_routes))
 
588
  :rule-classes nil
 
589
  :otf-flg t
 
590
  :hints (("goal" :do-not-induct t
 
591
                  :in-theory (disable trlstp))
 
592
; Matt K.: The following subgoal hint was changed to "8.2'" from "8" because of
 
593
; the change after ACL2 Version 3.6.1 to speed up evaluation of calls of mv-let
 
594
; (which was a change to the way ACL2 translates mv-let expressions in theorems
 
595
; into internal form).  It seems that this mv-let change may have affected the
 
596
; way make-event expansion is done here.
 
597
          ("Subgoal 7.2'" ; changed after v4-3 from "Subgoal 8.2'", for tau system
 
598
           :use ((:instance tomissives-extract-sublst (l (totmissives trlst))
 
599
                            (ids (tm-ids (totmissives trlst))))
 
600
                 (:instance totmissives-extract-sublst (l trlst)
 
601
                            (ids (v-ids trlst)))
 
602
                 (:instance extract-sublst-identity)))))
 
603
 
 
604
(in-theory (enable update-ntkstate))#|ACL2s-ToDo-Line|#