spin -a pulseGen1x1.pml
ltl prop1: ! ([] ((c[0].x[proteinGFP_]==0)))
gcc -DMEMLIM=12288 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000 -a -c0
Pid: 4792
pan:1: acceptance cycle (at depth 310)
Depth= 320 States= 1e+006 Transitions= 4.59e+006 Memory= 390.027 t= 6.49 R= 2e+005
Depth= 320 States= 2e+006 Transitions= 9.96e+006 Memory= 715.613 t= 14.2 R= 1e+005
Depth= 320 States= 3e+006 Transitions= 1.56e+007 Memory= 1041.199 t= 22.2 R= 1e+005
Depth= 323 States= 4e+006 Transitions= 2.16e+007 Memory= 1366.687 t= 30.8 R= 1e+005
Depth= 323 States= 5e+006 Transitions= 2.78e+007 Memory= 1692.273 t= 39.7 R= 1e+005
pan: out of memory
2.10124e+009 bytes used
102400 bytes more needed
1.28849e+010 bytes limit
hint: to reduce memory, recompile with
-DCOLLAPSE # good, fast compression, or
-DMA=672 # better/slower compression, or
-DHC # hash-compaction, approximation
-DBITSTATE # supertrace, approximation
(Spin Version 6.2.5 -- 3 May 2013)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (prop1)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 672 byte, depth reached 323, errors: 2684616
2978585 states, stored (5.95713e+006 visited)
27969153 states, matched
33926282 transitions (= visited+matched)
1.4052565e+008 atomic steps
hash conflicts: 1495812 (resolved)
Stats on memory usage (in Megabytes):
1954.333 equivalent memory usage for states (stored*(State-vector + overhead))
1946.315 actual memory usage for states (compression: 99.59%)
state-vector as stored = 669 byte + 16 byte overhead
64.000 memory used for hash table (-w24)
0.343 memory used for DFS stack (-m10000)
6.780 memory lost to fragmentation
2003.894 total actual memory usage
pan: elapsed time 48.6 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
]]>