A forum for Spin users
You are not logged in.
Pages: 1
Hi,
I would like to configure Spin so that it uses hash-compact with 14GB without running out of memory.
Unfortunately, playing with the -DHC makes no difference, case 1 with -DHC0 and case 2 with -DHC4 yield the same out of memory (see below).
So: Is this a bug or do I have to additionaly modify some other options? Which ones?
Thanks,
David
Case 1)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC0 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth= 753 States= 1e+06 Transitions= 1.01e+06 Memory= 166.672 t= 0.94 R= 1e+06
....
Depth= 813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660 t= 661 R= 5e+05
pan: reached -DMEMLIM bound
1.47324e+10 bytes used
102400 bytes more needed
1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts: 77109092 (resolved)
Stats on memory usage (in Megabytes):
78944.851 equivalent memory usage for states (stored*(State-vector + overhead))
12002.095 actual memory usage for states (compression: 15.20%)
state-vector as stored = 14 byte + 28 byte overhead
2048.000 memory used for hash table (-w28)
0.054 memory used for DFS stack (-m1000)
14049.914 total actual memory usage
Case 2)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC4 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth= 753 States= 1e+06 Transitions= 1.01e+06 Memory= 166.672 t= 1.12 R= 9e+05
...
Depth= 813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660 t= 596 R= 5e+05
pan: reached -DMEMLIM bound
1.47324e+10 bytes used
102400 bytes more needed
1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts: 77109092 (resolved)
Stats on memory usage (in Megabytes):
78944.851 equivalent memory usage for states (stored*(State-vector + overhead))
12002.095 actual memory usage for states (compression: 15.20%)
state-vector as stored = 14 byte + 28 byte overhead
2048.000 memory used for hash table (-w28)
0.054 memory used for DFS stack (-m1000)
14049.914 total actual memory usage
Offline
Yes, that is confusing at best -- or misleading really.
There is actually only one hashcompact mode -- all others (HC0, HC1, and HC3) map to the behavior of HC4.
I should document that somewhere in the manpages, sorry!
Offline
Thanks for the clarification.
Too bad -DHC0 does not have the effect as described in the spin book, since I have a huge state space and only 14GB of memory available. Thus using 32bit values would be a good approach in spite of the higher collision risk.
So is there a possibility to do this?
Offline
Pages: 1