mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-25 06:14:59 +00:00
37 lines
857 B
INI
37 lines
857 B
INI
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
|