-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathilp-test.scm
1174 lines (1133 loc) · 70 KB
/
ilp-test.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
#!r6rs
; This program and the accompanying materials are made available under the
; terms of the MIT license (X11 license) which accompanies this distribution.
; Author: R. Schöne
(library
(mquat ilp-test)
(export run-test test-cli-call)
(import (rnrs) (racr core) (racr testing)
(mquat utils) (mquat ilp) (mquat join) (mquat basic-ag) (mquat ast)
(mquat constants) (mquat ast-generation) (mquat ui))
;; Testing generated ILP, whether correct results are computed for small models
(define tmp-lp "test/tmp.lp")
(define (wrong-id who id) (error who (string-append "Unknown test case id '" (number->string id) "'\n")))
(define (change-hw-prov ast prop-name new-value . res-names)
(let ([resources (if (null? res-names) (=every-pe ast)
(filter (lambda (res) (find (lambda (name) (string=? (->name res) name)) res-names))
(=every-pe ast)))]
[f (if (procedure? new-value) new-value (lambda _ new-value))])
(for-each (lambda (res) (rewrite-terminal 'value (=provided-clause res prop-name (=type res)) f)) resources)))
(define (change-sw-req ast prop-name comparator new-value . mode-names)
(let ([modes (if (null? mode-names) (=every-mode ast)
(filter (lambda (mode) (find (lambda (name) (string=? (->name mode) name)) mode-names))
(=every-mode ast)))]
[f (if (procedure? new-value) new-value (lambda _ new-value))])
(for-each (lambda (mode) (let ([clause (=search-req-clause mode prop-name)])
(when (not clause) (error change-sw-req "No clause found" prop-name (->name mode)))
(rewrite-terminal 'value clause f)
(rewrite-terminal 'comp clause comparator))) modes)))
(define (change-sw-prov ast prop-name new-value . mode-names)
(let ([modes (if (null? mode-names) (=every-mode ast)
(filter (lambda (mode) (find (lambda (name) (string=? (->name mode) name)) mode-names))
(=every-mode ast)))]
[f (if (procedure? new-value) new-value (lambda _ new-value))])
(for-each (lambda (mode) (rewrite-terminal 'value (=provided-clause mode prop-name) f)) modes)))
(define (remove-req-constraints ast) (for-each (lambda (req) (rewrite-delete req)) (->* (->Constraints (<=request ast)))))
(define (change-req-constraint ast name comparator new-value)
(debug (->* (->Constraints (<=request ast))))
(let ([clause (ast-find-child (lambda (i child) (string=? (->name (=real (->ReturnType child))) name))
(->Constraints (<=request ast)))])
(rewrite-terminal 'value clause (lambda _ new-value))
(rewrite-terminal 'comp clause comparator)))
(define (change-req-mp-value ast new-value) (rewrite-terminal 'value (car (->* (->MetaParameter* (<=request ast)))) new-value))
(define no-freq-hw-clauses (lambda _ (lambda (p) (if (string=? pn-freq p) #f (list make-prov comp-eq (lambda _ 0.5))))))
(define no-freq-sw-clauses (lambda _ (lambda (p comp-nr) (if (string=? pn-freq p) #f #t))))
(define (run-test id-string)
; (set!no-frequency) ; only use property load for system creation
(let ([id (string->number id-string)]
[between (lambda (lb val ub) (and (>= val lb) (<= val ub)))])
(cond
[(between 0 id 40) (two-modes id)]
[(between 100 id 130) (two-impls id)]
[(between 200 id 210) (two-comps id)]
[(between 300 id 310) (two-comps-reqc id)]
[(between 400 id 410) (two-resource-types id)]
[(between 500 id 510) (new-resources id)]
[(between 600 id 610) (new-software id)]
[(between 700 id 710) (tree-res id)]
[(between 900 id 920) (unsolvable id)]
[else (wrong-id run-test id)])))
(define (two-modes id)
(cond
((< id 30)
; General description: 2 modes, first mode is better
(let* ([ast (create-system 2 0 1 1 2 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-1-2")
(case id
[(1) ; Description: no further constraints
; Expected outcome: first mode (mode-1-1-1) is deployed on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(2) ; Description: mode-1-1-1 does not meet its requirements (max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-1-2")
(remove-req-constraints ast)]
[(3) ; Description: mode-1-1-1 does not meet its requirements (min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-2
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-1-2")
(remove-req-constraints ast)]
[(4) ; Description: mode-1-1-1 does not meet request constraint (max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.8)
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 3 "m-1-1-2")]
[(5) ; Description: mode-1-1-1 does not meet request constraint (min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.8)
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 3 "m-1-1-1") ; min-req not met
(change-sw-prov ast "p-1" 7 "m-1-1-2")]
[(6) ; Description: Reqs only met on res-1
; Expected outcome: first mode (mode-1-1-1) is deployed on res-1
(change-hw-prov ast "load" 0.9 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(7) ; Description: Reqs only met on res-2
; Expected outcome: first mode (mode-1-1-1) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(8) ; Description: Reqs only met on res-2, mode-1-1-1 does not meet its requirements at all (only max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met on both resources
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-1-2") ; max-req not met on res-1
(remove-req-constraints ast)]
[(9) ; Description: Reqs only met on res-2, mode-1-1-1 does not meet its requirements at all (min-eq and max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met on both resources
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-1-2") ; max-req not met on res-1
(remove-req-constraints ast)]
[(10) ; Description: Reqs only met on res-2, mode-1-1-1 does not meet its requirements at all (only min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-2")
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met on both resources
(change-sw-req ast "load" comp-min-eq 0.8 "m-1-1-2") ; min-req not met on res-1
(remove-req-constraints ast)]
[(11) ; Description: Reqs only met on res-2, mode-1-1-1 does not meet request constraint (only max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 3 "m-1-1-2")
(change-sw-req ast "load" comp-max-eq 0.8)] ; max-req not met on res-1
[(12) ; Description: Reqs only met on res-2, mode-1-1-2 does not meet request constraint (req:min-eq and res:max-eq)
; Expected outcome: first mode (mode-1-1-1) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1")
(change-sw-prov ast "p-1" 3 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8)] ; max-req not met on res-1
[(13) ; Description: Reqs only met on res-1, mode-1-1-1 does not meet request constraint (req:max-eq and res:min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on res-1
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 3 "m-1-1-2")
(change-sw-req ast "load" comp-min-eq 0.8)] ; max-req not met on res-2
[(14) ; Description: Reqs only met on res-1, mode-1-1-2 does not meet request constraint (only min-eq)
; Expected outcome: first mode (mode-1-1-1) is deployed on res-1
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1")
(change-sw-prov ast "p-1" 3 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-min-eq 0.8)] ; min-req not met on res-2
[(15) ; Description: Dynamic provision function, mp-value + 5. mp-value = 10. Required >= 14.
; Expected outcome: mode-1-1-1 is deployed
(change-req-constraint ast "p-1" comp-min-eq 14)
(change-req-mp-value ast 10)
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 5 (=value-of lomp mp-name))) "m-1-1-1")
(change-sw-prov ast "p-1" 20 "m-1-1-2")]
[(16) ; Description: Dynamic provision function, mp-value + 5. mp-value = 3. Required >= 14.
; Expected outcome: mode-1-1-2 is deployed
(change-req-constraint ast "p-1" comp-min-eq 14)
(change-req-mp-value ast 3)
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 5 (=value-of lomp mp-name))) "m-1-1-1")
(change-sw-prov ast "p-1" 20 "m-1-1-2")])
(save-ilp tmp-lp ast)))
(else
; General description: 2 impls with each 1 mode, first impl is better
(let ([ast (create-system 2 0 1 2 1 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-2-1")
(change-sw-req ast "load" comp-max-eq 0.8)
(case id
[(30) ; No further constraints
; Expected outcome: first mode (mode-1-1-1) is deployed on res-1 or res-2
(remove-req-constraints ast)]
[(31) ; mode-1-1-1 does not meet its requirements (max-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1")
(remove-req-constraints ast)]
[(32) ; mode-1-1-1 does not meet its requirements (min-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-1 or res-2
(change-sw-req ast "load" comp-min-eq 0.9 "m-1-1-1")
(remove-req-constraints ast)]
[(33) ; mode-1-1-1 does not meet request constraint (max-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-1 or res-2
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1")
(change-sw-prov ast "p-1" 3 "m-1-2-1")]
[(34) ; mode-1-1-1 does not meet request constraint (min-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-1 or res-2
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 3 "m-1-1-1")
(change-sw-prov ast "p-1" 7 "m-1-2-1")]
[(35) ; Reqs only met on res-2, mode-1-1-1 does not meet request constraint (max-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1")
(change-sw-prov ast "p-1" 3 "m-1-2-1")]
[(36) ; Reqs only met on res-2, mode-1-1-1 does not meet request constraint (min-eq)
; Expected outcome: second mode (mode-1-2-1) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 3 "m-1-1-1")
(change-sw-prov ast "p-1" 7 "m-1-2-1")]
[else (wrong-id two-modes id)])
(save-ilp tmp-lp ast)))))
(define (two-impls id)
; General description: 2 impls with each 2 modes, first modes are better, first impl is better
(let ([ast (create-system 3 0 1 2 2 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-2-1")
(change-sw-prov ast pn-energy (+ 25 (/ id 1e3)) "m-1-2-2")
(case id
[(100) ; Description: normal load constraints
; Expected outcome: mode-1-1-1 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(101) ; Description: mode-1-1-1 does not meet its requirements (max-eq)
; Expected outcome: mode-1-1-2 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(remove-req-constraints ast)]
[(102) ; Description: mode-1-1-1 and mode-1-1-2 do not meet their requirements (both max-eq)
; Expected outcome: mode-1-2-1 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-2") ; max-req not met
(remove-req-constraints ast)]
[(103) ; Description: mode-1-1-1 and mode-1-1-2 do not meet their requirements (min-eq and max-eq)
; Interesting: complete impl not meeting reqs
; Expected outcome: mode-1-2-1 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-2") ; min-req not met
(remove-req-constraints ast)]
[(104) ; Description: mode-1-1-1 and mode-1-1-2 do not meet their requirements (both min-eq)
; Interesting: one mode per impl not meeting reqs (only min reqs)
; Expected outcome: mode-1-2-1 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-2") ; min-req not met
(remove-req-constraints ast)]
[(105) ; Description: mode-1-1-1 and mode-1-2-1 do not meet their requirements (min-eq and max-eq)
; Interesting: one mode per impl not meeting reqs
; Expected outcome: mode-1-1-2 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-2-1") ; min-req not met
(remove-req-constraints ast)]
[(106) ; Description: only mode-1-2-2 meet its requirements (others mix of max-eq)
; Expected outcome: mode-1-2-2 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-2-1") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-2-2")
(remove-req-constraints ast)]
[(107) ; Description: only mode-1-2-2 meet its requirements (all min-eq)
; Expected outcome: mode-1-2-2 is deployed on res-1, res-2 or res-3
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-min-eq 0.7 "m-1-2-1") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-2-2")
(remove-req-constraints ast)]
[(108) ; Description: Reqs only met on res-2 and res-3 (max-eq)
; Expected outcome: mode-1-1-1 is deployed on either res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(109) ; Description: Reqs only met on res-2 and res-3 (min-eq)
; Expected outcome: mode-1-1-1 is deployed on either res-2 or res-3
(change-hw-prov ast "load" 0.7)
(change-hw-prov ast "load" 0.3 "r-1")
(change-sw-req ast "load" comp-min-eq 0.4)
(remove-req-constraints ast)]
[(110) ; Description: Reqs only met on res-2 (max-eq)
; Expected outcome: mode-1-1-1 is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1" "r-3")
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(111) ; Description: Reqs only met on res-2 (min-eq)
; Expected outcome: mode-1-1-1 is deployed on res-2
(change-hw-prov ast "load" 0.3)
(change-hw-prov ast "load" 0.7 "r-2")
(change-sw-req ast "load" comp-min-eq 0.4)
(remove-req-constraints ast)]
[(112) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 does not meet its requirements (max-eq)
; Expected outcome: mode-1-1-2 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(remove-req-constraints ast)]
[(113) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 and mode-1-1-2 do not meet their requirements (both max-eq)
; Expected outcome: mode-1-2-1 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-2") ; max-req not met
(remove-req-constraints ast)]
[(114) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 & mode-1-1-2 do not meet their requirements (min-eq and max-eq)
; Interesting: complete impl not meeting reqs
; Expected outcome: mode-1-2-1 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-2") ; min-req not met
(remove-req-constraints ast)]
[(115) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 and mode-1-1-2 do not meet their requirements (both min-eq)
; Interesting: one mode per impl not meeting reqs (only min reqs)
; Expected outcome: mode-1-2-1 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-2") ; min-req not met
(remove-req-constraints ast)]
[(116) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 and mode-1-2-1 do not meet their requirements (min-eq and max-eq)
; Interesting: one mode per impl not meeting reqs
; Expected outcome: mode-1-1-2 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-2-1") ; min-req not met
(remove-req-constraints ast)]
[(117) ; Description: Reqs only met on res-2 and res-3
; only mode-1-2-2 meet its requirements (others mix of max-eq)
; Expected outcome: mode-1-2-2 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-2-1") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-2-2")
(remove-req-constraints ast)]
[(118) ; Description: Reqs only met on res-2 and res-3
; only mode-1-2-2 meet its requirements (all min-eq)
; Expected outcome: mode-1-2-2 is deployed on res-2 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-2") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-2-1") ; min-req not met
(change-sw-req ast "load" comp-max-eq 0.8 "m-1-2-2")
(remove-req-constraints ast)]
[(119) ; Description: Reqs only met on res-1 and res-3 (max-eq),
; mode-1-1-1 and mode 1-2-1 do not meet request constraints (min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-3
(change-hw-prov ast "load" 0.4 "r-1")
(change-hw-prov ast "load" 0.9 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 7)
(change-sw-prov ast "p-1" 3 "m-1-1-1") ; min-req not met
(change-sw-prov ast "p-1" 2 "m-1-2-1")] ; min-req not met
[(120) ; Description: Reqs only met on res-1 and res-3 (min-eq),
; mode-1-1-1 and mode 1-2-1 do not meet request constraints (min-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.8 "r-3")
(change-sw-req ast "load" comp-min-eq 0.8)
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 7)
(change-sw-prov ast "p-1" 3 "m-1-1-1") ; min-req not met
(change-sw-prov ast "p-1" 2 "m-1-2-1")] ; min-req not met
[(121) ; Description: Reqs only met on res-1 and res-3 (max-eq),
; mode-1-1-1 and mode 1-2-1 do not meet request constraints (max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-3
(change-hw-prov ast "load" 0.4 "r-1")
(change-hw-prov ast "load" 0.9 "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 1)
(change-sw-prov ast "p-1" 8 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 7 "m-1-2-1")] ; max-req not met
[(122) ; Description: Reqs only met on res-1 and res-3 (min-eq),
; mode-1-1-1 and mode 1-2-1 do not meet request constraints (max-eq)
; Expected outcome: second mode (mode-1-1-2) is deployed on either res-1 or res-3
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.8 "r-3")
(change-sw-req ast "load" comp-min-eq 0.8)
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 1)
(change-sw-prov ast "p-1" 8 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 7 "m-1-2-1")] ; max-req not met
[(123) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 and mode-1-2-1 do not meet their requirements (max-eq)
; mode-1-1-1 and mode-1-1-2 do not meet request constraints (max-eq)
; Expected outcome: fourth mode (mode-1-2-2) is deployed on either res-1 or res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.8 "r-3")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-2-1") ; max-req not met
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 1)
(change-sw-prov ast "p-1" 8 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 7 "m-1-1-2")] ; max-req not met
[(124) ; Description: Reqs only met on res-2
; mode-1-1-1 and mode-1-2-1 do not meet their requirements (max-eq)
; mode-1-1-1 and mode-1-1-2 do not meet request constraints (max-eq)
; Expected outcome: fourth mode (mode-1-2-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.9 "r-3")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-1-1") ; max-req not met
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-2-1") ; max-req not met
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 1)
(change-sw-prov ast "p-1" 8 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 7 "m-1-1-2")] ; max-req not met
[(125) ; Description: Reqs only met on res-2 and res-3
; mode-1-1-1 and mode-1-2-1 do not meet their requirements (min-eq)
; mode-1-1-1 and mode-1-1-2 do not meet request constraints (min-eq)
; Expected outcome: fourth mode (mode-1-2-2) is deployed on either res-1 or res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.8 "r-3")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-2-1") ; min-req not met
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 4)
(change-sw-prov ast "p-1" 1 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 2 "m-1-1-2")] ; max-req not met
[(126) ; Description: Reqs only met on res-2
; mode-1-1-1 and mode-1-2-1 do not meet their requirements (min-eq)
; mode-1-1-1 and mode-1-1-2 do not meet request constraints (min-eq)
; Expected outcome: fourth mode (mode-1-2-2) is deployed on res-2
(change-hw-prov ast "load" 0.9 "r-1")
(change-hw-prov ast "load" 0.4 "r-2")
(change-hw-prov ast "load" 0.9 "r-3")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-1-1") ; min-req not met
(change-sw-req ast "load" comp-min-eq 1.0 "m-1-2-1") ; min-req not met
(change-req-constraint ast "p-1" comp-min-eq 4)
(change-sw-prov ast "p-1" 4)
(change-sw-prov ast "p-1" 1 "m-1-1-1") ; min-req not met
(change-sw-prov ast "p-1" 2 "m-1-1-2")] ; min-req not met
[(127 128 129)
; Description: Dynamic provision function, mp-value + 5|10|15|20.
(change-req-constraint ast "p-1" comp-min-eq 30)
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 5 (=value-of lomp mp-name))) "m-1-1-1")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 10 (=value-of lomp mp-name))) "m-1-1-2")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 15 (=value-of lomp mp-name))) "m-1-2-1")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 20 (=value-of lomp mp-name))) "m-1-2-2")
(case id
[(127) ; mp-value = 30. Required >= 30.
; Expected outcome: mode-1-1-1 is deployed
(change-req-mp-value ast 30)]
[(128) ; Description: Dynamic provision function, mp-value + 5|10|15|20. mp-value = 20. Required >= 30.
; Expected outcome: mode-1-1-2 is deployed
(change-req-mp-value ast 20)]
[(129) ; Description: Dynamic provision function, mp-value + 5|10|15|20. mp-value = 10. Required >= 30.
; Expected outcome: mode-1-2-2 is deployed
(change-req-mp-value ast 10)])]
[else (wrong-id two-impls id)])
(save-ilp tmp-lp ast)))
(define (two-comps id)
; General description: 2 comps with each 2 impls with each 2 modes, first comps, first impls and first modes are better
; All modes of comp-1 require prop-2 <= 20, where by default all modes provide sufficiently prop-2 = 10
(let ([ast (create-system 3 0 2 2 2 (list (lambda (impl) #t) no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-2-1")
(change-sw-prov ast pn-energy (+ 25 (/ id 1e3)) "m-1-2-2")
(change-sw-prov ast pn-energy 30 "m-2-1-1")
(change-sw-prov ast pn-energy 35 "m-2-1-2")
(change-sw-prov ast pn-energy 40 "m-2-2-1")
(change-sw-prov ast pn-energy 45 "m-2-2-2")
(change-sw-req ast "p-2" comp-max-eq 20 "m-1-1-1" "m-1-1-2" "m-1-2-1" "m-1-2-2")
(change-sw-prov ast "p-2" 10 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(case id
[(200) ; Description: normal load constraints
; Expected outcome: both, mode-1-1-1 and mode-2-1-1 are deployed on either res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(201) ; Description: only impl-2-2 meets requirement of comp-1
; Expected outcome: both, mode-1-1-1 and mode-2-2-1 are deployed on either res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)
(change-sw-prov ast "p-2" 40 "m-2-1-1" "m-2-1-2")] ; max-req not met
[(202) ; Description: mode-2-1-1 not meet hw-reqs (max-eq), mode-1-1-1 not meet request constraint (max-eq)
; mode-2-2-1 and mode-2-2-2 not meet comp-1 reqs (max-eq)
; Expected outcome: both, mode-1-1-2 and mode-2-1-2 are deployed on either res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-2-1-1")
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 4 "m-1-1-2" "m-1-2-1" "m-1-2-2")
(change-sw-prov ast "p-2" 40 "m-2-2-1" "m-2-2-2")] ; max-req not met
[(203) ; Description: mode-2-1-1 not meet hw-reqs (max-eq), mode-1-1-1 not meet request constraint (max-eq)
; mode-2-2-1 and mode-2-2-2 not meet comp-1 reqs (max-eq)
; Reqs only met at res-3 at all
; Expected outcome: both, mode-1-1-2 and mode-2-1-2 are deployed on res-3
(change-hw-prov ast "load" 1.0 "r-1" "r-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-2-1-1")
(change-req-constraint ast "p-1" comp-max-eq 4)
(change-sw-prov ast "p-1" 7 "m-1-1-1") ; max-req not met
(change-sw-prov ast "p-1" 4 "m-1-1-2" "m-1-2-1" "m-1-2-2")
(change-sw-prov ast "p-2" 40 "m-2-2-1" "m-2-2-2")] ; max-req not met
[(204) ; Description: mode-2-2-2 meet hw-reqs at res-1 (max-eq), mode-1-2-2 meet hw-req at res-2 (min-eq)
; mode-2-1-*, mode-2-2-1, mode-1-1-* and mode-1-2-1 not meeting reqs
; Reqs not met at res-3
; Expected outcome: mode-1-2-2 at res-2 and mode-2-2-2 on res-1
(change-hw-prov ast "load" 0.3 "r-1")
(change-hw-prov ast "load" 0.5 "r-3")
(change-hw-prov ast "load" 0.7 "r-2")
(change-sw-req ast "load" comp-max-eq 0.2)
(change-sw-req ast "load" comp-max-eq 0.4 "m-2-2-2")
(change-sw-req ast "load" comp-min-eq 0.6 "m-1-2-2")
(remove-req-constraints ast)]
[(205 206 207) ; Description: Dynamic provision function, mp-value +/- 5|10|15|20 for comp-1/comp-2.
; All modes of comp-1 require prop-2 <= 20. Request constrains prop-1 >= 30.
(change-req-constraint ast "p-1" comp-min-eq 30)
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 5 (=value-of lomp mp-name))) "m-1-1-1")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 10 (=value-of lomp mp-name))) "m-1-1-2")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 15 (=value-of lomp mp-name))) "m-1-2-1")
(change-sw-prov ast "p-1" (lambda (lomp target) (+ 20 (=value-of lomp mp-name))) "m-1-2-2")
(change-sw-prov ast "p-2" (lambda (lomp target) (- 60 (=value-of lomp mp-name))) "m-2-1-1")
(change-sw-prov ast "p-2" (lambda (lomp target) (- 45 (=value-of lomp mp-name))) "m-2-1-2")
(change-sw-prov ast "p-2" (lambda (lomp target) (max 1 (- 31 (=value-of lomp mp-name)))) "m-2-2-1")
(change-sw-prov ast "p-2" (lambda (lomp target) (max 1 (- 15 (=value-of lomp mp-name)))) "m-2-2-2")
(case id
[(205) ; mp-value = 10. Expected outcome: mode-1-2-2 and mode-2-2-2 are deployed
(change-req-mp-value ast 10)]
[(206) ; mp-value = 20. Expected outcome: mode-1-1-2 and mode-2-2-1 are deployed
(change-req-mp-value ast 20)]
[(207) ; mp-value = 30. Expected outcome: mode-1-1-1 and mode-2-1-2 are deployed
(change-req-mp-value ast 30)])]
[else (wrong-id two-comps id)])
(save-ilp tmp-lp ast)))
(define (two-comps-reqc id)
; General description: 2 comps with each 2 impls with each 2 modes, first comps, first impls and first modes are better
; Only the first impl of comp-1 require prop-2 <= 20, where by default all modes provide sufficiently prop-2 = 10
(let ([ast (create-system 3 0 2 2 2 (list (lambda (impl) (string=? impl "i-1-1"))
no-freq-sw-clauses no-freq-hw-clauses #f) )])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-2-1")
(change-sw-prov ast pn-energy (+ 25 (/ id 1e3)) "m-1-2-2")
(change-sw-prov ast pn-energy 30 "m-2-1-1")
(change-sw-prov ast pn-energy 35 "m-2-1-2")
(change-sw-prov ast pn-energy 40 "m-2-2-1")
(change-sw-prov ast pn-energy 45 "m-2-2-2")
(change-sw-req ast "p-2" comp-max-eq 20 "m-1-1-1" "m-1-1-2")
(change-sw-prov ast "p-2" 10 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(case id
[(300) ; Description: normal load constraints
; Expected outcome: only mode-1-2-1 is deployed on either res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)]
[(301) ; Description: modes of impl-1-2 do not meet their requirements
; Expected outcome: both, mode-1-1-1 and mode-2-1-1 are deployed on either res-1, res-2 or res-3
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-req ast "load" comp-max-eq 0.2 "m-1-2-1" "m-1-2-2") ; max-req not met
(remove-req-constraints ast)]
[else (wrong-id two-comps-reqc id)])
(save-ilp tmp-lp ast)))
(define (two-resource-types id)
; General description: 1 comp, 2 impls with 2 modes each. Two different resources types and, thus,
; dynamical value functions within modes (type-0:res-2 → max load 0.7, type-1:res-1,res-3 → max load 0.3)
; Normally only deployable on resource of type-0 (which is only res-2)
(let* ([hw-types (lambda (res-name) (if (or (string=? res-name "r-1") (string=? res-name "r-3")) (cons 1 #t) #f))]
[load-f (lambda (lomp target) (if (string=? (->name target) "type-1") 0.3 0.7))]
[sw-clauses (lambda _ (lambda (p comp-nr) (if (string=? pn-load p) (list make-req comp-max-eq load-f)
((no-freq-sw-clauses) p comp-nr))))]
[ast (create-system 3 0 1 2 2 (list #f sw-clauses no-freq-hw-clauses hw-types))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-prov ast pn-energy (+ 20 (/ id 1e3)) "m-1-2-1")
(change-sw-prov ast pn-energy (+ 25 (/ id 1e3)) "m-1-2-2")
(case id
[(400) ; No further constraints
; Expected outcome: mode-1-1-1 on res-2
(remove-req-constraints ast)]
[(401) ; Impl-1-1 does not meet request constraint
; Expected outcome: mode-1-2-1 on res-2
(change-sw-prov ast "p-1" 3 "m-1-1-1" "m-1-1-2")
(change-sw-prov ast "p-1" 7 "m-1-2-1" "m-1-2-2")
(change-req-constraint ast "p-1" comp-min-eq 5)]
[(402) ; Dynamic provision value for requested property, on type-1 it's 7, on type-0 it's 3
; Expected outcome: No solution, since provision only met on type-1, but all modes only deployable on type-0-resources
(change-sw-prov ast "p-1" (lambda (lomp target) (if (string=? (->name target) "type-1") 7 3)))
(change-req-constraint ast "p-1" comp-min-eq 5)]
[(403) ; Dynamic provision value for requested property only for first three modes
; Expected outcome: mode-1-2-2 on res-2
(change-sw-prov ast "p-1" (lambda (lomp target) (if (string=? (->name target) "type-1") 7 3))
"m-1-1-1" "m-1-1-2" "m-1-2-1")
(change-sw-prov ast "p-1" (lambda (lomp target) 7) "m-1-2-2")
(change-req-constraint ast "p-1" comp-min-eq 5)]
[(404) ; Low load of 0.2
; Expected outcome: mode-1-1-1 on any res
(change-hw-prov ast "load" 0.2)
(remove-req-constraints ast)]
[else (wrong-id two-resource-types id)])
(save-ilp tmp-lp ast)))
(define (new-resources id)
(define (add-resource name status prototype parent)
(let* ([cs (->* (->ProvClause* prototype))]
[new-cs (map (lambda (c) (:ProvClause mquat-spec (:PropertyRef mquat-spec (ast-child 'refname (->ReturnType c))) (->comparator c) (->value c))) cs)])
(rewrite-add (->SubResources parent) (:Resource mquat-spec name (ast-child 'typename prototype) status (list) new-cs))))
; General description: New resources entering the system, enabling new configurations
(let ([ast (create-system 2 0 1 1 2 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-req ast "load" comp-max-eq 0.8)
(remove-req-constraints ast)
(case id
[(500) ; No further constraints
; Expected outcome: mode-1-1-1 on either res-1 or res-2
#t]
[(501) ; High load
; Expected outcome: No solution
(change-hw-prov ast "load" 0.9)]
[(502) ; High load, but a fresh resource available
; Expected outcome: mode-1-1-1 on (new) res-3
(change-hw-prov ast "load" 0.9)
(save-ilp tmp-lp ast) ; just emporary
(add-resource "r-3" online (car (->* (->SubResources (->HWRoot ast)))) (->HWRoot ast))
(change-hw-prov ast "load" 0.5 "r-3")]
[(503) ; High load, new resource available, but still no viable solution
; Expected outcome: No solution
(change-hw-prov ast "load" 0.9)
(save-ilp tmp-lp ast) ; just emporary
(add-resource "r-3" online (car (->* (->SubResources (->HWRoot ast)))) (->HWRoot ast))
(change-hw-prov ast "load" 0.9 "r-3")]
[(504) ; High load, new offline resource added with no load
; Expected outcome: No solution (offline resource should not be used)
(change-hw-prov ast "load" 0.9)
(save-ilp tmp-lp ast) ; just emporary
(add-resource "r-3" offline (car (->* (->SubResources (->HWRoot ast)))) (->HWRoot ast))
(change-hw-prov ast "load" 0.0 "r-3")]
[else (wrong-id new-resources id)])
(save-ilp tmp-lp ast)))
(define (new-software id)
; General description: New software (comp,impl,mode) entering the system, enabling new configurations
(let* ([ast (create-system 2 0 1 1 2 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))]
[energy (ast-find-child (lambda (i child) (string=? (->name child) pn-energy)) (->RealProperty* (->SWRoot ast)))])
(define (add-comp comp-nr)
(debug "#create new comp" comp-nr)
(let ([new (:Comp mquat-spec (node-name "c" (list comp-nr)) (list) #f
(list (:RealProperty mquat-spec (node-name "p" (list comp-nr))
#f "runtime" 'increasing agg-sum)
(:PropertyRef mquat-spec energy)))])
(rewrite-add (->Comp* (->SWRoot ast)) new) new))
(define (find-create l prefix lon make-new)
(let ([name (node-name prefix lon)])
(or (ast-find-child (lambda (i child) (string=? (->name child) name)) l) (make-new))))
(define (find-create-comp comp-nr) (find-create (->Comp* (->SWRoot ast)) "c" (list comp-nr) (lambda _ (add-comp comp-nr))))
(define (add-impl comp-nr impl-nr reqcompnrs)
(debug "#create new impl" comp-nr impl-nr reqcompnrs)
(let ([new (:Impl mquat-spec (node-name "i" (list impl-nr comp-nr)) (list)
(map (lambda (nr) (->name (find-create-comp nr))) reqcompnrs) #f #f)])
(rewrite-add (->Impl* (find-create-comp comp-nr)) new) new))
(define (find-create-impl comp-nr impl-nr reqcompnrs) (find-create (->Impl* (find-create-comp comp-nr)) "i"
(list impl-nr comp-nr)
(lambda _ (add-impl comp-nr impl-nr reqcompnrs))))
(define (add-mode comp-nr impl-nr mode-nr req-comp-nr load-f energy-f prov-f prev-f)
(debug "#create new mode" comp-nr impl-nr mode-nr req-comp-nr)
(let* ([impl (find-create-impl comp-nr impl-nr (if req-comp-nr (list req-comp-nr) (list)))]
[find-prop-hw (lambda (name) (ast-find-child (lambda (i child) (string=? (->name (=real child)) name))
(->Property* (car (->* (->ResourceType* (->HWRoot ast)))))))]
; [find-prop-sw (lambda (name comp) (ast-find-child (lambda (i child) (string=? (->name (=real child)) name))
; (->Property* comp)))]
[load (find-prop-hw pn-load)]
; [energy (find-prop-sw pn-energy (find-create-comp comp-nr))]
; [prev-p (and req-comp-nr (find-prop-sw (node-name "p" (list req-comp-nr)) (find-create-comp req-comp-nr)))]
; [this-p (find-prop-sw (node-name "p" (list comp-nr)) (find-create-comp comp-nr))]
[clauses (filter (lambda (c) c) (list (:ReqClause mquat-spec (:PropertyRef mquat-spec pn-load) comp-max-eq load-f)
(:ProvClause mquat-spec (:PropertyRef mquat-spec pn-energy) comp-max-eq energy-f)
(:ProvClause mquat-spec (:PropertyRef mquat-spec (node-name "p" (list comp-nr))) comp-max-eq prov-f)
(and req-comp-nr (:ReqClause mquat-spec (:PropertyRef mquat-spec (node-name "p" (list req-comp-nr)))
comp-max-eq prev-f))))]
[new (:Mode mquat-spec (node-name "m" (list mode-nr impl-nr comp-nr)) clauses)])
(rewrite-add (->Mode* impl) new) new))
(define (prov-obj val id) (+ val (/ id 1e3)))
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(change-sw-req ast "load" comp-max-eq 0.2)
(case id
[(600) ; No further constraints
; Expected outcome: No solution
(remove-req-constraints ast)]
[(601) ; New mode of first impl requiring less
; Expected outcome: (new) mode-1-1-3 on either res-1 or res-2
(remove-req-constraints ast)
(save-ilp tmp-lp ast)
(add-mode 1 1 3 #f (lambda _ 0.8) (lambda _ (prov-obj 20 id)) (lambda _ 2) #f)]
[(602) ; New mode of a new second impl requiring less
; Expected outcome: (new) mode-1-2-1 on either res-1 or res-2
(remove-req-constraints ast)
(save-ilp tmp-lp ast)
(add-mode 1 2 1 #f (lambda _ 0.8) (lambda _ (prov-obj 20 id)) (lambda _ 2) #f)]
[(603) ; New component with one impl and one mode and using the existing comp
; Expected outcome: mode-1-1-1 and (new) mode-2-1-1, both on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-1" 4)
(remove-req-constraints ast)
(save-ilp tmp-lp ast)
(add-mode 2 1 1 1 (lambda _ 0.8) (lambda _ 20) (lambda _ 2) (lambda _ 7))
(rewrite-terminal 'target (<=request ast) (->name (find-create-comp 2)))]
[(604) ; New component with one impl and one mode and using the existing comp
; High load on res-1, high load required for comp-1-modes, low load required for new comp/mode
; Expected outcome: mode-1-1-1 on res-1 and (new) mode-2-1-1 on res-2
(change-sw-req ast "load" comp-min-eq 0.9)
(change-hw-prov ast "load" 0.91 "r-1")
(change-sw-prov ast "p-1" 4)
(remove-req-constraints ast)
(save-ilp tmp-lp ast)
(add-mode 2 1 1 1 (lambda _ 0.8) (lambda _ 20) (lambda _ 2) (lambda _ 7))
(rewrite-terminal 'target (<=request ast) (->name (find-create-comp 2)))]
[(605) ; New component using the existing comp, with one impl and one mode. Request still targets old component.
; Expected outcome: mode-1-1-1 on either res-1 or res-2
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-1" 4)
(remove-req-constraints ast)
(save-ilp tmp-lp ast)
(add-mode 2 1 1 1 (lambda _ 0.8) (lambda _ 20) (lambda _ 2) (lambda _ 7))]
[else (wrong-id new-software id)])
(save-ilp tmp-lp ast)))
(define (tree-res id)
; General description: Tree hardware structure with different hardware types on each level
; Top level has 3 PEs and type-0, second level has 9 PEs and type-1, third level has 18 PEs and type-2
(let* ([hw-types (lambda (res-name) (cons (/ (- (string-length res-name) 3) 2) #t))]
[name->type-nr (lambda (type-name) (string->number (substring type-name 5 (string-length type-name))))]
[load-f (lambda (lomp target) (case (name->type-nr (->name target)) [(0) 0.2] [(1) 0.4] [(2) 0.7]
[else (error "load-f" "wrong type" (->name target))]))]
[sw-clauses (lambda _ (lambda (p comp-nr) (if (string=? pn-load p) (list make-req comp-max-eq load-f)
((no-freq-sw-clauses) p comp-nr))))]
[ast (create-system 30 3 1 1 2 (list #f sw-clauses no-freq-hw-clauses hw-types))])
(change-sw-prov ast pn-energy (+ 10 (/ id 1e3)) "m-1-1-1")
(change-sw-prov ast pn-energy (+ 15 (/ id 1e3)) "m-1-1-2")
(case id
[(700) ; No further constraints
; Expected outcome: mode-1-1-1 on one of the 18 type-2 resources
(remove-req-constraints ast)]
[(701) ; Lower load (0.3)
; Expected outcome: mode-1-1-1 on either type-1 or type-2 resources
(change-hw-prov ast "load" 0.3)
(remove-req-constraints ast)]
[(702) ; Even lower load (0.1)
; Expected outcome: mode-1-1-1 on an arbitrary resource
(change-hw-prov ast "load" 0.1)
(remove-req-constraints ast)]
[else (wrong-id tree-res id)])
(save-ilp tmp-lp ast)))
(define (unsolvable id)
; General description: Systems without a solution, thus, no optimal solution
(case id
[(900) ; All hw-reqs not met (min-eq)
(let ([ast (create-system 3 0 1 1 2 (list #f no-freq-sw-clauses no-freq-hw-clauses #f))])
(change-hw-prov ast "load" 0.4)
(change-sw-req ast "load" comp-min-eq 0.7)
(remove-req-constraints ast)
(save-ilp tmp-lp ast))]
[(901) ; All hw-reqs not met (max-eq)
(let ([ast (create-system 3 0 1 1 2)])
(change-hw-prov ast "load" 0.8)
(change-sw-req ast "load" comp-max-eq 0.3)
(remove-req-constraints ast)
(save-ilp tmp-lp ast))]
[(902) ; Request constraint not met for any mode of the target component (min-eq)
(let ([ast (create-system 3 0 1 2 3)])
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-1" 2)
(change-req-constraint ast "p-1" comp-min-eq 15)
(save-ilp tmp-lp ast))]
[(903) ; Request constraint not met for any mode of the target component (max-eq)
(let ([ast (create-system 3 0 1 2 3)])
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-1" 7)
(change-req-constraint ast "p-1" comp-max-eq 4)
(save-ilp tmp-lp ast))]
[(904) ; Requirement on second component not met by any of its modes (max-eq)
(let ([ast (create-system 3 0 2 2 2 (list (lambda _ #t) #f #f #f))])
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-2" 7 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(change-sw-req ast "p-2" comp-max-eq 4 "m-1-1-1" "m-1-1-2" "m-1-2-1" "m-1-2-2")
(save-ilp tmp-lp ast))]
[(905) ; Requirement on second component not met by any of its modes (min-eq)
(let ([ast (create-system 3 0 2 2 2 (list (lambda _ #t) #f #f #f))])
(change-hw-prov ast "load" 0.8)
(change-sw-req ast "load" comp-max-eq 0.3)
(change-sw-prov ast "p-2" 2 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(change-sw-req ast "p-2" comp-min-eq 15 "m-1-1-1" "m-1-1-2" "m-1-2-1" "m-1-2-2")
(save-ilp tmp-lp ast))]
[(906) ; Requirement on third component not met by any of its modes (max-eq)
(let ([ast (create-system 3 0 3 2 2 (list (lambda _ #t) #f #f #f))])
(change-sw-req ast "load" comp-max-eq 0.8)
(change-sw-prov ast "p-3" 7 "m-3-1-1" "m-3-1-2" "m-3-2-1" "m-3-2-2")
(change-sw-req ast "p-3" comp-max-eq 4 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(save-ilp tmp-lp ast))]
[(907) ; Requirement on third component not met by any of its modes (min-eq)
(let ([ast (create-system 3 0 3 2 2 (list (lambda _ #t) #f #f #f))])
(change-hw-prov ast "load" 0.8)
(change-sw-req ast "load" comp-max-eq 0.3)
(change-sw-prov ast "p-3" 2 "m-3-1-1" "m-3-1-2" "m-3-2-1" "m-3-2-2")
(change-sw-req ast "p-3" comp-min-eq 15 "m-2-1-1" "m-2-1-2" "m-2-2-1" "m-2-2-2")
(save-ilp tmp-lp ast))]
[(908) ; Mutual exclusion of requirements in implementation of first component
(let* ([ast (create-system 3 0 2 2 1 (list (lambda _ #t) no-freq-sw-clauses #f #f))]
[comp2 (car (->* (->Comp* (->SWRoot ast))))]
[p2 (car (->* (->Property* comp2)))]
[new-p (:RealProperty mquat-spec "new-p-2" (->unit p2) (->kind p2) (->direction p2) (->agg p2))]
[req-cls (=every-req-clause p2 comp-max-eq)]
[prov-cls (=every-prov-clause p2 comp-eq)])
(change-sw-req ast "load" comp-max-eq 0.8)
(rewrite-add (->Property* comp2) new-p)
(info p2)
(info "reqs" req-cls (length req-cls))
(info "provs" prov-cls (length prov-cls))
(for-each (lambda (cl) (info "comp" (eq? comp-max-eq (->comparator cl)) "sub" (ast-subtype? cl 'ReqClause)
"prop" (eq? p2 (=real (->ReturnType cl))))) (=every-sw-clause ast))
; "clone" req-clauses cls in p1 and change new clauses to target new property
(for-each (lambda (cl) (rewrite-add (<- cl) (:ReqClause mquat-spec (:PropertyRef mquat-spec (->name new-p)) (->comparator cl) (->value cl)))) req-cls)
; "clone" prov-clauses in p2
(for-each (lambda (cl) (rewrite-add (<- cl) (:ProvClause mquat-spec (:PropertyRef mquat-spec (->name new-p)) (->comparator cl) (->value cl)))) prov-cls)
; adjust values, s.t. one impl fulfills req for first property only, second impl fulfills req for second property only
(change-sw-req ast "p-2" comp-max-eq 10 "m-1-1-1" "m-1-2-1")
(change-sw-req ast "new-p-2" comp-max-eq 10 "m-1-1-1" "m-1-2-1")
(change-sw-prov ast "p-2" 4 "m-2-1-1")
(change-sw-prov ast "p-2" 19 "m-2-2-1")
(change-sw-prov ast "new-p-2" 18 "m-2-1-1")
(change-sw-prov ast "new-p-2" 3 "m-2-2-1")
(save-ilp tmp-lp ast))]
[else (wrong-id unsolvable id)]))
(define (read-solution table fname)
(when (not (file-exists? fname)) (error "read-solution" "File not found." fname))
(with-input-from-file fname
(lambda ()
(for-each (lambda (entry) (hashtable-set! table (car entry) (cdr entry))) (read)))))
(define (check-test id-s obj fname)
(let* ([table (make-hashtable string-hash string=?)]
[var-value (lambda (name) (or (hashtable-ref table name #f) (error #f "Var not found" name)))]
[contains? (lambda (name) (hashtable-contains? table name))]
[id (string->number id-s)]
[test-obj (lambda (expected-base actual id) (let ([expected (+ expected-base (/ id 1e3))])
(if (not (= actual expected))
(error #f "Wrong objective value, expected first, given last"
expected actual))))]
[test-assert (lambda (msg expr) (if (not expr) (error #f msg)))])
(define (val=? base expected . lres)
(debug lres)
(let ([=name (lambda (base res-nr)
(if (number? res-nr) (string-append base "#r_" (number->string res-nr))
(fold-left (lambda (result nr) (string-append result "_" (number->string nr)))
(string-append base "#r") res-nr)))]
[op (if (= expected 0) for-all exists)])
(op (lambda (res-nr) (= (var-value (=name base res-nr)) expected)) (if (list? (car lres)) (car lres) lres))))
(define (val=1? base . lres) (val=? base 1 lres))
(define (val=0? base . lres) (val=? base 0 lres))
(define (mrl2 l1 l2) (fold-left (lambda (result e1) (append result (map (lambda (e2) (list e1 e2)) l2))) (list) l1))
(define (mrl3 l1 l2 l3)
(fold-left (lambda (result e1)
(append result (fold-left (lambda (inner e2) (append inner (map (lambda (e3) (list e1 e2 e3)) l3)))
(list) l2))) (list) l1))
(define (combine base . lon) (fold-left (lambda (result n) (string-append result "_" (number->string (if n n 1)))) base lon))
(define make-name
(case-lambda
[(c i) (string-append "b#" (combine "c" c) "#" (if i (combine "i" c i) ""))]
[(c i m) (string-append (make-name c i) "#" (if m (combine "m" c i m) ""))]))
(define make-msg
(case-lambda
[(name val) (string-append name (if (= 1 val) " not" "") " deployed")]
[(name val lres) (fold-left (lambda (result r) (string-append result (if (number? r) (number->string r) "…") ","))
(string-append (make-msg name val) " on ") lres)]))
(define-syntax check-mode
(syntax-rules (*)
[(_ val (c ... (* (* (r ...)))))
(check-mode val (c ... (#f (#f (r ...)))))]
[(_ val (c ... (* (m ... (r ...)))))
(check-mode val (c ... (#f (m ... (r ...)))))]
[(_ val (c ... (i ... (* (r ...)))))
(check-mode val (c ... (i ... (#f (r ...)))))]
[(_ val (c ... (i ... (m ... (r ...)))))
(for-each (lambda (ec)
(for-each (lambda (ei)
(for-each (lambda (em) (let ([name (make-name ec ei em)]
[lres (list r ...)])
(test-assert (make-msg name val lres) (val=? name val r ...))))
(list m ...)))
(list i ...)))
(list c ...))]))
(define-syntax check-impl
(syntax-rules (*)
[(_ val (c ... *))
(check-impl val (c ... (#f)))]
[(_ val (c ... (i ...)))
(for-each (lambda (ec)
(for-each (lambda (ei) (let ([name (make-name ec ei)])
(test-assert (make-msg name val) (= (var-value name) val))))
(list i ...)))
(list c ...))]))
(read-solution table fname)
(for-each (lambda (key) (debug key ":" (hashtable-ref table key #f))) (vector->list (hashtable-keys table)))
; impl deployment
(case id
[(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 500 502 601 605 700 701 702)
(check-impl 1 (1 *))]
[(30 100 101 105 108 109 110 111 112 116 119 120 121 122 127 128 400 404)
(check-impl 1 (1 (1)))
(check-impl 0 (1 (2)))]
[(31 32 33 34 35 36 102 103 104 106 107 113 114 115 117 118 123 124 125 126 129 401 403 602)
(check-impl 0 (1 (1)))
(check-impl 1 (1 (2)))]
[(200 202 203 207 301) (check-impl 1 (1 2 (1)))
(check-impl 0 (1 2 (2)))]
[(201 206) (check-impl 1 (1 (1)))
(check-impl 0 (1 (2)))
(check-impl 0 (2 (1)))
(check-impl 1 (2 (2)))]
[(204 205) (check-impl 1 (1 2 (2)))
(check-impl 0 (1 2 (1)))]
[(300) (check-impl 0 (1 (1)))
(check-impl 1 (1 (2)))
(check-impl 0 (2 (1 2)))]
[(402 902 903) (check-impl 0 (1 (1 2)))]
[(501 503 600 900 901) (check-impl 0 (1 *))]
[(603 604) (check-impl 1 (1 2 *))]
[(904 905 908) (check-impl 0 (1 2 (1 2)))]
[(906 907) (check-impl 0 (1 2 3 (1 2)))]
[else (error #f "Unknown test case id for impls" id)])
; mode-deployment
(case id
[(1 15 500) (check-mode 1 (1 (* (1 (1 2)))))
(check-mode 0 (1 (* (2 (1 2)))))]
[(2 3 4 5 16) (check-mode 0 (1 (* (1 (1 2)))))
(check-mode 1 (1 (* (2 (1 2)))))]
[(6 14) (check-mode 1 (1 (* (1 (1)))))
(check-mode 0 (1 (* (1 (2)))))
(check-mode 0 (1 (* (2 (1 2)))))]
[(7 12) (check-mode 1 (1 (* (1 (2)))))
(check-mode 0 (1 (* (1 (1)))))
(check-mode 0 (1 (* (2 (1 2)))))]
[(13) (check-mode 0 (1 (* (1 (1 2)))))
(check-mode 1 (1 (* (2 (1)))))
(check-mode 0 (1 (* (2 (2)))))]
[(8 9 10 11) (check-mode 0 (1 (* (1 (1 2)))))
(check-mode 1 (1 (* (2 (2)))))
(check-mode 0 (1 (* (2 (1)))))]
[(30) (check-mode 1 (1 (1 (* (1 2)))))
(check-mode 0 (1 (2 (* (1 2)))))]
[(31 32 33 34) (check-mode 0 (1 (1 (* (1 2)))))
(check-mode 1 (1 (2 (* (1 2)))))]
[(35 36) (check-mode 0 (1 (1 (* (1 2)))))
(check-mode 1 (1 (2 (* (2)))))
(check-mode 0 (1 (2 (* (1)))))]
[(100 127 404) (check-mode 1 (1 (1 (1 (1 2 3)))))
(check-mode 0 (1 (1 (2 (1 2 3)))))
(check-mode 0 (1 (2 (1 2 (1 2 3)))))]
[(101 105 128) (check-mode 0 (1 (1 (1 (1 2 3)))))