mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
33 lines
997 B
Plaintext
33 lines
997 B
Plaintext
------------------------------ MODULE ToolGroupExpansion ------------------------------
|
|
EXTENDS Naturals, FiniteSets
|
|
|
|
(******************************************************************************
|
|
* ToolGroupExpansion.tla
|
|
*
|
|
* Conformance/security check: tool groups expand to specific tool sets.
|
|
*
|
|
* We treat tool ids as *strings* (TLC model values). This avoids confusion
|
|
* between TLA+ identifiers and model values.
|
|
******************************************************************************)
|
|
|
|
CONSTANTS
|
|
Tools, \* SUBSET STRING
|
|
GroupMemory \* SUBSET Tools (implementation's expansion of group:memory)
|
|
|
|
ASSUME
|
|
/\ Tools /= {}
|
|
/\ GroupMemory \subseteq Tools
|
|
|
|
MemorySearch == "memory_search"
|
|
MemoryGet == "memory_get"
|
|
|
|
Inv_GroupMemoryExact == GroupMemory = {MemorySearch, MemoryGet}
|
|
|
|
\* Trivial TLC behavior
|
|
VARIABLE dummy
|
|
Init == dummy = 0
|
|
Next == dummy' = dummy
|
|
Spec == Init /\ [][Next]_<<dummy>>
|
|
|
|
=============================================================================
|