Basic Model*   Trans Model    FIFO Model

lines of reachable code            423           368           330

state vector (bytes)               224           112            96

depth reached                 > 23,238         2,233         1,295

state transitions      > 7,476,737,400    30,970,738    15,728,760

memory usage (Mbytes)        > 128,217          1031           477

elapsed time (seconds)        > 19,800           128            62

----------
*The basic model cannot be model-checked in 128 Gbytes of memory.  This is
why most of the numbers in this column are lower bounds.