source: CIVL/mods/dev.civl.com/scripts/scale/v1.11.1_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: 30.9 KB
Line 
1>>>>>>>> Adder <<<<<<<<
2CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
3
4=== Command ===
5civl verify -inputB=2 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
6
7=== Stats ===
8 time (s) : 1.01
9 memory (bytes) : 514850816
10 max process count : 3
11 states : 87
12 states saved : 80
13 state matches : 1
14 transitions : 85
15 trace steps : 52
16 valid calls : 71
17 provers : z3, cvc4, cvc3
18 prover calls : 2
19
20=== Result ===
21The standard properties hold for all executions.
22>>>>>>>> Adder <<<<<<<<
23CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
24
25=== Command ===
26civl verify -inputB=3 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
27
28=== Stats ===
29 time (s) : 0.28
30 memory (bytes) : 514850816
31 max process count : 4
32 states : 205
33 states saved : 194
34 state matches : 6
35 transitions : 207
36 trace steps : 136
37 valid calls : 167
38 provers : z3, cvc4, cvc3
39 prover calls : 5
40
41=== Result ===
42The standard properties hold for all executions.
43>>>>>>>> Adder <<<<<<<<
44CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
45
46=== Command ===
47civl verify -inputB=4 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
48
49=== Stats ===
50 time (s) : 0.38
51 memory (bytes) : 514850816
52 max process count : 5
53 states : 476
54 states saved : 450
55 state matches : 23
56 transitions : 494
57 trace steps : 337
58 valid calls : 381
59 provers : z3, cvc4, cvc3
60 prover calls : 8
61
62=== Result ===
63The standard properties hold for all executions.
64>>>>>>>> Adder <<<<<<<<
65CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
66
67=== Command ===
68civl verify -inputB=5 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
69
70=== Stats ===
71 time (s) : 0.37
72 memory (bytes) : 514850816
73 max process count : 6
74 states : 1100
75 states saved : 1028
76 state matches : 72
77 transitions : 1166
78 trace steps : 811
79 valid calls : 865
80 provers : z3, cvc4, cvc3
81 prover calls : 11
82
83=== Result ===
84The standard properties hold for all executions.
85>>>>>>>> Adder <<<<<<<<
86CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
87
88=== Command ===
89civl verify -inputB=6 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
90
91=== Stats ===
92 time (s) : 0.48
93 memory (bytes) : 514850816
94 max process count : 7
95 states : 2525
96 states saved : 2328
97 state matches : 201
98 transitions : 2719
99 trace steps : 1910
100 valid calls : 1955
101 provers : z3, cvc4, cvc3
102 prover calls : 14
103
104=== Result ===
105The standard properties hold for all executions.
106>>>>>>>> Adder <<<<<<<<
107CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
108
109=== Command ===
110civl verify -inputB=7 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
111
112=== Stats ===
113 time (s) : 0.57
114 memory (bytes) : 514850816
115 max process count : 8
116 states : 5743
117 states saved : 5230
118 state matches : 522
119 transitions : 6257
120 trace steps : 4418
121 valid calls : 4387
122 provers : z3, cvc4, cvc3
123 prover calls : 17
124
125=== Result ===
126The standard properties hold for all executions.
127>>>>>>>> Adder <<<<<<<<
128CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
129
130=== Command ===
131civl verify -inputB=8 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
132
133=== Stats ===
134 time (s) : 0.72
135 memory (bytes) : 514850816
136 max process count : 9
137 states : 12930
138 states saved : 11654
139 state matches : 1291
140 transitions : 14212
141 trace steps : 10063
142 valid calls : 9761
143 provers : z3, cvc4, cvc3
144 prover calls : 20
145
146=== Result ===
147The standard properties hold for all executions.
148>>>>>>>> Adder <<<<<<<<
149CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
150
151=== Command ===
152civl verify -inputB=9 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
153
154=== Stats ===
155 time (s) : 1.05
156 memory (bytes) : 639107072
157 max process count : 10
158 states : 28822
159 states saved : 25760
160 state matches : 3084
161 transitions : 31896
162 trace steps : 22621
163 valid calls : 21533
164 provers : z3, cvc4, cvc3
165 prover calls : 23
166
167=== Result ===
168The standard properties hold for all executions.
169>>>>>>>> Adder <<<<<<<<
170CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
171
172=== Command ===
173civl verify -inputB=10 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
174
175=== Stats ===
176 time (s) : 1.43
177 memory (bytes) : 904921088
178 max process count : 11
179 states : 63659
180 states saved : 56508
181 state matches : 7181
182 transitions : 70829
183 trace steps : 50284
184 valid calls : 47127
185 provers : z3, cvc4, cvc3
186 prover calls : 26
187
188=== Result ===
189The standard properties hold for all executions.
190>>>>>>>> Adder <<<<<<<<
191CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
192
193=== Command ===
194civl verify -inputB=11 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
195
196=== Stats ===
197 time (s) : 2.43
198 memory (bytes) : 1218969600
199 max process count : 12
200 states : 139457
201 states saved : 123098
202 state matches : 16398
203 transitions : 155843
204 trace steps : 110716
205 valid calls : 102415
206 provers : z3, cvc4, cvc3
207 prover calls : 29
208
209=== Result ===
210The standard properties hold for all executions.
211>>>>>>>> Adder <<<<<<<<
212CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
213
214=== Command ===
215civl verify -inputB=12 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
216
217=== Stats ===
218 time (s) : 4.32
219 memory (bytes) : 1725431808
220 max process count : 13
221 states : 303320
222 states saved : 266490
223 state matches : 36879
224 transitions : 340186
225 trace steps : 241805
226 valid calls : 221189
227 provers : z3, cvc4, cvc3
228 prover calls : 32
229
230=== Result ===
231The standard properties hold for all executions.
232>>>>>>>> Adder <<<<<<<<
233CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
234
235=== Command ===
236civl verify -inputB=13 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
237
238=== Stats ===
239 time (s) : 10.25
240 memory (bytes) : 3327655936
241 max process count : 14
242 states : 655600
243 states saved : 573724
244 state matches : 81936
245 transitions : 737522
246 trace steps : 524447
247 valid calls : 475129
248 provers : z3, cvc4, cvc3
249 prover calls : 35
250
251=== Result ===
252The standard properties hold for all executions.
253>>>>>>>> Adder <<<<<<<<
254CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
25516s: mem=3242Mb trans=1235281 traceSteps=878859 explored=1093643 saved=952019 prove=38
256
257=== Command ===
258civl verify -inputB=14 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/adder.cvl
259
260=== Stats ===
261 time (s) : 18.74
262 memory (bytes) : 3397910528
263 max process count : 15
264 states : 1409289
265 states saved : 1229120
266 state matches : 180241
267 transitions : 1589515
268 trace steps : 1130674
269 valid calls : 1015787
270 provers : z3, cvc4, cvc3
271 prover calls : 38
272
273=== Result ===
274The standard properties hold for all executions.
275>>>>>>>> Barrier <<<<<<<<
276CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
277
278=== Command ===
279civl verify -inputB=2 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
280
281=== Stats ===
282 time (s) : 1.0
283 memory (bytes) : 514850816
284 max process count : 3
285 states : 431
286 states saved : 171
287 state matches : 40
288 transitions : 466
289 trace steps : 138
290 valid calls : 599
291 provers : z3, cvc4, cvc3
292 prover calls : 2
293
294=== Result ===
295The standard properties hold for all executions.
296>>>>>>>> Barrier <<<<<<<<
297CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
298
299=== Command ===
300civl verify -inputB=3 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
301
302=== Stats ===
303 time (s) : 0.33
304 memory (bytes) : 514850816
305 max process count : 4
306 states : 2067
307 states saved : 826
308 state matches : 376
309 transitions : 2436
310 trace steps : 788
311 valid calls : 3341
312 provers : z3, cvc4, cvc3
313 prover calls : 3
314
315=== Result ===
316The standard properties hold for all executions.
317>>>>>>>> Barrier <<<<<<<<
318CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
319
320=== Command ===
321civl verify -inputB=4 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
322
323=== Stats ===
324 time (s) : 0.42
325 memory (bytes) : 514850816
326 max process count : 5
327 states : 9801
328 states saved : 3950
329 state matches : 2460
330 transitions : 12252
331 trace steps : 4166
332 valid calls : 16981
333 provers : z3, cvc4, cvc3
334 prover calls : 4
335
336=== Result ===
337The standard properties hold for all executions.
338>>>>>>>> Barrier <<<<<<<<
339CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
340
341=== Command ===
342civl verify -inputB=5 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
343
344=== Stats ===
345 time (s) : 0.93
346 memory (bytes) : 649592832
347 max process count : 6
348 states : 46379
349 states saved : 18627
350 state matches : 13795
351 transitions : 60163
352 trace steps : 20895
353 valid calls : 82763
354 provers : z3, cvc4, cvc3
355 prover calls : 5
356
357=== Result ===
358The standard properties hold for all executions.
359>>>>>>>> Barrier <<<<<<<<
360CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
361
362=== Command ===
363civl verify -inputB=6 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
364
365=== Stats ===
366 time (s) : 2.21
367 memory (bytes) : 1446510592
368 max process count : 7
369 states : 217063
370 states saved : 86345
371 state matches : 71264
372 transitions : 288314
373 trace steps : 100914
374 valid calls : 393523
375 provers : z3, cvc4, cvc3
376 prover calls : 6
377
378=== Result ===
379The standard properties hold for all executions.
380>>>>>>>> Barrier <<<<<<<<
381CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
382
383=== Command ===
384civl verify -inputB=7 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
385
386=== Stats ===
387 time (s) : 8.85
388 memory (bytes) : 3116892160
389 max process count : 8
390 states : 1000367
391 states saved : 393748
392 state matches : 349994
393 transitions : 1350346
394 trace steps : 473878
395 valid calls : 1837145
396 provers : z3, cvc4, cvc3
397 prover calls : 7
398
399=== Result ===
400The standard properties hold for all executions.
401>>>>>>>> Barrier <<<<<<<<
402CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
40316s: mem=3020Mb trans=2119287 traceSteps=763138 explored=1584821 saved=626869 prove=8
40431s: mem=3357Mb trans=3962885 traceSteps=1429265 explored=2927359 saved=1175784 prove=8
405
406=== Command ===
407civl verify -inputB=8 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/barrier.cvl
408
409=== Stats ===
410 time (s) : 43.59
411 memory (bytes) : 3284664320
412 max process count : 9
413 states : 4540601
414 states saved : 1770300
415 state matches : 1661020
416 transitions : 6201604
417 trace steps : 2178150
418 valid calls : 8450321
419 provers : z3, cvc4, cvc3
420 prover calls : 8
421
422=== Result ===
423The standard properties hold for all executions.
424>>>>>>>> Block adder <<<<<<<<
425CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
426
427=== Command ===
428civl verify -inputB=4 -inputW=2 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
429
430=== Stats ===
431 time (s) : 1.16
432 memory (bytes) : 514850816
433 max process count : 3
434 states : 399
435 states saved : 190
436 state matches : 4
437 transitions : 402
438 trace steps : 125
439 valid calls : 671
440 provers : z3, cvc4, cvc3
441 prover calls : 11
442
443=== Result ===
444The standard properties hold for all executions.
445>>>>>>>> Block adder <<<<<<<<
446CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
447
448=== Command ===
449civl verify -inputB=6 -inputW=3 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
450
451=== Stats ===
452 time (s) : 0.61
453 memory (bytes) : 514850816
454 max process count : 4
455 states : 1196
456 states saved : 644
457 state matches : 36
458 transitions : 1231
459 trace steps : 463
460 valid calls : 2753
461 provers : z3, cvc4, cvc3
462 prover calls : 20
463
464=== Result ===
465The standard properties hold for all executions.
466>>>>>>>> Block adder <<<<<<<<
467CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
468
469=== Command ===
470civl verify -inputB=8 -inputW=4 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
471
472=== Stats ===
473 time (s) : 0.71
474 memory (bytes) : 514850816
475 max process count : 5
476 states : 3067
477 states saved : 1906
478 state matches : 184
479 transitions : 3250
480 trace steps : 1481
481 valid calls : 9103
482 provers : z3, cvc4, cvc3
483 prover calls : 29
484
485=== Result ===
486The standard properties hold for all executions.
487>>>>>>>> Block adder <<<<<<<<
488CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
489
490=== Command ===
491civl verify -inputB=10 -inputW=5 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
492
493=== Stats ===
494 time (s) : 0.95
495 memory (bytes) : 514850816
496 max process count : 6
497 states : 7436
498 states saved : 5322
499 state matches : 720
500 transitions : 8155
501 trace steps : 4391
502 valid calls : 26929
503 provers : z3, cvc4, cvc3
504 prover calls : 38
505
506=== Result ===
507The standard properties hold for all executions.
508>>>>>>>> Block adder <<<<<<<<
509CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
510
511=== Command ===
512civl verify -inputB=12 -inputW=6 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
513
514=== Stats ===
515 time (s) : 1.47
516 memory (bytes) : 514850816
517 max process count : 7
518 states : 17855
519 states saved : 14366
520 state matches : 2412
521 transitions : 20266
522 trace steps : 12373
523 valid calls : 74639
524 provers : z3, cvc4, cvc3
525 prover calls : 47
526
527=== Result ===
528The standard properties hold for all executions.
529>>>>>>>> Block adder <<<<<<<<
530CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
531
532=== Command ===
533civl verify -inputB=14 -inputW=7 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
534
535=== Stats ===
536 time (s) : 2.07
537 memory (bytes) : 641728512
538 max process count : 8
539 states : 43124
540 states saved : 37760
541 state matches : 7308
542 transitions : 50431
543 trace steps : 33503
544 valid calls : 198225
545 provers : z3, cvc4, cvc3
546 prover calls : 56
547
548=== Result ===
549The standard properties hold for all executions.
550>>>>>>>> Block adder <<<<<<<<
551CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
552
553=== Command ===
554civl verify -inputB=16 -inputW=8 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
555
556=== Stats ===
557 time (s) : 3.35
558 memory (bytes) : 1236795392
559 max process count : 9
560 states : 104715
561 states saved : 96898
562 state matches : 20656
563 transitions : 125370
564 trace steps : 87761
565 valid calls : 510303
566 provers : z3, cvc4, cvc3
567 prover calls : 65
568
569=== Result ===
570The standard properties hold for all executions.
571>>>>>>>> Block adder <<<<<<<<
572CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
573
574=== Command ===
575civl verify -inputB=18 -inputW=9 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
576
577=== Stats ===
578 time (s) : 6.92
579 memory (bytes) : 1757937664
580 max process count : 10
581 states : 254180
582 states saved : 243254
583 state matches : 55512
584 transitions : 309691
585 trace steps : 223543
586 valid calls : 1281761
587 provers : z3, cvc4, cvc3
588 prover calls : 74
589
590=== Result ===
591The standard properties hold for all executions.
592>>>>>>>> Block adder <<<<<<<<
593CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
59416s: mem=3152Mb trans=697377 traceSteps=511965 explored=565119 saved=551191 prove=83
595
596=== Command ===
597civl verify -inputB=20 -inputW=10 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
598
599=== Stats ===
600 time (s) : 16.01
601 memory (bytes) : 3305635840
602 max process count : 11
603 states : 613471
604 states saved : 598702
605 state matches : 143620
606 transitions : 757090
607 trace steps : 556061
608 valid calls : 3154239
609 provers : z3, cvc4, cvc3
610 prover calls : 83
611
612=== Result ===
613The standard properties hold for all executions.
614>>>>>>>> Block adder <<<<<<<<
615CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
61616s: mem=3103Mb trans=754838 traceSteps=558252 explored=606364 saved=596345 prove=92
61731s: mem=3382Mb trans=1549342 traceSteps=1148337 explored=1243618 saved=1226342 prove=92
618
619=== Command ===
620civl verify -inputB=22 -inputW=11 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/blockAdder.cvl
621
622=== Stats ===
623 time (s) : 34.31
624 memory (bytes) : 3344957440
625 max process count : 12
626 states : 1467356
627 states saved : 1447932
628 state matches : 360756
629 transitions : 1828111
630 trace steps : 1355663
631 valid calls : 7627553
632 provers : z3, cvc4, cvc3
633 prover calls : 92
634
635=== Result ===
636The standard properties hold for all executions.
637>>>>>>>> Dining philosopher <<<<<<<<
638CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
639
640=== Command ===
641civl verify -intOperationTransformer=false -inputBOUND=2 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
642
643=== Stats ===
644 time (s) : 0.94
645 memory (bytes) : 514850816
646 max process count : 3
647 states : 42
648 states saved : 30
649 state matches : 4
650 transitions : 43
651 trace steps : 27
652 valid calls : 155
653 provers : z3, cvc4, cvc3
654 prover calls : 0
655
656=== Result ===
657The standard properties hold for all executions.
658>>>>>>>> Dining philosopher <<<<<<<<
659CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
660
661=== Command ===
662civl verify -intOperationTransformer=false -inputBOUND=3 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
663
664=== Stats ===
665 time (s) : 0.23
666 memory (bytes) : 514850816
667 max process count : 4
668 states : 147
669 states saved : 103
670 state matches : 40
671 transitions : 182
672 trace steps : 130
673 valid calls : 786
674 provers : z3, cvc4, cvc3
675 prover calls : 2
676
677=== Result ===
678The standard properties hold for all executions.
679>>>>>>>> Dining philosopher <<<<<<<<
680CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
681
682=== Command ===
683civl verify -intOperationTransformer=false -inputBOUND=4 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
684
685=== Stats ===
686 time (s) : 0.29
687 memory (bytes) : 514850816
688 max process count : 5
689 states : 459
690 states saved : 306
691 state matches : 193
692 transitions : 645
693 trace steps : 479
694 valid calls : 3075
695 provers : z3, cvc4, cvc3
696 prover calls : 3
697
698=== Result ===
699The standard properties hold for all executions.
700>>>>>>>> Dining philosopher <<<<<<<<
701CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
702
703=== Command ===
704civl verify -intOperationTransformer=false -inputBOUND=5 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
705
706=== Stats ===
707 time (s) : 0.32
708 memory (bytes) : 514850816
709 max process count : 6
710 states : 1588
711 states saved : 1013
712 state matches : 912
713 transitions : 2491
714 trace steps : 1897
715 valid calls : 12530
716 provers : z3, cvc4, cvc3
717 prover calls : 4
718
719=== Result ===
720The standard properties hold for all executions.
721>>>>>>>> Dining philosopher <<<<<<<<
722CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
723
724=== Command ===
725civl verify -intOperationTransformer=false -inputBOUND=6 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
726
727=== Stats ===
728 time (s) : 0.47
729 memory (bytes) : 514850816
730 max process count : 7
731 states : 5086
732 states saved : 3135
733 state matches : 3341
734 transitions : 8416
735 trace steps : 6439
736 valid calls : 44771
737 provers : z3, cvc4, cvc3
738 prover calls : 5
739
740=== Result ===
741The standard properties hold for all executions.
742>>>>>>>> Dining philosopher <<<<<<<<
743CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
744
745=== Command ===
746civl verify -intOperationTransformer=false -inputBOUND=7 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
747
748=== Stats ===
749 time (s) : 1.0
750 memory (bytes) : 649592832
751 max process count : 8
752 states : 17899
753 states saved : 10766
754 state matches : 13210
755 transitions : 31096
756 trace steps : 23929
757 valid calls : 171825
758 provers : z3, cvc4, cvc3
759 prover calls : 6
760
761=== Result ===
762The standard properties hold for all executions.
763>>>>>>>> Dining philosopher <<<<<<<<
764CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
765
766=== Command ===
767civl verify -intOperationTransformer=false -inputBOUND=8 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
768
769=== Stats ===
770 time (s) : 1.99
771 memory (bytes) : 1447034880
772 max process count : 9
773 states : 56897
774 states saved : 33556
775 state matches : 44322
776 transitions : 101204
777 trace steps : 77820
778 valid calls : 588778
779 provers : z3, cvc4, cvc3
780 prover calls : 7
781
782=== Result ===
783The standard properties hold for all executions.
784>>>>>>>> Dining philosopher <<<<<<<<
785CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
786
787=== Command ===
788civl verify -intOperationTransformer=false -inputBOUND=9 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
789
790=== Stats ===
791 time (s) : 6.77
792 memory (bytes) : 3126853632
793 max process count : 10
794 states : 198388
795 states saved : 115248
796 state matches : 164564
797 transitions : 362935
798 trace steps : 279742
799 valid calls : 2190268
800 provers : z3, cvc4, cvc3
801 prover calls : 8
802
803=== Result ===
804The standard properties hold for all executions.
805>>>>>>>> Dining philosopher <<<<<<<<
806CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
80716s: mem=3042Mb trans=780893 traceSteps=592669 explored=467455 saved=279295 prove=9
808
809=== Command ===
810civl verify -intOperationTransformer=false -inputBOUND=10 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
811
812=== Stats ===
813 time (s) : 20.12
814 memory (bytes) : 3189768192
815 max process count : 11
816 states : 619996
817 states saved : 355589
818 state matches : 528608
819 transitions : 1148585
820 trace steps : 884114
821 valid calls : 7276913
822 provers : z3, cvc4, cvc3
823 prover calls : 9
824
825=== Result ===
826The standard properties hold for all executions.
827>>>>>>>> Dining philosopher <<<<<<<<
828CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
82916s: mem=3032Mb trans=743042 traceSteps=563966 explored=449126 saved=270114 prove=10
83031s: mem=3010Mb trans=1390388 traceSteps=1074513 explored=810365 saved=494567 prove=10
83146s: mem=3315Mb trans=1930955 traceSteps=1477035 explored=1174746 saved=720902 prove=10
83261s: mem=3298Mb trans=2741303 traceSteps=2084001 explored=1602462 saved=945235 prove=10
83376s: mem=3225Mb trans=3644457 traceSteps=2784874 explored=2007057 saved=1147548 prove=10
834
835=== Command ===
836civl verify -intOperationTransformer=false -inputBOUND=11 /Users/ziqingluo/Documents/workspace/CIVL//examples/concurrency/dining.cvl
837
838=== Stats ===
839 time (s) : 80.28
840 memory (bytes) : 3370647552
841 max process count : 12
842 states : 2130737
843 states saved : 1209388
844 state matches : 1890539
845 transitions : 4021255
846 trace steps : 3099830
847 valid calls : 26377866
848 provers : z3, cvc4, cvc3
849 prover calls : 10
850
851=== Result ===
852The standard properties hold for all executions.
853>>>>>>>> Diffusion2d <<<<<<<<
854CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
855
856=== Command ===
857civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=1 -inputNPROCSXB=1 -inputNPROCSYB=1 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
858
859=== Stats ===
860 time (s) : 3.87
861 memory (bytes) : 919076864
862 max process count : 2
863 states : 1139
864 states saved : 787
865 state matches : 0
866 transitions : 1137
867 trace steps : 550
868 valid calls : 2773
869 provers : z3, cvc4, cvc3
870 prover calls : 5
871
872=== Result ===
873The standard properties hold for all executions.
874>>>>>>>> Diffusion2d <<<<<<<<
875CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
876
877=== Command ===
878civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=2 -inputNPROCSXB=1 -inputNPROCSYB=2 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
879
880=== Stats ===
881 time (s) : 2.37
882 memory (bytes) : 919076864
883 max process count : 2
884 states : 2283
885 states saved : 1653
886 state matches : 0
887 transitions : 2281
888 trace steps : 1165
889 valid calls : 6210
890 provers : z3, cvc4, cvc3
891 prover calls : 9
892
893=== Result ===
894The standard properties hold for all executions.
895>>>>>>>> Diffusion2d <<<<<<<<
896CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
897
898=== Command ===
899civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=3 -inputNPROCSXB=1 -inputNPROCSYB=3 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
900
901=== Stats ===
902 time (s) : 2.12
903 memory (bytes) : 1492647936
904 max process count : 2
905 states : 3604
906 states saved : 2655
907 state matches : 0
908 transitions : 3602
909 trace steps : 1885
910 valid calls : 10472
911 provers : z3, cvc4, cvc3
912 prover calls : 12
913
914=== Result ===
915The standard properties hold for all executions.
916>>>>>>>> Diffusion2d <<<<<<<<
917CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
918
919=== Command ===
920civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=2 -inputNPROCSXB=2 -inputNPROCSYB=2 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
921
922=== Stats ===
923 time (s) : 4.29
924 memory (bytes) : 1511522304
925 max process count : 3
926 states : 14317
927 states saved : 9950
928 state matches : 0
929 transitions : 14314
930 trace steps : 6863
931 valid calls : 38798
932 provers : z3, cvc4, cvc3
933 prover calls : 19
934
935=== Result ===
936The standard properties hold for all executions.
937>>>>>>>> Diffusion2d <<<<<<<<
938CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
939
940=== Command ===
941civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=3 -inputNPROCSXB=2 -inputNPROCSYB=3 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
942
943=== Stats ===
944 time (s) : 4.66
945 memory (bytes) : 2580021248
946 max process count : 3
947 states : 23502
948 states saved : 16341
949 state matches : 0
950 transitions : 23499
951 trace steps : 11319
952 valid calls : 66193
953 provers : z3, cvc4, cvc3
954 prover calls : 22
955
956=== Result ===
957The standard properties hold for all executions.
958>>>>>>>> Diffusion2d <<<<<<<<
959CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
960
961=== Command ===
962civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=3 -inputNPROCSXB=3 -inputNPROCSYB=3 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
963
964=== Stats ===
965 time (s) : 14.2
966 memory (bytes) : 3006791680
967 max process count : 4
968 states : 76097
969 states saved : 50931
970 state matches : 0
971 transitions : 76093
972 trace steps : 34877
973 valid calls : 213879
974 provers : z3, cvc4, cvc3
975 prover calls : 36
976
977=== Result ===
978The standard properties hold for all executions.
979>>>>>>>> Diffusion2d <<<<<<<<
980CIVL v1.11+ of 2017-07-07 -- http://vsl.cis.udel.edu/civl
98117s: mem=2864Mb trans=96558 traceSteps=44627 explored=96562 saved=64715 prove=39
982
983=== Command ===
984civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=4 -inputNPROCSXB=3 -inputNPROCSYB=4 -enablePrintf=false /Users/ziqingluo/Documents/workspace/CIVL//examples/mpi/diffusion2d.c
985
986=== Stats ===
987 time (s) : 18.81
988 memory (bytes) : 3019374592
989 max process count : 4
990 states : 111272
991 states saved : 74273
992 state matches : 0
993 transitions : 111268
994 trace steps : 50994
995 valid calls : 320108
996 provers : z3, cvc4, cvc3
997 prover calls : 39
998
999=== Result ===
1000The standard properties hold for all executions.
Note: See TracBrowser for help on using the repository browser.