1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/formal-model/urcu-controldataflow-intel-ipi-compress'
2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
4 cat .input.define >> pan.ltl
6 spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl
7 cat .input.define > .input.spin
8 cat DEFINES >> .input.spin
9 cat urcu.spin >> .input.spin
10 rm -f .input.spin.trail
11 spin -a -X -N pan.ltl .input.spin
13 gcc -O2 -w -DHASH64 -DCOLLAPSE -o pan pan.c
14 ./pan -a -v -c1 -X -m10000000 -w20
15 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
16 (never claims generated from LTL formulae are stutter-invariant)
17 depth 0: Claim reached state 5 (line 1294)
18 Depth= 9223 States= 1e+06 Transitions= 6.87e+06 Memory= 516.350 t= 19.4 R= 5e+04
19 Depth= 9223 States= 2e+06 Transitions= 1.47e+07 Memory= 563.713 t= 43.1 R= 5e+04
20 Depth= 9223 States= 3e+06 Transitions= 2.46e+07 Memory= 613.127 t= 73.9 R= 4e+04
21 pan: resizing hashtable to -w22.. done
22 Depth= 9223 States= 4e+06 Transitions= 3.19e+07 Memory= 690.440 t= 95.5 R= 4e+04
23 Depth= 9223 States= 5e+06 Transitions= 3.95e+07 Memory= 736.533 t= 118 R= 4e+04
24 Depth= 9223 States= 6e+06 Transitions= 5.71e+07 Memory= 785.068 t= 174 R= 3e+04
25 Depth= 9223 States= 7e+06 Transitions= 6.81e+07 Memory= 834.580 t= 209 R= 3e+04
26 Depth= 9223 States= 8e+06 Transitions= 8.22e+07 Memory= 883.311 t= 254 R= 3e+04
27 Depth= 9223 States= 9e+06 Transitions= 9.54e+07 Memory= 932.139 t= 296 R= 3e+04
28 pan: resizing hashtable to -w24.. done
29 Depth= 9223 States= 1e+07 Transitions= 1.08e+08 Memory= 1104.670 t= 338 R= 3e+04
30 Depth= 9223 States= 1.1e+07 Transitions= 1.21e+08 Memory= 1155.451 t= 375 R= 3e+04
31 Depth= 9223 States= 1.2e+07 Transitions= 1.3e+08 Memory= 1205.744 t= 403 R= 3e+04
32 Depth= 9223 States= 1.3e+07 Transitions= 1.42e+08 Memory= 1254.572 t= 442 R= 3e+04
33 Depth= 9223 States= 1.4e+07 Transitions= 1.72e+08 Memory= 1302.717 t= 539 R= 3e+04
34 Depth= 9223 States= 1.5e+07 Transitions= 1.91e+08 Memory= 1354.768 t= 600 R= 3e+04
35 Depth= 9223 States= 1.6e+07 Transitions= 2.08e+08 Memory= 1405.842 t= 653 R= 2e+04
36 Depth= 9223 States= 1.7e+07 Transitions= 2.2e+08 Memory= 1456.818 t= 691 R= 2e+04
37 Depth= 9223 States= 1.8e+07 Transitions= 2.39e+08 Memory= 1506.135 t= 751 R= 2e+04
38 Depth= 9223 States= 1.9e+07 Transitions= 2.55e+08 Memory= 1556.330 t= 801 R= 2e+04
39 Depth= 9223 States= 2e+07 Transitions= 2.72e+08 Memory= 1604.084 t= 856 R= 2e+04
40 Depth= 9285 States= 2.1e+07 Transitions= 2.85e+08 Memory= 1650.080 t= 898 R= 2e+04
41 Depth= 9324 States= 2.2e+07 Transitions= 2.99e+08 Memory= 1696.760 t= 941 R= 2e+04
42 Depth= 9324 States= 2.3e+07 Transitions= 3.1e+08 Memory= 1746.369 t= 976 R= 2e+04
43 Depth= 9324 States= 2.4e+07 Transitions= 3.21e+08 Memory= 1792.561 t= 1.01e+03 R= 2e+04
44 Depth= 9324 States= 2.5e+07 Transitions= 3.34e+08 Memory= 1841.096 t= 1.05e+03 R= 2e+04
45 Depth= 9324 States= 2.6e+07 Transitions= 3.45e+08 Memory= 1890.998 t= 1.09e+03 R= 2e+04
46 Depth= 9324 States= 2.7e+07 Transitions= 3.59e+08 Memory= 1940.412 t= 1.13e+03 R= 2e+04
47 Depth= 9324 States= 2.8e+07 Transitions= 3.71e+08 Memory= 1987.776 t= 1.17e+03 R= 2e+04
48 Depth= 9324 States= 2.9e+07 Transitions= 3.84e+08 Memory= 2034.846 t= 1.21e+03 R= 2e+04
49 Depth= 9324 States= 3e+07 Transitions= 3.96e+08 Memory= 2081.233 t= 1.25e+03 R= 2e+04
50 Depth= 9324 States= 3.1e+07 Transitions= 4.09e+08 Memory= 2129.865 t= 1.29e+03 R= 2e+04
51 Depth= 9324 States= 3.2e+07 Transitions= 4.19e+08 Memory= 2179.670 t= 1.32e+03 R= 2e+04
52 Depth= 9324 States= 3.3e+07 Transitions= 4.3e+08 Memory= 2227.717 t= 1.36e+03 R= 2e+04
53 Depth= 9324 States= 3.4e+07 Transitions= 4.44e+08 Memory= 2277.033 t= 1.4e+03 R= 2e+04
54 pan: resizing hashtable to -w26.. done
55 Depth= 9324 States= 3.5e+07 Transitions= 4.6e+08 Memory= 2824.190 t= 1.46e+03 R= 2e+04
projects / urcu.git / blob