1 2 3 4
\* Direct-TLC check for PER-0020 compaction hot-tier invalidation (safety). \* Run from specs/: java -jar tla2tools.jar -config CompactionModel.cfg CompactionModel.tla SPECIFICATION CompactSpec INVARIANT NeverServesStale