source: CIVL/mods/dev.civl.com/scripts/scale/v1.14_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: 31.2 KB
Line 
1>>>>>>>> Adder <<<<<<<<
2CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
3
4=== Command ===
5civl verify -inputB=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
6
7=== Stats ===
8 time (s) : 1.25
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 : 91
17 provers : cvc4, z3, cvc3
18 prover calls : 2
19
20=== Result ===
21The standard properties hold for all executions.
22>>>>>>>> Adder <<<<<<<<
23CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
24
25=== Command ===
26civl verify -inputB=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
27
28=== Stats ===
29 time (s) : 0.35
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 : 219
38 provers : cvc4, z3, cvc3
39 prover calls : 4
40
41=== Result ===
42The standard properties hold for all executions.
43>>>>>>>> Adder <<<<<<<<
44CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
45
46=== Command ===
47civl verify -inputB=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
48
49=== Stats ===
50 time (s) : 0.43
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 : 508
59 provers : cvc4, z3, cvc3
60 prover calls : 6
61
62=== Result ===
63The standard properties hold for all executions.
64>>>>>>>> Adder <<<<<<<<
65CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
66
67=== Command ===
68civl verify -inputB=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
69
70=== Stats ===
71 time (s) : 0.49
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 : 1162
80 provers : cvc4, z3, cvc3
81 prover calls : 8
82
83=== Result ===
84The standard properties hold for all executions.
85>>>>>>>> Adder <<<<<<<<
86CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
87
88=== Command ===
89civl verify -inputB=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
90
91=== Stats ===
92 time (s) : 0.58
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 : 2629
101 provers : cvc4, z3, cvc3
102 prover calls : 10
103
104=== Result ===
105The standard properties hold for all executions.
106>>>>>>>> Adder <<<<<<<<
107CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
108
109=== Command ===
110civl verify -inputB=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
111
112=== Stats ===
113 time (s) : 0.72
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 : 5885
122 provers : cvc4, z3, cvc3
123 prover calls : 12
124
125=== Result ===
126The standard properties hold for all executions.
127>>>>>>>> Adder <<<<<<<<
128CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
129
130=== Command ===
131civl verify -inputB=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
132
133=== Stats ===
134 time (s) : 0.88
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 : 13042
143 provers : cvc4, z3, cvc3
144 prover calls : 14
145
146=== Result ===
147The standard properties hold for all executions.
148>>>>>>>> Adder <<<<<<<<
149CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
150
151=== Command ===
152civl verify -inputB=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
153
154=== Stats ===
155 time (s) : 1.22
156 memory (bytes) : 504365056
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 : 28644
164 provers : cvc4, z3, cvc3
165 prover calls : 16
166
167=== Result ===
168The standard properties hold for all executions.
169>>>>>>>> Adder <<<<<<<<
170CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
171
172=== Command ===
173civl verify -inputB=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
174
175=== Stats ===
176 time (s) : 1.66
177 memory (bytes) : 789577728
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 : 62419
185 provers : cvc4, z3, cvc3
186 prover calls : 18
187
188=== Result ===
189The standard properties hold for all executions.
190>>>>>>>> Adder <<<<<<<<
191CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
192
193=== Command ===
194civl verify -inputB=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
195
196=== Stats ===
197 time (s) : 2.58
198 memory (bytes) : 1039663104
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 : 135103
206 provers : cvc4, z3, cvc3
207 prover calls : 20
208
209=== Result ===
210The standard properties hold for all executions.
211>>>>>>>> Adder <<<<<<<<
212CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
213
214=== Command ===
215civl verify -inputB=12 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
216
217=== Stats ===
218 time (s) : 4.68
219 memory (bytes) : 2087714816
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 : 290728
227 provers : cvc4, z3, cvc3
228 prover calls : 22
229
230=== Result ===
231The standard properties hold for all executions.
232>>>>>>>> Adder <<<<<<<<
233CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
234
235=== Command ===
236civl verify -inputB=13 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
237
238=== Stats ===
239 time (s) : 10.19
240 memory (bytes) : 3173515264
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 : 622478
248 provers : cvc4, z3, cvc3
249 prover calls : 24
250
251=== Result ===
252The standard properties hold for all executions.
253>>>>>>>> Adder <<<<<<<<
254CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
25516s: mem=3098Mb trans=1175479 traceSteps=836293 explored=1040899 saved=906333 prove=26
256
257=== Command ===
258civl verify -inputB=14 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/adder.cvl
259
260=== Stats ===
261 time (s) : 22.57
262 memory (bytes) : 3839361024
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 : 1326961
270 provers : cvc4, z3, cvc3
271 prover calls : 26
272
273=== Result ===
274The standard properties hold for all executions.
275>>>>>>>> Barrier <<<<<<<<
276CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
277
278=== Command ===
279civl verify -inputB=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
280
281=== Stats ===
282 time (s) : 1.05
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 : 863
291 provers : cvc4, z3, cvc3
292 prover calls : 2
293
294=== Result ===
295The standard properties hold for all executions.
296>>>>>>>> Barrier <<<<<<<<
297CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
298
299=== Command ===
300civl verify -inputB=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
301
302=== Stats ===
303 time (s) : 0.4
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 : 4920
312 provers : cvc4, z3, cvc3
313 prover calls : 3
314
315=== Result ===
316The standard properties hold for all executions.
317>>>>>>>> Barrier <<<<<<<<
318CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
319
320=== Command ===
321civl verify -inputB=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
322
323=== Stats ===
324 time (s) : 0.51
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 : 25118
333 provers : cvc4, z3, cvc3
334 prover calls : 4
335
336=== Result ===
337The standard properties hold for all executions.
338>>>>>>>> Barrier <<<<<<<<
339CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
340
341=== Command ===
342civl verify -inputB=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
343
344=== Stats ===
345 time (s) : 1.01
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 : 122504
354 provers : cvc4, z3, cvc3
355 prover calls : 5
356
357=== Result ===
358The standard properties hold for all executions.
359>>>>>>>> Barrier <<<<<<<<
360CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
361
362=== Command ===
363civl verify -inputB=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
364
365=== Stats ===
366 time (s) : 2.29
367 memory (bytes) : 1449132032
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 : 582487
375 provers : cvc4, z3, cvc3
376 prover calls : 6
377
378=== Result ===
379The standard properties hold for all executions.
380>>>>>>>> Barrier <<<<<<<<
381CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
382
383=== Command ===
384civl verify -inputB=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
385
386=== Stats ===
387 time (s) : 9.29
388 memory (bytes) : 3127377920
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 : 2719222
396 provers : cvc4, z3, cvc3
397 prover calls : 7
398
399=== Result ===
400The standard properties hold for all executions.
401>>>>>>>> Barrier <<<<<<<<
402CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
40316s: mem=3104Mb trans=2009934 traceSteps=721270 explored=1503318 saved=591940 prove=8
40431s: mem=2992Mb trans=4061863 traceSteps=1463553 explored=2998363 saved=1204673 prove=8
40546s: mem=3311Mb trans=5831150 traceSteps=2045850 explored=4281517 saved=1657605 prove=8
406
407=== Command ===
408civl verify -inputB=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/barrier.cvl
409
410=== Stats ===
411 time (s) : 47.47
412 memory (bytes) : 3496476672
413 max process count : 9
414 states : 4540601
415 states saved : 1770300
416 state matches : 1661020
417 transitions : 6201604
418 trace steps : 2178150
419 valid calls : 12507866
420 provers : cvc4, z3, cvc3
421 prover calls : 8
422
423=== Result ===
424The standard properties hold for all executions.
425>>>>>>>> Block adder <<<<<<<<
426CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
427
428=== Command ===
429civl verify -inputB=4 -inputW=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
430
431=== Stats ===
432 time (s) : 1.3
433 memory (bytes) : 514850816
434 max process count : 3
435 states : 399
436 states saved : 190
437 state matches : 4
438 transitions : 402
439 trace steps : 125
440 valid calls : 1167
441 provers : cvc4, z3, cvc3
442 prover calls : 8
443
444=== Result ===
445The standard properties hold for all executions.
446>>>>>>>> Block adder <<<<<<<<
447CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
448
449=== Command ===
450civl verify -inputB=6 -inputW=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
451
452=== Stats ===
453 time (s) : 0.79
454 memory (bytes) : 514850816
455 max process count : 4
456 states : 1196
457 states saved : 644
458 state matches : 36
459 transitions : 1231
460 trace steps : 463
461 valid calls : 4772
462 provers : cvc4, z3, cvc3
463 prover calls : 14
464
465=== Result ===
466The standard properties hold for all executions.
467>>>>>>>> Block adder <<<<<<<<
468CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
469
470=== Command ===
471civl verify -inputB=8 -inputW=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
472
473=== Stats ===
474 time (s) : 1.02
475 memory (bytes) : 514850816
476 max process count : 5
477 states : 3067
478 states saved : 1906
479 state matches : 184
480 transitions : 3250
481 trace steps : 1481
482 valid calls : 15639
483 provers : cvc4, z3, cvc3
484 prover calls : 20
485
486=== Result ===
487The standard properties hold for all executions.
488>>>>>>>> Block adder <<<<<<<<
489CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
490
491=== Command ===
492civl verify -inputB=10 -inputW=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
493
494=== Stats ===
495 time (s) : 1.3
496 memory (bytes) : 514850816
497 max process count : 6
498 states : 7436
499 states saved : 5322
500 state matches : 720
501 transitions : 8155
502 trace steps : 4391
503 valid calls : 45884
504 provers : cvc4, z3, cvc3
505 prover calls : 26
506
507=== Result ===
508The standard properties hold for all executions.
509>>>>>>>> Block adder <<<<<<<<
510CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
511
512=== Command ===
513civl verify -inputB=12 -inputW=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
514
515=== Stats ===
516 time (s) : 1.74
517 memory (bytes) : 514850816
518 max process count : 7
519 states : 17855
520 states saved : 14366
521 state matches : 2412
522 transitions : 20266
523 trace steps : 12373
524 valid calls : 126359
525 provers : cvc4, z3, cvc3
526 prover calls : 32
527
528=== Result ===
529The standard properties hold for all executions.
530>>>>>>>> Block adder <<<<<<<<
531CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
532
533=== Command ===
534civl verify -inputB=14 -inputW=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
535
536=== Stats ===
537 time (s) : 2.31
538 memory (bytes) : 911736832
539 max process count : 8
540 states : 43124
541 states saved : 37760
542 state matches : 7308
543 transitions : 50431
544 trace steps : 33503
545 valid calls : 333948
546 provers : cvc4, z3, cvc3
547 prover calls : 38
548
549=== Result ===
550The standard properties hold for all executions.
551>>>>>>>> Block adder <<<<<<<<
552CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
553
554=== Command ===
555civl verify -inputB=16 -inputW=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
556
557=== Stats ===
558 time (s) : 3.82
559 memory (bytes) : 1231552512
560 max process count : 9
561 states : 104715
562 states saved : 96898
563 state matches : 20656
564 transitions : 125370
565 trace steps : 87761
566 valid calls : 856463
567 provers : cvc4, z3, cvc3
568 prover calls : 44
569
570=== Result ===
571The standard properties hold for all executions.
572>>>>>>>> Block adder <<<<<<<<
573CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
574
575=== Command ===
576civl verify -inputB=18 -inputW=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
577
578=== Stats ===
579 time (s) : 7.29
580 memory (bytes) : 2570584064
581 max process count : 10
582 states : 254180
583 states saved : 243254
584 state matches : 55512
585 transitions : 309691
586 trace steps : 223543
587 valid calls : 2144708
588 provers : cvc4, z3, cvc3
589 prover calls : 50
590
591=== Result ===
592The standard properties hold for all executions.
593>>>>>>>> Block adder <<<<<<<<
594CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
59517s: mem=3179Mb trans=711270 traceSteps=522328 explored=576255 saved=562255 prove=56
596
597=== Command ===
598civl verify -inputB=20 -inputW=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
599
600=== Stats ===
601 time (s) : 16.83
602 memory (bytes) : 3333947392
603 max process count : 11
604 states : 613471
605 states saved : 598702
606 state matches : 143620
607 transitions : 757090
608 trace steps : 556061
609 valid calls : 5264479
610 provers : cvc4, z3, cvc3
611 prover calls : 56
612
613=== Result ===
614The standard properties hold for all executions.
615>>>>>>>> Block adder <<<<<<<<
616CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
61716s: mem=3113Mb trans=686467 traceSteps=507735 explored=551380 saved=542323 prove=62
61831s: mem=3346Mb trans=1439151 traceSteps=1066299 explored=1155411 saved=1138884 prove=62
619
620=== Command ===
621civl verify -inputB=22 -inputW=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/blockAdder.cvl
622
623=== Stats ===
624 time (s) : 36.15
625 memory (bytes) : 3535798272
626 max process count : 12
627 states : 1467356
628 states saved : 1447932
629 state matches : 360756
630 transitions : 1828111
631 trace steps : 1355663
632 valid calls : 12702964
633 provers : cvc4, z3, cvc3
634 prover calls : 62
635
636=== Result ===
637The standard properties hold for all executions.
638>>>>>>>> Dining philosopher <<<<<<<<
639CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
640
641=== Command ===
642civl verify -intOperationTransformer=false -inputBOUND=2 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
643
644=== Stats ===
645 time (s) : 0.96
646 memory (bytes) : 514850816
647 max process count : 3
648 states : 42
649 states saved : 30
650 state matches : 4
651 transitions : 43
652 trace steps : 27
653 valid calls : 213
654 provers : cvc4, z3, cvc3
655 prover calls : 0
656
657=== Result ===
658The standard properties hold for all executions.
659>>>>>>>> Dining philosopher <<<<<<<<
660CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
661
662=== Command ===
663civl verify -intOperationTransformer=false -inputBOUND=3 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
664
665=== Stats ===
666 time (s) : 0.3
667 memory (bytes) : 514850816
668 max process count : 4
669 states : 147
670 states saved : 103
671 state matches : 40
672 transitions : 182
673 trace steps : 130
674 valid calls : 1149
675 provers : cvc4, z3, cvc3
676 prover calls : 2
677
678=== Result ===
679The standard properties hold for all executions.
680>>>>>>>> Dining philosopher <<<<<<<<
681CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
682
683=== Command ===
684civl verify -intOperationTransformer=false -inputBOUND=4 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
685
686=== Stats ===
687 time (s) : 0.36
688 memory (bytes) : 514850816
689 max process count : 5
690 states : 459
691 states saved : 306
692 state matches : 193
693 transitions : 645
694 trace steps : 479
695 valid calls : 4592
696 provers : cvc4, z3, cvc3
697 prover calls : 3
698
699=== Result ===
700The standard properties hold for all executions.
701>>>>>>>> Dining philosopher <<<<<<<<
702CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
703
704=== Command ===
705civl verify -intOperationTransformer=false -inputBOUND=5 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
706
707=== Stats ===
708 time (s) : 0.41
709 memory (bytes) : 514850816
710 max process count : 6
711 states : 1588
712 states saved : 1013
713 state matches : 912
714 transitions : 2491
715 trace steps : 1897
716 valid calls : 18932
717 provers : cvc4, z3, cvc3
718 prover calls : 4
719
720=== Result ===
721The standard properties hold for all executions.
722>>>>>>>> Dining philosopher <<<<<<<<
723CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
724
725=== Command ===
726civl verify -intOperationTransformer=false -inputBOUND=6 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
727
728=== Stats ===
729 time (s) : 0.59
730 memory (bytes) : 514850816
731 max process count : 7
732 states : 5086
733 states saved : 3135
734 state matches : 3341
735 transitions : 8416
736 trace steps : 6439
737 valid calls : 67751
738 provers : cvc4, z3, cvc3
739 prover calls : 5
740
741=== Result ===
742The standard properties hold for all executions.
743>>>>>>>> Dining philosopher <<<<<<<<
744CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
745
746=== Command ===
747civl verify -intOperationTransformer=false -inputBOUND=7 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
748
749=== Stats ===
750 time (s) : 1.03
751 memory (bytes) : 649592832
752 max process count : 8
753 states : 17899
754 states saved : 10766
755 state matches : 13210
756 transitions : 31096
757 trace steps : 23929
758 valid calls : 260545
759 provers : cvc4, z3, cvc3
760 prover calls : 6
761
762=== Result ===
763The standard properties hold for all executions.
764>>>>>>>> Dining philosopher <<<<<<<<
765CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
766
767=== Command ===
768civl verify -intOperationTransformer=false -inputBOUND=8 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
769
770=== Stats ===
771 time (s) : 1.91
772 memory (bytes) : 1445462016
773 max process count : 9
774 states : 56897
775 states saved : 33556
776 state matches : 44322
777 transitions : 101204
778 trace steps : 77820
779 valid calls : 891894
780 provers : cvc4, z3, cvc3
781 prover calls : 7
782
783=== Result ===
784The standard properties hold for all executions.
785>>>>>>>> Dining philosopher <<<<<<<<
786CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
787
788=== Command ===
789civl verify -intOperationTransformer=false -inputBOUND=9 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
790
791=== Stats ===
792 time (s) : 6.09
793 memory (bytes) : 3124756480
794 max process count : 10
795 states : 198388
796 states saved : 115248
797 state matches : 164564
798 transitions : 362935
799 trace steps : 279742
800 valid calls : 3319541
801 provers : cvc4, z3, cvc3
802 prover calls : 8
803
804=== Result ===
805The standard properties hold for all executions.
806>>>>>>>> Dining philosopher <<<<<<<<
807CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
80816s: mem=3040Mb trans=897240 traceSteps=681675 explored=522184 saved=306683 prove=9
809
810=== Command ===
811civl verify -intOperationTransformer=false -inputBOUND=10 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
812
813=== Stats ===
814 time (s) : 18.01
815 memory (bytes) : 3187146752
816 max process count : 11
817 states : 619996
818 states saved : 355589
819 state matches : 528608
820 transitions : 1148585
821 trace steps : 884114
822 valid calls : 11016852
823 provers : cvc4, z3, cvc3
824 prover calls : 9
825
826=== Result ===
827The standard properties hold for all executions.
828>>>>>>>> Dining philosopher <<<<<<<<
829CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
83016s: mem=3043Mb trans=878298 traceSteps=667143 explored=513358 saved=302268 prove=10
83131s: mem=3027Mb trans=1589082 traceSteps=1226082 explored=944946 saved=582022 prove=10
83246s: mem=3348Mb trans=2364691 traceSteps=1795674 explored=1425838 saved=856898 prove=10
83361s: mem=3309Mb trans=3435878 traceSteps=2620878 explored=1917887 saved=1102963 prove=10
834
835=== Command ===
836civl verify -intOperationTransformer=false -inputBOUND=11 /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/concurrency/dining.cvl
837
838=== Stats ===
839 time (s) : 67.52
840 memory (bytes) : 3448242176
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 : 39942930
848 provers : cvc4, z3, cvc3
849 prover calls : 10
850
851=== Result ===
852The standard properties hold for all executions.
853>>>>>>>> Diffusion2d <<<<<<<<
854CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
855
856=== Command ===
857civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=1 -inputNPROCSXB=1 -inputNPROCSYB=1 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
858
859=== Stats ===
860 time (s) : 4.35
861 memory (bytes) : 919076864
862 max process count : 2
863 states : 1140
864 states saved : 775
865 state matches : 0
866 transitions : 1138
867 trace steps : 538
868 valid calls : 3313
869 provers : cvc4, z3, cvc3
870 prover calls : 3
871
872=== Result ===
873The standard properties hold for all executions.
874>>>>>>>> Diffusion2d <<<<<<<<
875CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
876
877=== Command ===
878civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=2 -inputNPROCSXB=1 -inputNPROCSYB=2 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
879
880=== Stats ===
881 time (s) : 2.68
882 memory (bytes) : 1512046592
883 max process count : 2
884 states : 2284
885 states saved : 1629
886 state matches : 0
887 transitions : 2282
888 trace steps : 1141
889 valid calls : 7463
890 provers : cvc4, z3, cvc3
891 prover calls : 5
892
893=== Result ===
894The standard properties hold for all executions.
895>>>>>>>> Diffusion2d <<<<<<<<
896CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
897
898=== Command ===
899civl verify -inputNSTEPSB=2 -inputNXB=1 -inputNYB=3 -inputNPROCSXB=1 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
900
901=== Stats ===
902 time (s) : 2.95
903 memory (bytes) : 1512046592
904 max process count : 2
905 states : 3605
906 states saved : 2619
907 state matches : 0
908 transitions : 3603
909 trace steps : 1849
910 valid calls : 12629
911 provers : cvc4, z3, cvc3
912 prover calls : 7
913
914=== Result ===
915The standard properties hold for all executions.
916>>>>>>>> Diffusion2d <<<<<<<<
917CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
918
919=== Command ===
920civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=2 -inputNPROCSXB=2 -inputNPROCSYB=2 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
921
922=== Stats ===
923 time (s) : 4.93
924 memory (bytes) : 2589982720
925 max process count : 3
926 states : 14327
927 states saved : 9800
928 state matches : 0
929 transitions : 14324
930 trace steps : 6713
931 valid calls : 52083
932 provers : cvc4, z3, cvc3
933 prover calls : 15
934
935=== Result ===
936The standard properties hold for all executions.
937>>>>>>>> Diffusion2d <<<<<<<<
938CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
939
940=== Command ===
941civl verify -inputNSTEPSB=2 -inputNXB=2 -inputNYB=3 -inputNPROCSXB=2 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
942
943=== Stats ===
944 time (s) : 6.48
945 memory (bytes) : 2619867136
946 max process count : 3
947 states : 23516
948 states saved : 16107
949 state matches : 0
950 transitions : 23513
951 trace steps : 11085
952 valid calls : 88651
953 provers : cvc4, z3, cvc3
954 prover calls : 17
955
956=== Result ===
957The standard properties hold for all executions.
958>>>>>>>> Diffusion2d <<<<<<<<
959CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
96017s: mem=2842Mb trans=72341 traceSteps=32520 explored=72344 saved=47742 prove=34
961
962=== Command ===
963civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=3 -inputNPROCSXB=3 -inputNPROCSYB=3 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
964
965=== Stats ===
966 time (s) : 17.41
967 memory (bytes) : 2980577280
968 max process count : 4
969 states : 76154
970 states saved : 50193
971 state matches : 0
972 transitions : 76150
973 trace steps : 34139
974 valid calls : 310971
975 provers : cvc4, z3, cvc3
976 prover calls : 34
977
978=== Result ===
979The standard properties hold for all executions.
980>>>>>>>> Diffusion2d <<<<<<<<
981CIVL v1.14 of 2018-03-16 -- http://vsl.cis.udel.edu/civl
98217s: mem=2963Mb trans=73950 traceSteps=34165 explored=73953 saved=49471 prove=36
983
984=== Command ===
985civl verify -inputNSTEPSB=2 -inputNXB=3 -inputNYB=4 -inputNPROCSXB=3 -inputNPROCSYB=4 -enablePrintf=false /Users/yihaoyan/Documents/eclipseMars/trunk/CIVL/examples/mpi/diffusion2d.c
986
987=== Stats ===
988 time (s) : 24.7
989 memory (bytes) : 3112173568
990 max process count : 4
991 states : 111347
992 states saved : 73235
993 state matches : 0
994 transitions : 111343
995 trace steps : 49956
996 valid calls : 463610
997 provers : cvc4, z3, cvc3
998 prover calls : 36
999
1000=== Result ===
1001The standard properties hold for all executions.
Note: See TracBrowser for help on using the repository browser.