The 3 GB can probably be attributed to the set of fingerprints (of explored states). Try increasing the memory allocated to TLC on the TLC Options page of the Toolbox.
There are countless optimizations to make model-checking faster. My feeling is that the proposed optimization doesn’t justify the effort. That said, efficient state-graph serialization alone would be useful infrastructure for other features. Thus, I’m happy to advise anybody who wants to do the heavy lifting.
Markus
I see. I just ran a 3-hour-long verification and Storage says 3 GB. I assume this is mostly due to the fingerprint graph then?
Do you think it'd be useful to check properties while avoid rerunning the state-space exploration?