mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
33 lines
952 B
INI
33 lines
952 B
INI
|
\* TLC model-check config for the draft MultiTenantRelay model.
|
||
|
|
\* Run:
|
||
|
|
\* java -cp ~/.buzz/.scratch/tla2tools.jar tlc2.TLC -config MultiTenantRelay.cfg MultiTenantRelay.tla
|
||
|
|
SPECIFICATION Spec
|
||
|
|
|
||
|
|
CONSTANTS
|
||
|
|
Communities = {commA, commB}
|
||
|
|
Channels = {chanA1, chanA2, chanB1, chanB2, chanFresh}
|
||
|
|
Hosts = {hostA, hostB, hostBad}
|
||
|
|
Actors = {alice}
|
||
|
|
Workers = {relay1}
|
||
|
|
MsgIds = {msg1}
|
||
|
|
AuditVals = {audit0, audit1}
|
||
|
|
CommA = commA
|
||
|
|
CommB = commB
|
||
|
|
ChanA1 = chanA1
|
||
|
|
ChanA2 = chanA2
|
||
|
|
ChanB1 = chanB1
|
||
|
|
ChanB2 = chanB2
|
||
|
|
ChanFresh = chanFresh
|
||
|
|
HostA = hostA
|
||
|
|
HostB = hostB
|
||
|
|
HostBad = hostBad
|
||
|
|
NoChannel = noChannel
|
||
|
|
NoCommunity = noCommunity
|
||
|
|
OpenCommunities = {commA}
|
||
|
|
SanitizedErrors = {"auth-required", "restricted", "invalid", "duplicate", "pow", "rate-limited", "blocked", "error", "frame-too-large"}
|
||
|
|
|
||
|
|
INVARIANT Safety
|
||
|
|
CONSTRAINT BoundedObservations
|
||
|
|
CONSTRAINT BoundedWitnesses
|
||
|
|
SYMMETRY Symmetry
|