mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
39 lines
1.1 KiB
Plaintext
39 lines
1.1 KiB
Plaintext
----------- MODULE RoutingThreadParentChannelOverrideHarness -----------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* RoutingThreadParentChannelOverrideHarness.tla
|
|
*
|
|
* Correctness model:
|
|
* - Discord thread messages should inherit the *parent channel* routing policy
|
|
* (dm scope / channel overrides), not the thread channel's own config.
|
|
*
|
|
* This is a tiny conformance-style harness that isolates just that rule.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
GlobalDmScope,
|
|
ParentDmScope,
|
|
ThreadDmScope
|
|
|
|
ASSUME
|
|
/\ GlobalDmScope \in {"main","per-peer"}
|
|
/\ ParentDmScope \in {"main","per-peer"}
|
|
/\ ThreadDmScope \in {"main","per-peer"}
|
|
|
|
\* Which channel's scope config should apply
|
|
EffectiveScope(isThread) ==
|
|
IF isThread
|
|
THEN ParentDmScope
|
|
ELSE ThreadDmScope
|
|
|
|
Inv_ThreadInheritsParent == EffectiveScope(TRUE) = ParentDmScope
|
|
|
|
\* Trivial Spec for TLC
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|