model: CompactionLifecycle.tla sha256=6fe9fd078133ea141f94ea41215b9aa3877c66ed82d9c8a3dc08af4572dc9cee
CompactionLifecycle_design cfg_sha256=fafefd62b7bed61eba2efd38d6b34aabc0b9a5ff24692ef06af6077abe041ecb out_sha256=3528d2948e0c59614baa3a8156e4677cd3269cd6d78b1af1ddfb5afe8ec0a886 result=PASS
CompactionLifecycle_design_live cfg_sha256=7d459409550d5212bf5fe69f2625b7c2d4a2822b6140225e9fba1c0d0291f7ae out_sha256=d39d0734d76f10fa3a130c03ab00044ca91f0a32272b07cc1a9268b9e67a96e1 result=PASS
M1_send_before_activated cfg_sha256=0d2e3654671334eecd92e628317f444b4c17b4c93a91eb38c5a1fce90c0401ee out_sha256=4a85d8997c72f1915d512a1deb90f18d584686720191b6c62bab41497f77b10f result=VIOLATED NoInstallWithoutActivation
M2_last_arrival_wins cfg_sha256=b6dbe214f11e19d31057d587777fedd504dd55f7dbe61392e5fa0858ddeb7167 out_sha256=b830c4f0ec8a8ac5feed183c89b21cc4c565dfb534d34cae5531731728ff8085 result=VIOLATED OneStatePerIdentityUnderAnyArrivalOrder
M3_no_revalidation cfg_sha256=94c17d765ca600e70291e0db754a069d352aa54d9d47d668fb5e315faed18fd1 out_sha256=8ba1a218f39f90e519a6c0e14c348d3b98836b1b437a7e80abd5903f39740dfe result=VIOLATED StaleCandidateNeverInstalled
M4_fallback_by_candidate cfg_sha256=fd0af8f9730b5093a62d10c266961cb65b83123331196338ae19589ca1fe53c4 out_sha256=96e20994109d74d5a6b6de59d0144d3e6f2b8b39ec4901c4a9220add5cef3513 result=VIOLATED FallbackNeverConflictsWithAnotherInvocation
M5_complete_on_send cfg_sha256=f7818622346f43800cfa0abee153130d085f752be278c134945aa075f7fe47ab out_sha256=0e085835e520a67641dc25eb11fc95d4c22c4ed2dc1fa7fb2d59a92b01160dbe result=VIOLATED NoCompleteBeforeInstalled
M6_no_gap_rule cfg_sha256=e49e220cc7ea15eca61548c459ab2761568983287eed0f77a805946e90b15fbf out_sha256=6d9abe5a29d81f677a0b4606667ba3e16873afe77050e7d63f72c27de645b9bb result=VIOLATED EveryActivationResolves
M7_no_barrier cfg_sha256=388b1c32384c53b9fda03bdae3efdb98dd0317a0be92ed0b6b1b490addd061ac out_sha256=e4a34b21fd1785d2d736379042b24ac278f36347a229406513db15013bb36b0f result=VIOLATED NoBuildOverIncompleteSources
