SPECIFICATION Spec

CONSTANTS
    Users = {u1, u2, u3}
    Tenants = {t1, t2}
    Webhooks = {wh1, wh2, wh3}
    OAuthApps = {app1, app2}
    APIKeys = {key1, key2, key3}
    EventTypes = {event1, event2, event3}
    MaxWebhooksPerTenant = 2
    MaxKeysPerUser = 2
    RateLimitPerHour = 100

INVARIANTS
    TypeOK
    AdminOnlyIntegrationManagement
    WebhookTenantLimit
    APIKeyUserLimit
    RateLimitEnforcement
    WebhookTenantIsolation
    OAuthAppTenantIsolation
    APIKeyTenantIsolation
    TokenTenantConsistency
    ActiveDeliveriesQueued

PROPERTIES
    EventualDeliveryCompletion
    EventualRetryOrFail
    EventualExpiration

\* Constraint to limit state space for model checking
CONSTRAINT
    /\ Len(integrationAuditLog) <= 15
    /\ Len(webhookQueue) <= 5
    /\ Cardinality(webhookDeliveries) <= 6
    /\ Cardinality(oauthTokens) <= 4