tool: source=https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar sha1=2b8c20402dc740fed5b03f9d39f652e85d70b17c sha256=ab4694601923fd5ac06452abbf847c366a5054a3d739552085edd6ed986c29ec
model: DurableEvidenceDelivery.tla sha256=afaa9e4c450deb4fc50f7733c525531a0cbc5090ffbb050a5dc3530372396023
DurableEvidenceDelivery_design cfg_sha256=e69d32d0e9feece240781e89bda358681b3c39e0b64e9b727cf541ab00aa5318 result=PASS
M1_no_off_host_intent cfg_sha256=cfa9ada6979260248b2a1c89dded4e3dbab8d2482f8d8c5b7983ed47467e21fe result=VIOLATED DispatchUsesRecordedIntent
M2_dispatch_stale_intent cfg_sha256=e9ec005d567c14ccc84bb940573150093584d8c9ca76aa4f586b633462a5ed6d result=VIOLATED DispatchUsesExactCurrentIntent
M2_admit_unconfirmed cfg_sha256=e6f3024d3009977ad0759fedb5992ccd49e4ca898501ff9b901c1bc757671449 result=VIOLATED NoAdmissionWithoutConfirmation
M3_nonidempotent_confirmation cfg_sha256=90e275ab42109c9c6bf49afb6e4826754283fcb7ee5411e6558492f13db983a6 result=VIOLATED OneLogicalAttemptPerExecution
M4_admit_stale_revision cfg_sha256=dec889ade5d9375e2ea2487d7bc193fd315a2836d12280cb6bced46dbe6b5ef8 result=VIOLATED NoStaleRevisionAdmission
M5_cleanup_drops_history cfg_sha256=d6fa6a4a3216a22898b9c3831639a183a1838cd4b70de62bc00f68670bdc8d98 result=VIOLATED RecordedEvidenceIsRetained
M6_admit_older_pass cfg_sha256=5104001fe20925c812f2604bd997307ce2efe5e2a07b786508abe0abd9fe69d6 result=VIOLATED HighestAllocatedAttemptSelected
M7_lost_unconfirmed_pass cfg_sha256=ce0d1f3ed0db3920da2f29319b4fe69494c116c3644004b858ceb4af04f94dd3 result=VIOLATED LostUnconfirmedPassIsUnresolved
M8_dispatch_foreign_subject cfg_sha256=e8b12f844ac9b34ddb023821ac8b504a9788d3ce4aca4735275c310dbfa81917 result=VIOLATED DispatchUsesExactSubjectIntent
