source: CIVL/mods/dev.civl.com/scripts/scale/v1.17_bench_dat/bench.scale.out@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 32.2 KB
Line 
1>>>>>>>> Adder <<<<<<<<
2CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
3
4=== Source files ===
5adder.cvl (../../examples/concurrency/adder.cvl)
6
7
8=== Command ===
9civl verify -inputB=2 ../..//examples/concurrency/adder.cvl
10
11=== Stats ===
12 time (s) : 1.02
13 memory (bytes) : 514850816
14 max process count : 3
15 states : 87
16 states saved : 80
17 state matches : 1
18 transitions : 85
19 trace steps : 52
20 valid calls : 72
21 provers : z3
22 prover calls : 2
23
24=== Result ===
25The standard properties hold for all executions.
26>>>>>>>> Adder <<<<<<<<
27CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
28
29=== Source files ===
30adder.cvl (../../examples/concurrency/adder.cvl)
31
32
33=== Command ===
34civl verify -inputB=3 ../..//examples/concurrency/adder.cvl
35
36=== Stats ===
37 time (s) : 0.32
38 memory (bytes) : 514850816
39 max process count : 4
40 states : 205
41 states saved : 194
42 state matches : 6
43 transitions : 207
44 trace steps : 136
45 valid calls : 165
46 provers : z3
47 prover calls : 5
48
49=== Result ===
50The standard properties hold for all executions.
51>>>>>>>> Adder <<<<<<<<
52CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
53
54=== Source files ===
55adder.cvl (../../examples/concurrency/adder.cvl)
56
57
58=== Command ===
59civl verify -inputB=4 ../..//examples/concurrency/adder.cvl
60
61=== Stats ===
62 time (s) : 0.38
63 memory (bytes) : 514850816
64 max process count : 5
65 states : 476
66 states saved : 450
67 state matches : 23
68 transitions : 494
69 trace steps : 337
70 valid calls : 373
71 provers : z3
72 prover calls : 8
73
74=== Result ===
75The standard properties hold for all executions.
76>>>>>>>> Adder <<<<<<<<
77CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
78
79=== Source files ===
80adder.cvl (../../examples/concurrency/adder.cvl)
81
82
83=== Command ===
84civl verify -inputB=5 ../..//examples/concurrency/adder.cvl
85
86=== Stats ===
87 time (s) : 0.42
88 memory (bytes) : 514850816
89 max process count : 6
90 states : 1100
91 states saved : 1028
92 state matches : 72
93 transitions : 1166
94 trace steps : 811
95 valid calls : 852
96 provers : z3
97 prover calls : 11
98
99=== Result ===
100The standard properties hold for all executions.
101>>>>>>>> Adder <<<<<<<<
102CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
103
104=== Source files ===
105adder.cvl (../../examples/concurrency/adder.cvl)
106
107
108=== Command ===
109civl verify -inputB=6 ../..//examples/concurrency/adder.cvl
110
111=== Stats ===
112 time (s) : 0.52
113 memory (bytes) : 514850816
114 max process count : 7
115 states : 2525
116 states saved : 2328
117 state matches : 201
118 transitions : 2719
119 trace steps : 1910
120 valid calls : 1954
121 provers : z3
122 prover calls : 14
123
124=== Result ===
125The standard properties hold for all executions.
126>>>>>>>> Adder <<<<<<<<
127CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
128
129=== Source files ===
130adder.cvl (../../examples/concurrency/adder.cvl)
131
132
133=== Command ===
134civl verify -inputB=7 ../..//examples/concurrency/adder.cvl
135
136=== Stats ===
137 time (s) : 0.63
138 memory (bytes) : 514850816
139 max process count : 8
140 states : 5743
141 states saved : 5230
142 state matches : 522
143 transitions : 6257
144 trace steps : 4418
145 valid calls : 4463
146 provers : z3
147 prover calls : 17
148
149=== Result ===
150The standard properties hold for all executions.
151>>>>>>>> Adder <<<<<<<<
152CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
153
154=== Source files ===
155adder.cvl (../../examples/concurrency/adder.cvl)
156
157
158=== Command ===
159civl verify -inputB=8 ../..//examples/concurrency/adder.cvl
160
161=== Stats ===
162 time (s) : 0.88
163 memory (bytes) : 514850816
164 max process count : 9
165 states : 12930
166 states saved : 11654
167 state matches : 1291
168 transitions : 14212
169 trace steps : 10063
170 valid calls : 10107
171 provers : z3
172 prover calls : 20
173
174=== Result ===
175The standard properties hold for all executions.
176>>>>>>>> Adder <<<<<<<<
177CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
178
179=== Source files ===
180adder.cvl (../../examples/concurrency/adder.cvl)
181
182
183=== Command ===
184civl verify -inputB=9 ../..//examples/concurrency/adder.cvl
185
186=== Stats ===
187 time (s) : 1.2
188 memory (bytes) : 640679936
189 max process count : 10
190 states : 28822
191 states saved : 25760
192 state matches : 3084
193 transitions : 31896
194 trace steps : 22621
195 valid calls : 22662
196 provers : z3
197 prover calls : 23
198
199=== Result ===
200The standard properties hold for all executions.
201>>>>>>>> Adder <<<<<<<<
202CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
203
204=== Source files ===
205adder.cvl (../../examples/concurrency/adder.cvl)
206
207
208=== Command ===
209civl verify -inputB=10 ../..//examples/concurrency/adder.cvl
210
211=== Stats ===
212 time (s) : 1.83
213 memory (bytes) : 906493952
214 max process count : 11
215 states : 63659
216 states saved : 56508
217 state matches : 7181
218 transitions : 70829
219 trace steps : 50284
220 valid calls : 50320
221 provers : z3
222 prover calls : 26
223
224=== Result ===
225The standard properties hold for all executions.
226>>>>>>>> Adder <<<<<<<<
227CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
228
229=== Source files ===
230adder.cvl (../../examples/concurrency/adder.cvl)
231
232
233=== Command ===
234civl verify -inputB=11 ../..//examples/concurrency/adder.cvl
235
236=== Stats ===
237 time (s) : 2.68
238 memory (bytes) : 1230503936
239 max process count : 12
240 states : 139457
241 states saved : 123098
242 state matches : 16398
243 transitions : 155843
244 trace steps : 110716
245 valid calls : 110745
246 provers : z3
247 prover calls : 29
248
249=== Result ===
250The standard properties hold for all executions.
251>>>>>>>> Adder <<<<<<<<
252CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
253
254=== Source files ===
255adder.cvl (../../examples/concurrency/adder.cvl)
256
257
258=== Command ===
259civl verify -inputB=12 ../..//examples/concurrency/adder.cvl
260
261=== Stats ===
262 time (s) : 4.75
263 memory (bytes) : 2570584064
264 max process count : 13
265 states : 303320
266 states saved : 266490
267 state matches : 36879
268 transitions : 340186
269 trace steps : 241805
270 valid calls : 241825
271 provers : z3
272 prover calls : 32
273
274=== Result ===
275The standard properties hold for all executions.
276>>>>>>>> Adder <<<<<<<<
277CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
278
279=== Source files ===
280adder.cvl (../../examples/concurrency/adder.cvl)
281
282
283=== Command ===
284civl verify -inputB=13 ../..//examples/concurrency/adder.cvl
285
286=== Stats ===
287 time (s) : 10.6
288 memory (bytes) : 3167223808
289 max process count : 14
290 states : 655600
291 states saved : 573724
292 state matches : 81936
293 transitions : 737522
294 trace steps : 524447
295 valid calls : 524456
296 provers : z3
297 prover calls : 35
298
299=== Result ===
300The standard properties hold for all executions.
301>>>>>>>> Adder <<<<<<<<
302CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
30316s: mem=3084Mb trans=1157560 traceSteps=823541 explored=1025058 saved=892569 prove=38
304
305=== Source files ===
306adder.cvl (../../examples/concurrency/adder.cvl)
307
308
309=== Command ===
310civl verify -inputB=14 ../..//examples/concurrency/adder.cvl
311
312=== Stats ===
313 time (s) : 23.1
314 memory (bytes) : 3778543616
315 max process count : 15
316 states : 1409289
317 states saved : 1229120
318 state matches : 180241
319 transitions : 1589515
320 trace steps : 1130674
321 valid calls : 1130670
322 provers : z3
323 prover calls : 38
324
325=== Result ===
326The standard properties hold for all executions.
327>>>>>>>> Barrier <<<<<<<<
328CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
329
330=== Source files ===
331barrier.cvl (../../examples/concurrency/barrier.cvl)
332
333
334=== Command ===
335civl verify -inputB=2 ../..//examples/concurrency/barrier.cvl
336
337=== Stats ===
338 time (s) : 1.04
339 memory (bytes) : 514850816
340 max process count : 3
341 states : 431
342 states saved : 171
343 state matches : 40
344 transitions : 466
345 trace steps : 138
346 valid calls : 454
347 provers : z3
348 prover calls : 2
349
350=== Result ===
351The standard properties hold for all executions.
352>>>>>>>> Barrier <<<<<<<<
353CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
354
355=== Source files ===
356barrier.cvl (../../examples/concurrency/barrier.cvl)
357
358
359=== Command ===
360civl verify -inputB=3 ../..//examples/concurrency/barrier.cvl
361
362=== Stats ===
363 time (s) : 0.37
364 memory (bytes) : 514850816
365 max process count : 4
366 states : 2067
367 states saved : 826
368 state matches : 376
369 transitions : 2436
370 trace steps : 788
371 valid calls : 2349
372 provers : z3
373 prover calls : 3
374
375=== Result ===
376The standard properties hold for all executions.
377>>>>>>>> Barrier <<<<<<<<
378CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
379
380=== Source files ===
381barrier.cvl (../../examples/concurrency/barrier.cvl)
382
383
384=== Command ===
385civl verify -inputB=4 ../..//examples/concurrency/barrier.cvl
386
387=== Stats ===
388 time (s) : 0.49
389 memory (bytes) : 514850816
390 max process count : 5
391 states : 9801
392 states saved : 3950
393 state matches : 2460
394 transitions : 12252
395 trace steps : 4166
396 valid calls : 11627
397 provers : z3
398 prover calls : 4
399
400=== Result ===
401The standard properties hold for all executions.
402>>>>>>>> Barrier <<<<<<<<
403CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
404
405=== Source files ===
406barrier.cvl (../../examples/concurrency/barrier.cvl)
407
408
409=== Command ===
410civl verify -inputB=5 ../..//examples/concurrency/barrier.cvl
411
412=== Stats ===
413 time (s) : 0.99
414 memory (bytes) : 649592832
415 max process count : 6
416 states : 46379
417 states saved : 18627
418 state matches : 13795
419 transitions : 60163
420 trace steps : 20895
421 valid calls : 56275
422 provers : z3
423 prover calls : 5
424
425=== Result ===
426The standard properties hold for all executions.
427>>>>>>>> Barrier <<<<<<<<
428CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
429
430=== Source files ===
431barrier.cvl (../../examples/concurrency/barrier.cvl)
432
433
434=== Command ===
435civl verify -inputB=6 ../..//examples/concurrency/barrier.cvl
436
437=== Stats ===
438 time (s) : 2.42
439 memory (bytes) : 1447559168
440 max process count : 7
441 states : 217063
442 states saved : 86345
443 state matches : 71264
444 transitions : 288314
445 trace steps : 100914
446 valid calls : 267294
447 provers : z3
448 prover calls : 6
449
450=== Result ===
451The standard properties hold for all executions.
452>>>>>>>> Barrier <<<<<<<<
453CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
454
455=== Source files ===
456barrier.cvl (../../examples/concurrency/barrier.cvl)
457
458
459=== Command ===
460civl verify -inputB=7 ../..//examples/concurrency/barrier.cvl
461
462=== Stats ===
463 time (s) : 10.0
464 memory (bytes) : 3128426496
465 max process count : 8
466 states : 1000367
467 states saved : 393748
468 state matches : 349994
469 transitions : 1350346
470 trace steps : 473878
471 valid calls : 1247627
472 provers : z3
473 prover calls : 7
474
475=== Result ===
476The standard properties hold for all executions.
477>>>>>>>> Barrier <<<<<<<<
478CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
47916s: mem=3105Mb trans=1980598 traceSteps=708732 explored=1481230 saved=581084 prove=8
48031s: mem=2997Mb trans=4015714 traceSteps=1447134 explored=2965598 saved=1190415 prove=8
48146s: mem=3342Mb trans=5643197 traceSteps=1981075 explored=4148064 saved=1604592 prove=8
482
483=== Source files ===
484barrier.cvl (../../examples/concurrency/barrier.cvl)
485
486
487=== Command ===
488civl verify -inputB=8 ../..//examples/concurrency/barrier.cvl
489
490=== Stats ===
491 time (s) : 48.67
492 memory (bytes) : 3508535296
493 max process count : 9
494 states : 4540601
495 states saved : 1770300
496 state matches : 1661020
497 transitions : 6201604
498 trace steps : 2178150
499 valid calls : 5734495
500 provers : z3
501 prover calls : 8
502
503=== Result ===
504The standard properties hold for all executions.
505>>>>>>>> Block adder <<<<<<<<
506CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
507
508=== Source files ===
509blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
510
511
512=== Command ===
513civl verify -inputB=4 -inputW=2 ../..//examples/concurrency/blockAdder.cvl
514
515=== Stats ===
516 time (s) : 1.24
517 memory (bytes) : 514850816
518 max process count : 3
519 states : 399
520 states saved : 190
521 state matches : 4
522 transitions : 402
523 trace steps : 125
524 valid calls : 706
525 provers : z3
526 prover calls : 11
527
528=== Result ===
529The standard properties hold for all executions.
530>>>>>>>> Block adder <<<<<<<<
531CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
532
533=== Source files ===
534blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
535
536
537=== Command ===
538civl verify -inputB=6 -inputW=3 ../..//examples/concurrency/blockAdder.cvl
539
540=== Stats ===
541 time (s) : 0.7
542 memory (bytes) : 514850816
543 max process count : 4
544 states : 1196
545 states saved : 644
546 state matches : 36
547 transitions : 1231
548 trace steps : 463
549 valid calls : 2965
550 provers : z3
551 prover calls : 20
552
553=== Result ===
554The standard properties hold for all executions.
555>>>>>>>> Block adder <<<<<<<<
556CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
557
558=== Source files ===
559blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
560
561
562=== Command ===
563civl verify -inputB=8 -inputW=4 ../..//examples/concurrency/blockAdder.cvl
564
565=== Stats ===
566 time (s) : 0.83
567 memory (bytes) : 514850816
568 max process count : 5
569 states : 3067
570 states saved : 1906
571 state matches : 184
572 transitions : 3250
573 trace steps : 1481
574 valid calls : 9950
575 provers : z3
576 prover calls : 29
577
578=== Result ===
579The standard properties hold for all executions.
580>>>>>>>> Block adder <<<<<<<<
581CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
582
583=== Source files ===
584blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
585
586
587=== Command ===
588civl verify -inputB=10 -inputW=5 ../..//examples/concurrency/blockAdder.cvl
589
590=== Stats ===
591 time (s) : 1.16
592 memory (bytes) : 514850816
593 max process count : 6
594 states : 7436
595 states saved : 5322
596 state matches : 720
597 transitions : 8155
598 trace steps : 4391
599 valid calls : 29713
600 provers : z3
601 prover calls : 38
602
603=== Result ===
604The standard properties hold for all executions.
605>>>>>>>> Block adder <<<<<<<<
606CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
607
608=== Source files ===
609blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
610
611
612=== Command ===
613civl verify -inputB=12 -inputW=6 ../..//examples/concurrency/blockAdder.cvl
614
615=== Stats ===
616 time (s) : 1.52
617 memory (bytes) : 514850816
618 max process count : 7
619 states : 17855
620 states saved : 14366
621 state matches : 2412
622 transitions : 20266
623 trace steps : 12373
624 valid calls : 82834
625 provers : z3
626 prover calls : 47
627
628=== Result ===
629The standard properties hold for all executions.
630>>>>>>>> Block adder <<<<<<<<
631CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
632
633=== Source files ===
634blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
635
636
637=== Command ===
638civl verify -inputB=14 -inputW=7 ../..//examples/concurrency/blockAdder.cvl
639
640=== Stats ===
641 time (s) : 2.15
642 memory (bytes) : 644349952
643 max process count : 8
644 states : 43124
645 states saved : 37760
646 state matches : 7308
647 transitions : 50431
648 trace steps : 33503
649 valid calls : 220757
650 provers : z3
651 prover calls : 56
652
653=== Result ===
654The standard properties hold for all executions.
655>>>>>>>> Block adder <<<<<<<<
656CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
657
658=== Source files ===
659blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
660
661
662=== Command ===
663civl verify -inputB=16 -inputW=8 ../..//examples/concurrency/blockAdder.cvl
664
665=== Stats ===
666 time (s) : 3.51
667 memory (bytes) : 1234173952
668 max process count : 9
669 states : 104715
670 states saved : 96898
671 state matches : 20656
672 transitions : 125370
673 trace steps : 87761
674 valid calls : 569502
675 provers : z3
676 prover calls : 65
677
678=== Result ===
679The standard properties hold for all executions.
680>>>>>>>> Block adder <<<<<<<<
681CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
682
683=== Source files ===
684blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
685
686
687=== Command ===
688civl verify -inputB=18 -inputW=9 ../..//examples/concurrency/blockAdder.cvl
689
690=== Stats ===
691 time (s) : 7.06
692 memory (bytes) : 2581594112
693 max process count : 10
694 states : 254180
695 states saved : 243254
696 state matches : 55512
697 transitions : 309691
698 trace steps : 223543
699 valid calls : 1432321
700 provers : z3
701 prover calls : 74
702
703=== Result ===
704The standard properties hold for all executions.
705>>>>>>>> Block adder <<<<<<<<
706CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
70716s: mem=3172Mb trans=667042 traceSteps=489570 explored=540517 saved=527024 prove=83
708
709=== Source files ===
710blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
711
712
713=== Command ===
714civl verify -inputB=20 -inputW=10 ../..//examples/concurrency/blockAdder.cvl
715
716=== Stats ===
717 time (s) : 16.53
718 memory (bytes) : 3326607360
719 max process count : 11
720 states : 613471
721 states saved : 598702
722 state matches : 143620
723 transitions : 757090
724 trace steps : 556061
725 valid calls : 3527778
726 provers : z3
727 prover calls : 83
728
729=== Result ===
730The standard properties hold for all executions.
731>>>>>>>> Block adder <<<<<<<<
732CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
73316s: mem=3105Mb trans=717215 traceSteps=530706 explored=575852 saved=566681 prove=92
73431s: mem=3355Mb trans=1518953 traceSteps=1125613 explored=1219439 saved=1202247 prove=92
735
736=== Source files ===
737blockAdder.cvl (../../examples/concurrency/blockAdder.cvl)
738
739
740=== Command ===
741civl verify -inputB=22 -inputW=11 ../..//examples/concurrency/blockAdder.cvl
742
743=== Stats ===
744 time (s) : 34.68
745 memory (bytes) : 3434610688
746 max process count : 12
747 states : 1467356
748 states saved : 1447932
749 state matches : 360756
750 transitions : 1828111
751 trace steps : 1355663
752 valid calls : 8536053
753 provers : z3
754 prover calls : 92
755
756=== Result ===
757The standard properties hold for all executions.
758>>>>>>>> Dining philosopher <<<<<<<<
759CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
760
761=== Source files ===
762dining.cvl (../../examples/concurrency/dining.cvl)
763
764
765=== Command ===
766civl verify -intOperationTransformer=false -inputBOUND=2 ../..//examples/concurrency/dining.cvl
767
768=== Stats ===
769 time (s) : 0.98
770 memory (bytes) : 514850816
771 max process count : 3
772 states : 42
773 states saved : 30
774 state matches : 4
775 transitions : 43
776 trace steps : 27
777 valid calls : 122
778 provers : z3
779 prover calls : 0
780
781=== Result ===
782The standard properties hold for all executions.
783>>>>>>>> Dining philosopher <<<<<<<<
784CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
785
786=== Source files ===
787dining.cvl (../../examples/concurrency/dining.cvl)
788
789
790=== Command ===
791civl verify -intOperationTransformer=false -inputBOUND=3 ../..//examples/concurrency/dining.cvl
792
793=== Stats ===
794 time (s) : 0.27
795 memory (bytes) : 514850816
796 max process count : 4
797 states : 147
798 states saved : 103
799 state matches : 40
800 transitions : 182
801 trace steps : 130
802 valid calls : 582
803 provers : z3
804 prover calls : 2
805
806=== Result ===
807The standard properties hold for all executions.
808>>>>>>>> Dining philosopher <<<<<<<<
809CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
810
811=== Source files ===
812dining.cvl (../../examples/concurrency/dining.cvl)
813
814
815=== Command ===
816civl verify -intOperationTransformer=false -inputBOUND=4 ../..//examples/concurrency/dining.cvl
817
818=== Stats ===
819 time (s) : 0.31
820 memory (bytes) : 514850816
821 max process count : 5
822 states : 459
823 states saved : 306
824 state matches : 193
825 transitions : 645
826 trace steps : 479
827 valid calls : 2189
828 provers : z3
829 prover calls : 3
830
831=== Result ===
832The standard properties hold for all executions.
833>>>>>>>> Dining philosopher <<<<<<<<
834CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
835
836=== Source files ===
837dining.cvl (../../examples/concurrency/dining.cvl)
838
839
840=== Command ===
841civl verify -intOperationTransformer=false -inputBOUND=5 ../..//examples/concurrency/dining.cvl
842
843=== Stats ===
844 time (s) : 0.36
845 memory (bytes) : 514850816
846 max process count : 6
847 states : 1588
848 states saved : 1013
849 state matches : 912
850 transitions : 2491
851 trace steps : 1897
852 valid calls : 8743
853 provers : z3
854 prover calls : 4
855
856=== Result ===
857The standard properties hold for all executions.
858>>>>>>>> Dining philosopher <<<<<<<<
859CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
860
861=== Source files ===
862dining.cvl (../../examples/concurrency/dining.cvl)
863
864
865=== Command ===
866civl verify -intOperationTransformer=false -inputBOUND=6 ../..//examples/concurrency/dining.cvl
867
868=== Stats ===
869 time (s) : 0.51
870 memory (bytes) : 514850816
871 max process count : 7
872 states : 5086
873 states saved : 3135
874 state matches : 3341
875 transitions : 8416
876 trace steps : 6439
877 valid calls : 30730
878 provers : z3
879 prover calls : 5
880
881=== Result ===
882The standard properties hold for all executions.
883>>>>>>>> Dining philosopher <<<<<<<<
884CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
885
886=== Source files ===
887dining.cvl (../../examples/concurrency/dining.cvl)
888
889
890=== Command ===
891civl verify -intOperationTransformer=false -inputBOUND=7 ../..//examples/concurrency/dining.cvl
892
893=== Stats ===
894 time (s) : 0.97
895 memory (bytes) : 649592832
896 max process count : 8
897 states : 17899
898 states saved : 10766
899 state matches : 13210
900 transitions : 31096
901 trace steps : 23929
902 valid calls : 116652
903 provers : z3
904 prover calls : 6
905
906=== Result ===
907The standard properties hold for all executions.
908>>>>>>>> Dining philosopher <<<<<<<<
909CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
910
911=== Source files ===
912dining.cvl (../../examples/concurrency/dining.cvl)
913
914
915=== Command ===
916civl verify -intOperationTransformer=false -inputBOUND=8 ../..//examples/concurrency/dining.cvl
917
918=== Stats ===
919 time (s) : 2.22
920 memory (bytes) : 1445986304
921 max process count : 9
922 states : 56897
923 states saved : 33556
924 state matches : 44322
925 transitions : 101204
926 trace steps : 77820
927 valid calls : 394567
928 provers : z3
929 prover calls : 7
930
931=== Result ===
932The standard properties hold for all executions.
933>>>>>>>> Dining philosopher <<<<<<<<
934CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
935
936=== Source files ===
937dining.cvl (../../examples/concurrency/dining.cvl)
938
939
940=== Command ===
941civl verify -intOperationTransformer=false -inputBOUND=9 ../..//examples/concurrency/dining.cvl
942
943=== Stats ===
944 time (s) : 7.21
945 memory (bytes) : 3125805056
946 max process count : 10
947 states : 198388
948 states saved : 115248
949 state matches : 164564
950 transitions : 362935
951 trace steps : 279742
952 valid calls : 1454138
953 provers : z3
954 prover calls : 8
955
956=== Result ===
957The standard properties hold for all executions.
958>>>>>>>> Dining philosopher <<<<<<<<
959CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
96016s: mem=3043Mb trans=770468 traceSteps=584772 explored=462383 saved=276751 prove=9
961
962=== Source files ===
963dining.cvl (../../examples/concurrency/dining.cvl)
964
965
966=== Command ===
967civl verify -intOperationTransformer=false -inputBOUND=10 ../..//examples/concurrency/dining.cvl
968
969=== Stats ===
970 time (s) : 20.3
971 memory (bytes) : 2910322688
972 max process count : 11
973 states : 619996
974 states saved : 355589
975 state matches : 528608
976 transitions : 1148585
977 trace steps : 884114
978 valid calls : 4776319
979 provers : z3
980 prover calls : 9
981
982=== Result ===
983The standard properties hold for all executions.
984>>>>>>>> Dining philosopher <<<<<<<<
985CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
98616s: mem=3034Mb trans=730922 traceSteps=554462 explored=443887 saved=267491 prove=10
98731s: mem=3025Mb trans=1413485 traceSteps=1092316 explored=826520 saved=505427 prove=10
98846s: mem=3338Mb trans=1992662 traceSteps=1520882 explored=1215388 saved=743685 prove=10
98961s: mem=3324Mb trans=2864907 traceSteps=2178687 explored=1660317 saved=974173 prove=10
99076s: mem=3259Mb trans=3791764 traceSteps=2903291 explored=2064834 saved=1176437 prove=10
991
992=== Source files ===
993dining.cvl (../../examples/concurrency/dining.cvl)
994
995
996=== Command ===
997civl verify -intOperationTransformer=false -inputBOUND=11 ../..//examples/concurrency/dining.cvl
998
999=== Stats ===
1000 time (s) : 78.06
1001 memory (bytes) : 3407347712
1002 max process count : 12
1003 states : 2130737
1004 states saved : 1209388
1005 state matches : 1890539
1006 transitions : 4021255
1007 trace steps : 3099830
1008 valid calls : 17169687
1009 provers : z3
1010 prover calls : 10
1011
1012=== Result ===
1013The standard properties hold for all executions.
1014>>>>>>>> Diffusion2d <<<<<<<<
1015CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1016
1017=== Source files ===
1018diffusion2d.c (../../examples/mpi/diffusion2d.c)
1019
1020
1021=== Command ===
1022civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=1 -inputNPROCSXB=1 -inputNPROCSYB=1 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1023
1024=== Stats ===
1025 time (s) : 4.09
1026 memory (bytes) : 919076864
1027 max process count : 2
1028 states : 1140
1029 states saved : 775
1030 state matches : 0
1031 transitions : 1138
1032 trace steps : 538
1033 valid calls : 2868
1034 provers : z3
1035 prover calls : 4
1036
1037=== Result ===
1038The standard properties hold for all executions.
1039>>>>>>>> Diffusion2d <<<<<<<<
1040CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1041
1042=== Source files ===
1043diffusion2d.c (../../examples/mpi/diffusion2d.c)
1044
1045
1046=== Command ===
1047civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=2 -inputNPROCSXB=1 -inputNPROCSYB=2 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1048
1049=== Stats ===
1050 time (s) : 2.49
1051 memory (bytes) : 919076864
1052 max process count : 2
1053 states : 2284
1054 states saved : 1629
1055 state matches : 0
1056 transitions : 2282
1057 trace steps : 1141
1058 valid calls : 6457
1059 provers : z3
1060 prover calls : 8
1061
1062=== Result ===
1063The standard properties hold for all executions.
1064>>>>>>>> Diffusion2d <<<<<<<<
1065CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1066
1067=== Source files ===
1068diffusion2d.c (../../examples/mpi/diffusion2d.c)
1069
1070
1071=== Command ===
1072civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=3 -inputNPROCSXB=1 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1073
1074=== Stats ===
1075 time (s) : 2.54
1076 memory (bytes) : 1514668032
1077 max process count : 2
1078 states : 3605
1079 states saved : 2619
1080 state matches : 0
1081 transitions : 3603
1082 trace steps : 1849
1083 valid calls : 10909
1084 provers : z3
1085 prover calls : 11
1086
1087=== Result ===
1088The standard properties hold for all executions.
1089>>>>>>>> Diffusion2d <<<<<<<<
1090CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1091
1092=== Source files ===
1093diffusion2d.c (../../examples/mpi/diffusion2d.c)
1094
1095
1096=== Command ===
1097civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=2 -inputNPROCSXB=2 -inputNPROCSYB=2 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1098
1099=== Stats ===
1100 time (s) : 4.74
1101 memory (bytes) : 2536505344
1102 max process count : 3
1103 states : 14327
1104 states saved : 9800
1105 state matches : 0
1106 transitions : 14324
1107 trace steps : 6713
1108 valid calls : 46448
1109 provers : z3
1110 prover calls : 18
1111
1112=== Result ===
1113The standard properties hold for all executions.
1114>>>>>>>> Diffusion2d <<<<<<<<
1115CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1116
1117=== Source files ===
1118diffusion2d.c (../../examples/mpi/diffusion2d.c)
1119
1120
1121=== Command ===
1122civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=3 -inputNPROCSXB=2 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1123
1124=== Stats ===
1125 time (s) : 5.69
1126 memory (bytes) : 2545942528
1127 max process count : 3
1128 states : 23516
1129 states saved : 16107
1130 state matches : 0
1131 transitions : 23513
1132 trace steps : 11085
1133 valid calls : 78933
1134 provers : z3
1135 prover calls : 21
1136
1137=== Result ===
1138The standard properties hold for all executions.
1139>>>>>>>> Diffusion2d <<<<<<<<
1140CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
1141
1142=== Source files ===
1143diffusion2d.c (../../examples/mpi/diffusion2d.c)
1144
1145
1146=== Command ===
1147civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=3 -inputNPROCSXB=3 -inputNPROCSYB=3 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1148
1149=== Stats ===
1150 time (s) : 14.92
1151 memory (bytes) : 2967470080
1152 max process count : 4
1153 states : 76154
1154 states saved : 50193
1155 state matches : 0
1156 transitions : 76150
1157 trace steps : 34139
1158 valid calls : 281960
1159 provers : z3
1160 prover calls : 35
1161
1162=== Result ===
1163The standard properties hold for all executions.
1164>>>>>>>> Diffusion2d <<<<<<<<
1165CIVL v1.17 of 2018-07-18 -- http://vsl.cis.udel.edu/civl
116617s: mem=3034Mb trans=86601 traceSteps=39473 explored=86605 saved=57453 prove=38
1167
1168=== Source files ===
1169diffusion2d.c (../../examples/mpi/diffusion2d.c)
1170
1171
1172=== Command ===
1173civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=4 -inputNPROCSXB=3 -inputNPROCSYB=4 -enablePrintf=false ../..//examples/mpi/diffusion2d.c
1174
1175=== Stats ===
1176 time (s) : 21.01
1177 memory (bytes) : 3183476736
1178 max process count : 4
1179 states : 111347
1180 states saved : 73235
1181 state matches : 0
1182 transitions : 111343
1183 trace steps : 49956
1184 valid calls : 419906
1185 provers : z3
1186 prover calls : 38
1187
1188=== Result ===
1189The standard properties hold for all executions.
Note: See TracBrowser for help on using the repository browser.