mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
40 lines
1.2 KiB
Plaintext
40 lines
1.2 KiB
Plaintext
------------------ MODULE RoutingTriRuleHarness_BadThreadUsesThreadScope ------------------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* Negative model:
|
|
* BUG: thread messages use the thread channel scope instead of parent scope.
|
|
* This can accidentally allow collapses when parent intended per-peer.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
GlobalScope,
|
|
ParentScope,
|
|
ThreadScope,
|
|
HasIdentityLink
|
|
|
|
ASSUME
|
|
/\ GlobalScope \in {"main","per-peer"}
|
|
/\ ParentScope \in {"main","per-peer"}
|
|
/\ ThreadScope \in {"main","per-peer"}
|
|
/\ HasIdentityLink \in BOOLEAN
|
|
|
|
\* BUG: thread-parent binding ignored
|
|
BindScope(isThread) == ThreadScope
|
|
|
|
EffectiveScope(isThread) == BindScope(isThread)
|
|
|
|
CollapseAllowed(isThread) == (EffectiveScope(isThread) = "main") /\ HasIdentityLink
|
|
|
|
Inv_ThreadUsesParent == EffectiveScope(TRUE) = ParentScope
|
|
|
|
Inv_NoCollapseWhenParentPerPeer ==
|
|
(ParentScope = "per-peer") => ~CollapseAllowed(TRUE)
|
|
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|