mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
28 lines
810 B
Plaintext
28 lines
810 B
Plaintext
----------- MODULE MultiChannelIdentityCollisionHarness_BadDisplayNameUnifies -----------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* Negative model:
|
|
* BUG: identities are unified based on a non-unique display identifier across
|
|
* platforms, effectively ignoring the LinkExists constraint.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
LinkExists
|
|
|
|
ASSUME
|
|
LinkExists \in BOOLEAN
|
|
|
|
\* BUG: collapse allowed regardless of explicit link
|
|
CollapseAllowed == TRUE
|
|
|
|
Inv_NoCrossPlatformCollapseWithoutLink ==
|
|
(~LinkExists) => ~CollapseAllowed
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|