=========================================================================== ANALYSIS 1: attempt at full coverage =========================================================================== pan: resizing hashtable to -w35.. pan: out of memory 1.34445e+11 bytes used 2.74878e+11 bytes more needed 1.37439e+11 bytes limit hint: to reduce memory, recompile with -DMA=224 # better/slower compression, or -DBITSTATE # supertrace, approximation (Spin Version 5.1.3 -- 11 December 2007) Warning: Search not completed + Partial Order Reduction + Compression Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 224 byte, depth reached 21280, errors: 0 1.076e+09 states, stored 1.1801585e+09 states, matched 2.2561585e+09 transitions (= stored+matched) 1 atomic steps hash conflicts: 1.1203797e+09 (resolved) Stats on memory usage (in Megabytes): 258590.698 equivalent memory usage for states (stored*(State-vector + overhead)) 0.000 actual memory usage for states (less than 1k) 262144.000 memory used for hash table (-w35) 4.578 memory used for DFS stack (-m100000) 128217.000 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 290451 62155 24005 2 ] unreached in proctype UAC line 110, "pan_in", state 11, "assert(0)" line 119, "pan_in", state 23, "assert(0)" line 125, "pan_in", state 32, "assert(0)" line 156, "pan_in", state 83, "assert(0)" line 176, "pan_in", state 111, "ackc!ack,none" line 176, "pan_in", state 112, "media = flow" line 181, "pan_in", state 122, "assert(0)" line 207, "pan_in", state 166, "assert(0)" line 222, "pan_in", state 188, "assert(0)" line 254, "pan_in", state 237, "assert(0)" line 283, "pan_in", state 289, "assert(0)" line 286, "pan_in", state 295, "assert(0)" line 295, "pan_in", state 317, "assert(0)" line 297, "pan_in", state 322, "assert(0)" line 331, "pan_in", state 398, "assert(0)" line 333, "pan_in", state 402, "-end-" (16 of 402 states) unreached in proctype UAS line 362, "pan_in", state 10, "assert(0)" line 393, "pan_in", state 61, "assert(0)" line 394, "pan_in", state 63, "assert(0)" line 395, "pan_in", state 65, "assert(0)" line 397, "pan_in", state 70, "assert(0)" line 401, "pan_in", state 78, "media = offering" line 402, "pan_in", state 80, "relOut = 1" line 402, "pan_in", state 81, "canSucc = 0" line 414, "pan_in", state 108, "media = offering" line 416, "pan_in", state 113, "media = flow" line 445, "pan_in", state 166, "assert(0)" line 446, "pan_in", state 168, "assert(0)" line 478, "pan_in", state 227, "assert(0)" line 501, "pan_in", state 273, "assert(0)" line 502, "pan_in", state 275, "assert(0)" line 503, "pan_in", state 277, "assert(0)" line 523, "pan_in", state 322, "assert(0)" line 525, "pan_in", state 326, "-end-" (18 of 326 states) unreached in proctype :init: (0 of 4 states) pan: elapsed time 1.98e+04 seconds pan: rate 54287.803 states/second pan: avg transition delay 8.785e-06 usec =========================================================================== ANALYSIS 2: supertrace -w34 =========================================================================== (Spin Version 5.1.3 -- 11 December 2007) + Partial Order Reduction Bit statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 224 byte, depth reached 23238, errors: 0 3.5501939e+09 states, stored 3.9265436e+09 states, matched 7.4767374e+09 transitions (= stored+matched) 1 atomic steps hash factor: 4.83914 (best if > 100.) bits set per state: 3 (-k3) Stats on memory usage (in Megabytes): 826117.803 equivalent memory usage for states (stored*(State-vector + overhead)) 2048.000 memory used for hash array (-w34) 0.763 memory used for bit stack 4.578 memory used for DFS stack (-m100000) 5.739 other (proc and chan stacks) 2059.102 total actual memory usage unreached in proctype UAC line 110, "pan_in", state 11, "assert(0)" line 119, "pan_in", state 23, "assert(0)" line 125, "pan_in", state 32, "assert(0)" line 156, "pan_in", state 83, "assert(0)" line 181, "pan_in", state 122, "assert(0)" line 207, "pan_in", state 166, "assert(0)" line 222, "pan_in", state 188, "assert(0)" line 254, "pan_in", state 237, "assert(0)" line 283, "pan_in", state 289, "assert(0)" line 286, "pan_in", state 295, "assert(0)" line 295, "pan_in", state 317, "assert(0)" line 297, "pan_in", state 322, "assert(0)" line 331, "pan_in", state 398, "assert(0)" line 333, "pan_in", state 402, "-end-" (14 of 402 states) unreached in proctype UAS line 362, "pan_in", state 10, "assert(0)" line 393, "pan_in", state 61, "assert(0)" line 394, "pan_in", state 63, "assert(0)" line 395, "pan_in", state 65, "assert(0)" line 397, "pan_in", state 70, "assert(0)" line 445, "pan_in", state 166, "assert(0)" line 446, "pan_in", state 168, "assert(0)" line 478, "pan_in", state 227, "assert(0)" line 501, "pan_in", state 273, "assert(0)" line 502, "pan_in", state 275, "assert(0)" line 503, "pan_in", state 277, "assert(0)" line 523, "pan_in", state 322, "assert(0)" line 525, "pan_in", state 326, "-end-" (13 of 326 states) unreached in proctype :init: (0 of 4 states) pan: elapsed time 1.95e+04 seconds pan: rate 182390.65 states/second pan: avg transition delay 2.6034e-06 usec =========================================================================== ANALYSIS 3: minimized size of reqc (queue for requests from UAC) =========================================================================== pan: resizing hashtable to -w35.. pan: out of memory 1.34444e+11 bytes used 2.74878e+11 bytes more needed 1.37439e+11 bytes limit hint: to reduce memory, recompile with -DMA=216 # better/slower compression, or -DBITSTATE # supertrace, approximation (Spin Version 5.1.3 -- 11 December 2007) Warning: Search not completed + Partial Order Reduction + Compression Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 216 byte, depth reached 21280, errors: 0 1.076e+09 states, stored 1.1801549e+09 states, matched 2.2561549e+09 transitions (= stored+matched) 1 atomic steps hash conflicts: 1.120206e+09 (resolved) Stats on memory usage (in Megabytes): 250381.470 equivalent memory usage for states (stored*(State-vector + overhead)) 0.000 actual memory usage for states (less than 1k) 262144.000 memory used for hash table (-w35) 4.578 memory used for DFS stack (-m100000) 128216.218 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 283147 62155 24005 2 ] unreached in proctype UAC line 111, "pan_in", state 11, "assert(0)" line 120, "pan_in", state 23, "assert(0)" line 126, "pan_in", state 32, "assert(0)" line 157, "pan_in", state 83, "assert(0)" line 177, "pan_in", state 111, "ackc!ack,none" line 177, "pan_in", state 112, "media = flow" line 182, "pan_in", state 122, "assert(0)" line 208, "pan_in", state 166, "assert(0)" line 223, "pan_in", state 188, "assert(0)" line 255, "pan_in", state 237, "assert(0)" line 284, "pan_in", state 289, "assert(0)" line 287, "pan_in", state 295, "assert(0)" line 296, "pan_in", state 317, "assert(0)" line 298, "pan_in", state 322, "assert(0)" line 332, "pan_in", state 398, "assert(0)" line 334, "pan_in", state 402, "-end-" (16 of 402 states) unreached in proctype UAS line 363, "pan_in", state 10, "assert(0)" line 394, "pan_in", state 61, "assert(0)" line 395, "pan_in", state 63, "assert(0)" line 396, "pan_in", state 65, "assert(0)" line 398, "pan_in", state 70, "assert(0)" line 402, "pan_in", state 78, "media = offering" line 403, "pan_in", state 80, "relOut = 1" line 403, "pan_in", state 81, "canSucc = 0" line 415, "pan_in", state 108, "media = offering" line 417, "pan_in", state 113, "media = flow" line 446, "pan_in", state 166, "assert(0)" line 447, "pan_in", state 168, "assert(0)" line 479, "pan_in", state 227, "assert(0)" line 502, "pan_in", state 273, "assert(0)" line 503, "pan_in", state 275, "assert(0)" line 504, "pan_in", state 277, "assert(0)" line 524, "pan_in", state 322, "assert(0)" line 526, "pan_in", state 326, "-end-" (18 of 326 states) unreached in proctype :init: (0 of 4 states) pan: elapsed time 1.46e+04 seconds pan: rate 73659.429 states/second pan: avg transition delay 6.4746e-06 usec ===========================================================================