a normal content info with the same timestamp.
2. Added another invariant to check if GetContentInfo returns only the latest content.
3. Added a few TODOs
2. Added no-op time ticks back. Reasoing - Consider the scenario where there is just one snapshot which writes a few contents and stays in pending state for some time (says x seconds) until it reaches its
MaxSnapshotTime. During these x seconds, no GC process can garbage collect the contents written by the partial snapshot. However, the contents might get garbage collected once those x seconds are over. So, consider that there is a GC process that starts after these x seconds have passed and then garbage collects the contents. But in the TLA+ spec, the timestamp will tick only if some tangible step
occurs - some contents are written/ flushed, a snapshot is deleted, a GC is started, etc. Avoiding no-op time ticks prevents the spec from capturing the scenario explained.
And hence, I am reverting the change of avoiding no-op time ticks. Maybe we can revisit the issue of no-op ticks later, if needed.
2. Added GC steps. Need to test, the state space is exploding after adding the 3 possible GC processing steps.
3. Added 2 TODOs -
One for GetContentInfo
One for TriggerGC
1. Removed blobs (re-include if later it becomes necessary to specify blob compaction)
2. Used bags for index_blobs and snapshots to reduce state space.
3. Added a global time ticker, instead of the complicated method of "possible" incremeting timer while flushing.
4. Added a status flag to the snapshot record.
5. Snapshot were filled with the contents they are to write while triggering. Changed that to choose any contents before snapshot completion.
This saves the state space - an incomplete snapshot (i.e., only part of intended contents written before MaxSnapshotTime) is same as another
incomplete snapshot that wrote the same contents but had a larger set of intended contents to be written.
