model: CiRedTriage.tla sha256=157fe1d35304197bbc19ce1c3225cc9353ecdf2c1fe0592557849fa6694fa3a6
CiRedTriage_design cfg_sha256=5f83d191b78d64f4fe7c312550302892c8e2ff7a4bcd677804ed3fea95b9e5f2 out_sha256=e29668ba1c10db518ec1e65fea833724501e0ee54bb661a9db3435de625e4d0f result=PASS
M1_key_head cfg_sha256=f38896270dad5c17f6fa65e86933c3948846b9e3caa3b007ba7436bbdb2f6efe out_sha256=32672f67c34a4f930afe2af7206fe34edb04ab5ff866b86ea58e77d2969f1eb0 result=VIOLATED NoLostRed
M2_key_delivery cfg_sha256=361a418fa2cbb21b50cb9a224fe56f8ce17d0f9078c583a97d9e11dd7e965208 out_sha256=61610b22d35416178d1db2ca7ff3f250f981e636faebc4e92421409fa841f756 result=VIOLATED OneTriagePerIdentity
M3_blind_insert cfg_sha256=b689b1bc2e6aac348c51e71634f6fa0bbaa3941aa5a4bf7ce8d35dd51f07f6b3 out_sha256=ad043e58cd0caa67c43be167392ac0fe5a861ce7e3db240919af30d9bb8261f0 result=VIOLATED OneTriagePerIdentity
M4_volatile_dedup cfg_sha256=41a860e7d9e051b5df827f54dcb4667ba0f84f402fe8d18398ee76f2f90e5c75 out_sha256=75e79c102f1a4dcf8b66bf43c94bbb56865ac8b5fb53f3a10e578d0d828d671f result=VIOLATED OneTriagePerIdentity
M5_ack_before_write cfg_sha256=40ef69558f6ccc014f22e361f7c676709b33d9a7fa40fcb13196fa44c806f4fe out_sha256=0bd9407879ec012376a5b082c9f6cd1dd7e34804593314b3c61ce470eed2c013 result=VIOLATED AckedIsDurable
M6_poll_own_writer cfg_sha256=c17fe44f5769a429187bfddfccb17a1f88273cef069eae2679943b1f70f2e749 out_sha256=2dca55794a1a6690253af266f7d8ad6fa1d64c916d414ff20d55bd5e0290dbe6 result=VIOLATED PollNeverDoubleWrites
M7_no_poll cfg_sha256=ed1ec5415099761b229eb85fc45d8341ea1d4015f4d774ac6fa2d9ad5fe9fe95 out_sha256=0c5202f3d71d6aa6a0453faf193c10561e6c1159f9dfc548782e77c007fa664b result=VIOLATED NoLostRed
M8_upsert_update cfg_sha256=991452e4f8f5d9c832cdc314c9a528c48787b5bd6cbfd2b682aba2aaf599a499 out_sha256=c954815c015c9f082ae94ee05ce61395f4965141008891f647a38bd27f9bd7f2 result=VIOLATED ColumnOwnership
M9_start_from_memory cfg_sha256=f5f9b2b81d719e9a0f82832658c0bfc15ab8c093f5fc1ffe991daaf54ae789df out_sha256=4c29dc2ceaef44d742410811ecdcce820ab34fab9aa3f717626981c4d35790ae result=VIOLATED NoLostStart
M10_receiver_no_dedup cfg_sha256=869b55bfbd614c741de22cf22e85418cccb0e524719ba8d91d89665e9c95138c out_sha256=20d3a8fa0fb90ebf21316da3847403f87f847a394b6db2f065f6829190be5f24 result=VIOLATED OneStartPerIdentity
M11_dead_letter_unrecorded cfg_sha256=3278fbe8fa6e5c57b94964e2349128e68a9e3730d57f01b19df9e95343324ae4 out_sha256=3b2c99b8c36c3c040f43e04b2066b7b34a4520bc48657f6791f19107ca9ecc71 result=VIOLATED AckedIsDurable
