cls
9dfa06ffee
Docker image / Build (linux/amd64) (push) Has been cancelled
Docker image / Build (linux/arm64) (push) Has been cancelled
Docker image / Merge release multi-arch manifest (push) Has been cancelled
Docker image / Merge debug multi-arch manifest (push) Has been cancelled
Docker image / Build public push gateway (linux/amd64) (push) Has been cancelled
Docker image / Build public push gateway (linux/arm64) (push) Has been cancelled
Docker image / Publish public push gateway image (push) Has been cancelled
Sprig image / Build (linux/amd64) (push) Has been cancelled
Sprig image / Build (linux/arm64) (push) Has been cancelled
Sprig image / Merge multi-arch manifest (push) Has been cancelled
Harbor Buzz Orchestra / Python tests and lint (push) Has been cancelled
CI / Detect Changed Paths (push) Has been cancelled
CI / Rust Lint (push) Has been cancelled
CI / Unit Tests (push) Has been cancelled
CI / Desktop Core (push) Has been cancelled
CI / Desktop Smoke E2E (1) (push) Has been cancelled
CI / Desktop Smoke E2E (2) (push) Has been cancelled
CI / Desktop Smoke E2E (3) (push) Has been cancelled
CI / Desktop Smoke E2E (4) (push) Has been cancelled
CI / Desktop (push) Has been cancelled
CI / Desktop E2E Relay (push) Has been cancelled
CI / Desktop E2E Integration (1/2) (push) Has been cancelled
CI / Desktop E2E Integration (2/2) (push) Has been cancelled
CI / Desktop E2E Integration (push) Has been cancelled
CI / Backend Integration (relay e2e) (push) Has been cancelled
CI / Relay E2E (push) Has been cancelled
CI / Web (push) Has been cancelled
CI / Mobile (push) Has been cancelled
CI / Security (push) Has been cancelled
CI / Dead Token Reference Guard (push) Has been cancelled
CI / Server Cross-Compile (aarch64-unknown-linux-musl) (push) Has been cancelled
CI / Server Cross-Compile (x86_64-unknown-linux-musl) (push) Has been cancelled
CI / Windows Rust (x86_64-pc-windows-msvc) (push) Has been cancelled
CI / Desktop Build (macOS) (push) Has been cancelled
helm chart / lint + unittest + render matrix (push) Has been cancelled
helm chart / install on kind (gated) (push) Has been cancelled
helm chart / publish chart to GHCR (push) Has been cancelled
Mesh Lifecycle / Relay-Driven Mesh Lifecycle Smoke (push) Has been cancelled
Sprig / Build (aarch64-unknown-linux-musl) (push) Has been cancelled
Sprig / Build (x86_64-unknown-linux-musl) (push) Has been cancelled
Sprig / Publish rolling release (push) Has been cancelled
Sprig / Publish tagged release (push) Has been cancelled
Signed-off-by: cls_宁波本机 <908705107@qq.com>
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
|