mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-30 00:34:56 +00:00
Add TLA+ specifications for future functionality (workflows, collaboration, integrations)
Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot]
142
spec/README.md
142
spec/README.md
@@ -4,17 +4,23 @@ This directory contains the formal TLA+ specification for the MetaBuilder system
|
||||
|
||||
## Overview
|
||||
|
||||
The specification models the core invariants and behaviors of MetaBuilder, including:
|
||||
The specification models both current and future MetaBuilder functionality through multiple TLA+ modules:
|
||||
|
||||
**Core System Specifications:**
|
||||
- **6-Level Permission System**: Hierarchical access control (Public → User → Moderator → Admin → God → Supergod)
|
||||
- **Multi-Tenant Data Isolation**: Strict separation of data between tenants
|
||||
- **Database Abstraction Layer (DBAL)**: Query processing with security guarantees
|
||||
- **Package Management**: Installation, enabling, and disabling of feature packages
|
||||
- **Audit Logging**: Complete tracking of privileged operations
|
||||
|
||||
**Future Functionality Specifications:**
|
||||
- **Workflow System**: Workflow execution, scheduling, and state management
|
||||
- **Real-Time Collaboration**: Concurrent editing, presence, comments, and mentions
|
||||
- **Integration Ecosystem**: Webhooks, OAuth apps, API keys, and rate limiting
|
||||
|
||||
## Files
|
||||
|
||||
### `metabuilder.tla`
|
||||
### Core System: `metabuilder.tla`
|
||||
|
||||
The main TLA+ specification file that defines:
|
||||
|
||||
@@ -42,6 +48,86 @@ Configuration file for the TLC model checker that specifies:
|
||||
- Temporal properties to verify
|
||||
- State space constraints for bounded model checking
|
||||
|
||||
### Future Functionality: `workflow_system.tla`
|
||||
|
||||
Specification for advanced workflow execution features:
|
||||
|
||||
- **Template Management**: God-level users create and manage workflow templates
|
||||
- **Workflow Execution**: Admin-level users trigger manual or scheduled workflows
|
||||
- **Step Dependencies**: Define and enforce execution order constraints
|
||||
- **Error Handling**: Automatic retry logic with configurable limits
|
||||
- **Concurrency Control**: Limit concurrent workflow executions per tenant
|
||||
- **Safety Properties**:
|
||||
- `GodOnlyTemplateCreation`: Only Level 5+ users can author workflows
|
||||
- `AdminOnlyExecution`: Only Level 4+ users can execute workflows
|
||||
- `TenantIsolation`: Workflows are strictly isolated by tenant
|
||||
- `ConcurrencyLimit`: Per-tenant concurrent execution limits
|
||||
- `RetryLimit`: Failed steps don't exceed retry threshold
|
||||
- `DependencyEnforcement`: Steps execute only after dependencies complete
|
||||
- **Liveness Properties**:
|
||||
- `EventualStepExecution`: Pending steps eventually execute
|
||||
- `EventualCompletion`: Running workflows eventually complete or fail
|
||||
- `EventualScheduleTrigger`: Scheduled workflows eventually trigger
|
||||
|
||||
### `workflow_system.cfg`
|
||||
|
||||
Configuration for workflow system model checking with workflow templates, steps, and execution limits.
|
||||
|
||||
### Future Functionality: `collaboration.tla`
|
||||
|
||||
Specification for real-time collaboration features:
|
||||
|
||||
- **Session Management**: User connection, idle, and disconnection states
|
||||
- **Concurrent Editing**: Multiple users editing documents simultaneously
|
||||
- **Comments and Mentions**: Users can comment and mention others in documents
|
||||
- **Presence Tracking**: Real-time user online/idle/offline status
|
||||
- **Notifications**: Mention notifications with read status tracking
|
||||
- **Version History**: Document snapshot creation and tracking
|
||||
- **Safety Properties**:
|
||||
- `DocumentTenantIsolation`: Editors can only access documents in their tenant
|
||||
- `ConcurrentEditorLimit`: Maximum concurrent editors per document
|
||||
- `CommentTenantConsistency`: Comments belong to document's tenant
|
||||
- `MentionTenantIsolation`: Mentions stay within tenant boundaries
|
||||
- `NotificationLimit`: Pending notifications don't exceed limits
|
||||
- `DisconnectedNotEditing`: Disconnected users automatically stop editing
|
||||
- `OperationAuthorship`: All operations come from authorized editors
|
||||
- **Liveness Properties**:
|
||||
- `EventualNotificationHandling`: Notifications eventually get read or cleared
|
||||
- `EventualMentionRead`: Mentioned users eventually see their mentions
|
||||
- `EventualStopEditing`: Active editors eventually stop or disconnect
|
||||
|
||||
### `collaboration.cfg`
|
||||
|
||||
Configuration for collaboration model checking with documents, comments, and concurrent editors.
|
||||
|
||||
### Future Functionality: `integrations.tla`
|
||||
|
||||
Specification for integration ecosystem:
|
||||
|
||||
- **Webhook Management**: Create, configure, and manage webhooks for events
|
||||
- **OAuth Applications**: OAuth app lifecycle and token management
|
||||
- **API Key Management**: User-level API key creation and expiration
|
||||
- **Event Subscriptions**: Subscribe to and filter system events
|
||||
- **Rate Limiting**: Track and enforce API call rate limits per identity
|
||||
- **Delivery Guarantees**: Webhook delivery with retry logic
|
||||
- **Safety Properties**:
|
||||
- `AdminOnlyIntegrationManagement`: Only Level 4+ users manage integrations
|
||||
- `WebhookTenantLimit`: Webhooks per tenant don't exceed limits
|
||||
- `APIKeyUserLimit`: API keys per user don't exceed limits
|
||||
- `RateLimitEnforcement`: API calls respect rate limits
|
||||
- `WebhookTenantIsolation`: Webhooks isolated by tenant
|
||||
- `OAuthAppTenantIsolation`: OAuth apps isolated by tenant
|
||||
- `TokenTenantConsistency`: OAuth tokens match app tenants
|
||||
- `ActiveDeliveriesQueued`: Active deliveries are properly queued
|
||||
- **Liveness Properties**:
|
||||
- `EventualDeliveryCompletion`: Webhook deliveries eventually complete or fail
|
||||
- `EventualRetryOrFail`: Failed deliveries retry or permanently fail
|
||||
- `EventualExpiration`: Expired API keys eventually marked as expired
|
||||
|
||||
### `integrations.cfg`
|
||||
|
||||
Configuration for integration ecosystem model checking with webhooks, OAuth apps, and API keys.
|
||||
|
||||
## Key Concepts
|
||||
|
||||
### Permission Levels
|
||||
@@ -215,6 +301,58 @@ This specification aligns with the MetaBuilder architecture documentation:
|
||||
- `docs/architecture/data/data-driven-architecture.md` → Package system
|
||||
- `dbal/README.md` → DBAL state machine and security model
|
||||
- `README.md` → Multi-tenant system
|
||||
- `docs/todo/improvements/20-FUTURE-FEATURES-TODO.md` → Future features specifications
|
||||
|
||||
## Modeling Future Features
|
||||
|
||||
The TLA+ specifications for future features serve multiple purposes:
|
||||
|
||||
### 1. Design Validation
|
||||
Before implementing complex features like workflows or real-time collaboration, the formal specifications help:
|
||||
- Identify potential race conditions and deadlocks
|
||||
- Verify that permission enforcement is complete
|
||||
- Ensure multi-tenant isolation is maintained
|
||||
- Validate concurrency control mechanisms
|
||||
|
||||
### 2. API Contract Definition
|
||||
The specifications define precise contracts for:
|
||||
- **Workflow System**: Template creation, execution triggers, step dependencies
|
||||
- **Collaboration**: Session management, concurrent editing, notification delivery
|
||||
- **Integrations**: Webhook delivery guarantees, OAuth token lifecycle, rate limiting
|
||||
|
||||
### 3. Implementation Guide
|
||||
Each specification provides:
|
||||
- Clear state transitions for the system to implement
|
||||
- Invariants that must be maintained by the implementation
|
||||
- Temporal properties describing expected system behavior
|
||||
- Edge cases that must be handled (retries, failures, disconnections)
|
||||
|
||||
### 4. Testing Blueprint
|
||||
The specifications can guide:
|
||||
- Property-based testing strategies
|
||||
- Concurrency test scenarios
|
||||
- Multi-tenant isolation test cases
|
||||
- Load testing parameters (rate limits, concurrent users)
|
||||
|
||||
### Running Future Feature Specs
|
||||
|
||||
Model check individual future features:
|
||||
|
||||
```bash
|
||||
# Check workflow system
|
||||
java -cp tla2tools.jar tlc2.TLC spec/workflow_system.tla -config spec/workflow_system.cfg
|
||||
|
||||
# Check collaboration system
|
||||
java -cp tla2tools.jar tlc2.TLC spec/collaboration.tla -config spec/collaboration.cfg
|
||||
|
||||
# Check integrations system
|
||||
java -cp tla2tools.jar tlc2.TLC spec/integrations.tla -config spec/integrations.cfg
|
||||
```
|
||||
|
||||
Each specification is standalone and can be verified independently. This modular approach allows:
|
||||
- Parallel verification of different subsystems
|
||||
- Incremental feature development
|
||||
- Focused debugging when invariants are violated
|
||||
|
||||
## References
|
||||
|
||||
|
||||
32
spec/collaboration.cfg
Normal file
32
spec/collaboration.cfg
Normal file
@@ -0,0 +1,32 @@
|
||||
SPECIFICATION Spec
|
||||
|
||||
CONSTANTS
|
||||
Users = {u1, u2, u3}
|
||||
Tenants = {t1, t2}
|
||||
Documents = {doc1, doc2}
|
||||
MaxConcurrentEditors = 3
|
||||
MaxNotifications = 10
|
||||
|
||||
INVARIANTS
|
||||
TypeOK
|
||||
DocumentTenantIsolation
|
||||
ConcurrentEditorLimit
|
||||
CommentTenantConsistency
|
||||
MentionTenantIsolation
|
||||
NotificationLimit
|
||||
ActiveEditorsOnly
|
||||
DisconnectedNotEditing
|
||||
OperationAuthorship
|
||||
VersionConsistency
|
||||
|
||||
PROPERTIES
|
||||
EventualNotificationHandling
|
||||
EventualMentionRead
|
||||
EventualStopEditing
|
||||
|
||||
\* Constraint to limit state space for model checking
|
||||
CONSTRAINT
|
||||
/\ Cardinality(comments) <= 5
|
||||
/\ Cardinality(mentions) <= 5
|
||||
/\ \A u \in Users: Len(notifications[u]) <= 8
|
||||
/\ \A t \in Tenants: Len(activityFeed[t]) <= 12
|
||||
542
spec/collaboration.tla
Normal file
542
spec/collaboration.tla
Normal file
@@ -0,0 +1,542 @@
|
||||
---------------------------- MODULE collaboration ----------------------------
|
||||
(***************************************************************************
|
||||
* Real-Time Collaboration Specification for MetaBuilder *
|
||||
* *
|
||||
* This specification models real-time collaboration features including: *
|
||||
* - Concurrent document editing with operational transformation *
|
||||
* - User presence and activity tracking *
|
||||
* - Commenting and mentioning system *
|
||||
* - Activity feeds and notifications *
|
||||
* - Conflict detection and resolution *
|
||||
* - Session management and connection handling *
|
||||
***************************************************************************)
|
||||
|
||||
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
||||
|
||||
CONSTANTS
|
||||
Users, \* Set of all users
|
||||
Tenants, \* Set of tenants
|
||||
Documents, \* Set of documents
|
||||
MaxConcurrentEditors, \* Maximum concurrent editors per document
|
||||
MaxNotifications \* Maximum pending notifications per user
|
||||
|
||||
VARIABLES
|
||||
userTenants, \* User -> Tenant
|
||||
userSessions, \* User -> Session state {active, idle, disconnected}
|
||||
documentOwners, \* Document -> User (owner)
|
||||
documentTenants, \* Document -> Tenant
|
||||
documentContent, \* Document -> Sequence of operations
|
||||
documentEditors, \* Document -> Set of Users (currently editing)
|
||||
userPresence, \* User -> {online, idle, offline}
|
||||
comments, \* Set of comment records
|
||||
mentions, \* Set of mention records
|
||||
notifications, \* User -> Sequence of notifications
|
||||
activityFeed, \* Tenant -> Sequence of activities
|
||||
versionHistory \* Document -> Sequence of versions
|
||||
|
||||
vars == <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, comments,
|
||||
mentions, notifications, activityFeed, versionHistory>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Type Definitions *)
|
||||
|
||||
SessionState == {"active", "idle", "disconnected"}
|
||||
PresenceState == {"online", "idle", "offline"}
|
||||
OperationType == {"insert", "delete", "replace", "format"}
|
||||
|
||||
Operation == [
|
||||
type: OperationType,
|
||||
position: Nat,
|
||||
content: STRING,
|
||||
user: Users,
|
||||
timestamp: Nat
|
||||
]
|
||||
|
||||
Comment == [
|
||||
id: Nat,
|
||||
documentId: Documents,
|
||||
userId: Users,
|
||||
tenantId: Tenants,
|
||||
content: STRING,
|
||||
position: Nat,
|
||||
timestamp: Nat,
|
||||
resolved: BOOLEAN
|
||||
]
|
||||
|
||||
Mention == [
|
||||
id: Nat,
|
||||
commentId: Nat,
|
||||
mentionedUser: Users,
|
||||
mentioningUser: Users,
|
||||
tenantId: Tenants,
|
||||
timestamp: Nat,
|
||||
read: BOOLEAN
|
||||
]
|
||||
|
||||
Notification == [
|
||||
id: Nat,
|
||||
userId: Users,
|
||||
type: STRING,
|
||||
sourceId: Nat,
|
||||
message: STRING,
|
||||
timestamp: Nat,
|
||||
read: BOOLEAN
|
||||
]
|
||||
|
||||
Activity == [
|
||||
userId: Users,
|
||||
tenantId: Tenants,
|
||||
action: STRING,
|
||||
targetId: Nat,
|
||||
timestamp: Nat
|
||||
]
|
||||
|
||||
Version == [
|
||||
documentId: Documents,
|
||||
content: Seq(Operation),
|
||||
createdBy: Users,
|
||||
timestamp: Nat,
|
||||
versionNumber: Nat
|
||||
]
|
||||
|
||||
TypeOK ==
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ userSessions \in [Users -> SessionState]
|
||||
/\ documentOwners \in [Documents -> Users]
|
||||
/\ documentTenants \in [Documents -> Tenants]
|
||||
/\ documentContent \in [Documents -> Seq(Operation)]
|
||||
/\ documentEditors \in [Documents -> SUBSET Users]
|
||||
/\ userPresence \in [Users -> PresenceState]
|
||||
/\ comments \subseteq Comment
|
||||
/\ mentions \subseteq Mention
|
||||
/\ notifications \in [Users -> Seq(Notification)]
|
||||
/\ activityFeed \in [Tenants -> Seq(Activity)]
|
||||
/\ versionHistory \in [Documents -> Seq(Version)]
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Permission Checks *)
|
||||
|
||||
\* User can access document if in same tenant
|
||||
CanAccessDocument(user, doc) ==
|
||||
userTenants[user] = documentTenants[doc]
|
||||
|
||||
\* User can edit if they can access and not too many concurrent editors
|
||||
CanEditDocument(user, doc) ==
|
||||
/\ CanAccessDocument(user, doc)
|
||||
/\ Cardinality(documentEditors[doc]) < MaxConcurrentEditors
|
||||
|
||||
\* User can comment if they can access
|
||||
CanComment(user, doc) ==
|
||||
CanAccessDocument(user, doc)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Helper Functions *)
|
||||
|
||||
\* Count pending notifications for a user
|
||||
CountPendingNotifications(user) ==
|
||||
LET unread == {n \in 1..Len(notifications[user]) :
|
||||
~notifications[user][n].read}
|
||||
IN Cardinality(unread)
|
||||
|
||||
\* Get comment by ID
|
||||
GetComment(cid) ==
|
||||
CHOOSE c \in comments : c.id = cid
|
||||
|
||||
\* Check if user is mentioned in a comment
|
||||
IsMentioned(user, comment) ==
|
||||
\E m \in mentions :
|
||||
/\ m.commentId = comment.id
|
||||
/\ m.mentionedUser = user
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Initial State *)
|
||||
|
||||
Init ==
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ userSessions = [u \in Users |-> "disconnected"]
|
||||
/\ documentOwners \in [Documents -> Users]
|
||||
/\ documentTenants \in [Documents -> Tenants]
|
||||
/\ documentContent = [d \in Documents |-> <<>>]
|
||||
/\ documentEditors = [d \in Documents |-> {}]
|
||||
/\ userPresence = [u \in Users |-> "offline"]
|
||||
/\ comments = {}
|
||||
/\ mentions = {}
|
||||
/\ notifications = [u \in Users |-> <<>>]
|
||||
/\ activityFeed = [t \in Tenants |-> <<>>]
|
||||
/\ versionHistory = [d \in Documents |-> <<>>]
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Session Management *)
|
||||
|
||||
\* User connects and becomes active
|
||||
UserConnect(user) ==
|
||||
/\ userSessions[user] = "disconnected"
|
||||
/\ userSessions' = [userSessions EXCEPT ![user] = "active"]
|
||||
/\ userPresence' = [userPresence EXCEPT ![user] = "online"]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "connected",
|
||||
targetId |-> 0,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, documentOwners, documentTenants, documentContent,
|
||||
documentEditors, comments, mentions, notifications, versionHistory>>
|
||||
|
||||
\* User becomes idle
|
||||
UserGoIdle(user) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ userSessions' = [userSessions EXCEPT ![user] = "idle"]
|
||||
/\ userPresence' = [userPresence EXCEPT ![user] = "idle"]
|
||||
/\ UNCHANGED <<userTenants, documentOwners, documentTenants, documentContent,
|
||||
documentEditors, comments, mentions, notifications,
|
||||
activityFeed, versionHistory>>
|
||||
|
||||
\* User disconnects
|
||||
UserDisconnect(user) ==
|
||||
/\ userSessions[user] \in {"active", "idle"}
|
||||
/\ userSessions' = [userSessions EXCEPT ![user] = "disconnected"]
|
||||
/\ userPresence' = [userPresence EXCEPT ![user] = "offline"]
|
||||
/\ documentEditors' = [d \in Documents |->
|
||||
IF user \in documentEditors[d]
|
||||
THEN documentEditors[d] \ {user}
|
||||
ELSE documentEditors[d]]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "disconnected",
|
||||
targetId |-> 0,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, documentOwners, documentTenants, documentContent,
|
||||
comments, mentions, notifications, versionHistory>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Document Editing *)
|
||||
|
||||
\* User starts editing a document
|
||||
StartEditing(user, doc) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ CanEditDocument(user, doc)
|
||||
/\ user \notin documentEditors[doc]
|
||||
/\ documentEditors' = [documentEditors EXCEPT ![doc] = @ \cup {user}]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "start_editing",
|
||||
targetId |-> doc,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, userPresence, comments, mentions,
|
||||
notifications, versionHistory>>
|
||||
|
||||
\* User stops editing a document
|
||||
StopEditing(user, doc) ==
|
||||
/\ user \in documentEditors[doc]
|
||||
/\ documentEditors' = [documentEditors EXCEPT ![doc] = @ \ {user}]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "stop_editing",
|
||||
targetId |-> doc,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, userPresence, comments, mentions,
|
||||
notifications, versionHistory>>
|
||||
|
||||
\* User applies an operation to a document
|
||||
ApplyOperation(user, doc, op) ==
|
||||
/\ user \in documentEditors[doc]
|
||||
/\ userSessions[user] = "active"
|
||||
/\ CanAccessDocument(user, doc)
|
||||
/\ op.user = user
|
||||
/\ op.type \in OperationType
|
||||
/\ documentContent' = [documentContent EXCEPT
|
||||
![doc] = Append(@, op)]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "edit_document",
|
||||
targetId |-> doc,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentEditors, userPresence, comments, mentions,
|
||||
notifications, versionHistory>>
|
||||
|
||||
\* Create a version snapshot
|
||||
CreateVersion(user, doc) ==
|
||||
/\ user = documentOwners[doc]
|
||||
/\ CanAccessDocument(user, doc)
|
||||
/\ LET
|
||||
versionNum == Len(versionHistory[doc]) + 1
|
||||
newVersion == [
|
||||
documentId |-> doc,
|
||||
content |-> documentContent[doc],
|
||||
createdBy |-> user,
|
||||
timestamp |-> versionNum,
|
||||
versionNumber |-> versionNum
|
||||
]
|
||||
IN
|
||||
/\ versionHistory' = [versionHistory EXCEPT
|
||||
![doc] = Append(@, newVersion)]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "create_version",
|
||||
targetId |-> doc,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]])
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, comments,
|
||||
mentions, notifications>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Comments and Mentions *)
|
||||
|
||||
\* User adds a comment
|
||||
AddComment(user, doc, cid, content, position) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ CanComment(user, doc)
|
||||
/\ cid \notin {c.id : c \in comments}
|
||||
/\ LET newComment == [
|
||||
id |-> cid,
|
||||
documentId |-> doc,
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
content |-> content,
|
||||
position |-> position,
|
||||
timestamp |-> Len(activityFeed[userTenants[user]]),
|
||||
resolved |-> FALSE
|
||||
] IN
|
||||
/\ comments' = comments \cup {newComment}
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "add_comment",
|
||||
targetId |-> cid,
|
||||
timestamp |-> Len(@)
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, mentions,
|
||||
notifications, versionHistory>>
|
||||
|
||||
\* User mentions another user in a comment
|
||||
MentionUser(user, mentionedUser, cid, mid) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ \E c \in comments : c.id = cid /\ c.userId = user
|
||||
/\ userTenants[user] = userTenants[mentionedUser]
|
||||
/\ mid \notin {m.id : m \in mentions}
|
||||
/\ CountPendingNotifications(mentionedUser) < MaxNotifications
|
||||
/\ LET
|
||||
comment == GetComment(cid)
|
||||
newMention == [
|
||||
id |-> mid,
|
||||
commentId |-> cid,
|
||||
mentionedUser |-> mentionedUser,
|
||||
mentioningUser |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
timestamp |-> Len(activityFeed[userTenants[user]]),
|
||||
read |-> FALSE
|
||||
]
|
||||
newNotif == [
|
||||
id |-> mid,
|
||||
userId |-> mentionedUser,
|
||||
type |-> "mention",
|
||||
sourceId |-> cid,
|
||||
message |-> "You were mentioned in a comment",
|
||||
timestamp |-> Len(notifications[mentionedUser]),
|
||||
read |-> FALSE
|
||||
]
|
||||
IN
|
||||
/\ mentions' = mentions \cup {newMention}
|
||||
/\ notifications' = [notifications EXCEPT
|
||||
![mentionedUser] = Append(@, newNotif)]
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "mention_user",
|
||||
targetId |-> mid,
|
||||
timestamp |-> Len(@)
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, comments,
|
||||
versionHistory>>
|
||||
|
||||
\* User resolves a comment
|
||||
ResolveComment(user, cid) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ \E c \in comments :
|
||||
/\ c.id = cid
|
||||
/\ CanAccessDocument(user, c.documentId)
|
||||
/\ ~c.resolved
|
||||
/\ comments' = (comments \ {c}) \cup {[c EXCEPT !.resolved = TRUE]}
|
||||
/\ activityFeed' = [activityFeed EXCEPT
|
||||
![userTenants[user]] = Append(@, [
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
action |-> "resolve_comment",
|
||||
targetId |-> cid,
|
||||
timestamp |-> Len(@)
|
||||
])]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, mentions,
|
||||
notifications, versionHistory>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Notifications *)
|
||||
|
||||
\* User reads a notification
|
||||
ReadNotification(user, notifIndex) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ notifIndex \in 1..Len(notifications[user])
|
||||
/\ ~notifications[user][notifIndex].read
|
||||
/\ LET
|
||||
notif == notifications[user][notifIndex]
|
||||
updatedNotif == [notif EXCEPT !.read = TRUE]
|
||||
IN
|
||||
/\ notifications' = [notifications EXCEPT
|
||||
![user] = [i \in 1..Len(@) |->
|
||||
IF i = notifIndex THEN updatedNotif ELSE @[i]]]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, comments,
|
||||
mentions, activityFeed, versionHistory>>
|
||||
|
||||
\* Clear all read notifications
|
||||
ClearReadNotifications(user) ==
|
||||
/\ userSessions[user] = "active"
|
||||
/\ LET
|
||||
unread == SelectSeq(notifications[user], LAMBDA n : ~n.read)
|
||||
IN
|
||||
/\ notifications' = [notifications EXCEPT ![user] = unread]
|
||||
/\ UNCHANGED <<userTenants, userSessions, documentOwners, documentTenants,
|
||||
documentContent, documentEditors, userPresence, comments,
|
||||
mentions, activityFeed, versionHistory>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Next State Relation *)
|
||||
|
||||
Next ==
|
||||
\/ \E u \in Users: UserConnect(u)
|
||||
\/ \E u \in Users: UserGoIdle(u)
|
||||
\/ \E u \in Users: UserDisconnect(u)
|
||||
\/ \E u \in Users, d \in Documents: StartEditing(u, d)
|
||||
\/ \E u \in Users, d \in Documents: StopEditing(u, d)
|
||||
\/ \E u \in Users, d \in Documents, op \in Operation:
|
||||
ApplyOperation(u, d, op)
|
||||
\/ \E u \in Users, d \in Documents: CreateVersion(u, d)
|
||||
\/ \E u \in Users, d \in Documents, cid \in Nat,
|
||||
content \in STRING, pos \in Nat:
|
||||
AddComment(u, d, cid, content, pos)
|
||||
\/ \E u \in Users, mu \in Users, cid \in Nat, mid \in Nat:
|
||||
MentionUser(u, mu, cid, mid)
|
||||
\/ \E u \in Users, cid \in Nat: ResolveComment(u, cid)
|
||||
\/ \E u \in Users, idx \in Nat: ReadNotification(u, idx)
|
||||
\/ \E u \in Users: ClearReadNotifications(u)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Safety Properties *)
|
||||
|
||||
\* Document access is tenant-isolated
|
||||
DocumentTenantIsolation ==
|
||||
\A u \in Users, d \in Documents:
|
||||
u \in documentEditors[d] => userTenants[u] = documentTenants[d]
|
||||
|
||||
\* Concurrent editors don't exceed limit
|
||||
ConcurrentEditorLimit ==
|
||||
\A d \in Documents:
|
||||
Cardinality(documentEditors[d]) <= MaxConcurrentEditors
|
||||
|
||||
\* Comments belong to document's tenant
|
||||
CommentTenantConsistency ==
|
||||
\A c \in comments:
|
||||
c.tenantId = documentTenants[c.documentId]
|
||||
|
||||
\* Mentions are within same tenant
|
||||
MentionTenantIsolation ==
|
||||
\A m \in mentions:
|
||||
userTenants[m.mentionedUser] = m.tenantId
|
||||
|
||||
\* Notifications don't exceed limit
|
||||
NotificationLimit ==
|
||||
\A u \in Users:
|
||||
CountPendingNotifications(u) <= MaxNotifications
|
||||
|
||||
\* Only active users can edit
|
||||
ActiveEditorsOnly ==
|
||||
\A u \in Users, d \in Documents:
|
||||
u \in documentEditors[d] =>
|
||||
userSessions[u] \in {"active", "idle"}
|
||||
|
||||
\* Disconnected users are not editing
|
||||
DisconnectedNotEditing ==
|
||||
\A u \in Users:
|
||||
userSessions[u] = "disconnected" =>
|
||||
~\E d \in Documents : u \in documentEditors[d]
|
||||
|
||||
\* Operations in document are from editors
|
||||
OperationAuthorship ==
|
||||
\A d \in Documents, i \in 1..Len(documentContent[d]):
|
||||
LET op == documentContent[d][i]
|
||||
IN CanAccessDocument(op.user, d)
|
||||
|
||||
\* Version snapshots preserve content
|
||||
VersionConsistency ==
|
||||
\A d \in Documents, v \in 1..Len(versionHistory[d]):
|
||||
versionHistory[d][v].documentId = d
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Liveness Properties *)
|
||||
|
||||
\* Pending notifications eventually get read or cleared
|
||||
EventualNotificationHandling ==
|
||||
\A u \in Users:
|
||||
(CountPendingNotifications(u) > 0) ~>
|
||||
(CountPendingNotifications(u) = 0 \/ userSessions[u] = "disconnected")
|
||||
|
||||
\* Comments with mentions eventually get read
|
||||
EventualMentionRead ==
|
||||
\A m \in mentions:
|
||||
~m.read ~> (m.read \/ userSessions[m.mentionedUser] = "disconnected")
|
||||
|
||||
\* Active editors eventually stop editing or disconnect
|
||||
EventualStopEditing ==
|
||||
\A u \in Users, d \in Documents:
|
||||
u \in documentEditors[d] ~>
|
||||
(u \notin documentEditors[d] \/ userSessions[u] = "disconnected")
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* System Specification *)
|
||||
|
||||
Spec ==
|
||||
/\ Init
|
||||
/\ [][Next]_vars
|
||||
/\ \A u \in Users, d \in Documents: WF_vars(StopEditing(u, d))
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Invariants *)
|
||||
|
||||
Invariants ==
|
||||
/\ TypeOK
|
||||
/\ DocumentTenantIsolation
|
||||
/\ ConcurrentEditorLimit
|
||||
/\ CommentTenantConsistency
|
||||
/\ MentionTenantIsolation
|
||||
/\ NotificationLimit
|
||||
/\ ActiveEditorsOnly
|
||||
/\ DisconnectedNotEditing
|
||||
/\ OperationAuthorship
|
||||
/\ VersionConsistency
|
||||
|
||||
=============================================================================
|
||||
36
spec/integrations.cfg
Normal file
36
spec/integrations.cfg
Normal file
@@ -0,0 +1,36 @@
|
||||
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
|
||||
644
spec/integrations.tla
Normal file
644
spec/integrations.tla
Normal file
@@ -0,0 +1,644 @@
|
||||
---------------------------- MODULE integrations ----------------------------
|
||||
(***************************************************************************
|
||||
* Integration Ecosystem Specification for MetaBuilder *
|
||||
* *
|
||||
* This specification models the integration ecosystem including: *
|
||||
* - Webhook management and delivery *
|
||||
* - OAuth application framework *
|
||||
* - API key management *
|
||||
* - Third-party app directory *
|
||||
* - Event subscriptions and filtering *
|
||||
* - Rate limiting and quota management *
|
||||
***************************************************************************)
|
||||
|
||||
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
||||
|
||||
CONSTANTS
|
||||
Users, \* Set of all users
|
||||
Tenants, \* Set of tenants
|
||||
Webhooks, \* Set of webhook IDs
|
||||
OAuthApps, \* Set of OAuth application IDs
|
||||
APIKeys, \* Set of API key IDs
|
||||
EventTypes, \* Set of event types to subscribe to
|
||||
MaxWebhooksPerTenant, \* Maximum webhooks per tenant
|
||||
MaxKeysPerUser, \* Maximum API keys per user
|
||||
RateLimitPerHour \* API calls allowed per hour
|
||||
|
||||
VARIABLES
|
||||
userLevels, \* User -> Permission Level
|
||||
userTenants, \* User -> Tenant
|
||||
webhookConfigs, \* Set of webhook configurations
|
||||
webhookQueue, \* Sequence of pending webhook deliveries
|
||||
webhookDeliveries, \* Set of delivery records
|
||||
oauthApps, \* Set of OAuth application records
|
||||
oauthTokens, \* Set of OAuth token records
|
||||
apiKeys, \* Set of API key records
|
||||
apiCallCounts, \* (User/App, Hour) -> Call count
|
||||
eventSubscriptions, \* Set of event subscriptions
|
||||
integrationAuditLog \* Sequence of integration events
|
||||
|
||||
vars == <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
||||
apiCallCounts, eventSubscriptions, integrationAuditLog>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Type Definitions *)
|
||||
|
||||
PermissionLevel == 1..6
|
||||
|
||||
WebhookStatus == {"active", "paused", "disabled"}
|
||||
DeliveryStatus == {"pending", "success", "failed", "retrying"}
|
||||
OAuthAppStatus == {"active", "suspended", "revoked"}
|
||||
APIKeyStatus == {"active", "expired", "revoked"}
|
||||
|
||||
WebhookConfig == [
|
||||
id: Webhooks,
|
||||
tenantId: Tenants,
|
||||
ownerId: Users,
|
||||
url: STRING,
|
||||
status: WebhookStatus,
|
||||
events: SUBSET EventTypes,
|
||||
secret: STRING,
|
||||
createdAt: Nat
|
||||
]
|
||||
|
||||
WebhookDelivery == [
|
||||
id: Nat,
|
||||
webhookId: Webhooks,
|
||||
eventType: EventTypes,
|
||||
payload: STRING,
|
||||
status: DeliveryStatus,
|
||||
attempts: Nat,
|
||||
timestamp: Nat
|
||||
]
|
||||
|
||||
OAuthApp == [
|
||||
id: OAuthApps,
|
||||
tenantId: Tenants,
|
||||
ownerId: Users,
|
||||
name: STRING,
|
||||
status: OAuthAppStatus,
|
||||
scopes: SUBSET STRING,
|
||||
redirectUri: STRING,
|
||||
clientId: STRING,
|
||||
createdAt: Nat
|
||||
]
|
||||
|
||||
OAuthToken == [
|
||||
id: Nat,
|
||||
appId: OAuthApps,
|
||||
userId: Users,
|
||||
tenantId: Tenants,
|
||||
accessToken: STRING,
|
||||
scopes: SUBSET STRING,
|
||||
expiresAt: Nat,
|
||||
createdAt: Nat
|
||||
]
|
||||
|
||||
APIKey == [
|
||||
id: APIKeys,
|
||||
userId: Users,
|
||||
tenantId: Tenants,
|
||||
name: STRING,
|
||||
key: STRING,
|
||||
status: APIKeyStatus,
|
||||
scopes: SUBSET STRING,
|
||||
expiresAt: Nat,
|
||||
createdAt: Nat
|
||||
]
|
||||
|
||||
EventSubscription == [
|
||||
id: Nat,
|
||||
subscriberId: Users \cup OAuthApps,
|
||||
tenantId: Tenants,
|
||||
eventType: EventTypes,
|
||||
filters: STRING,
|
||||
active: BOOLEAN
|
||||
]
|
||||
|
||||
TypeOK ==
|
||||
/\ userLevels \in [Users -> PermissionLevel]
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ webhookConfigs \subseteq WebhookConfig
|
||||
/\ webhookQueue \in Seq(WebhookDelivery)
|
||||
/\ webhookDeliveries \subseteq WebhookDelivery
|
||||
/\ oauthApps \subseteq OAuthApp
|
||||
/\ oauthTokens \subseteq OAuthToken
|
||||
/\ apiKeys \subseteq APIKey
|
||||
/\ apiCallCounts \in [(Users \cup OAuthApps) \X Nat -> Nat]
|
||||
/\ eventSubscriptions \subseteq EventSubscription
|
||||
/\ integrationAuditLog \in Seq([
|
||||
user: Users \cup {"system"},
|
||||
action: STRING,
|
||||
targetId: Nat \cup Webhooks \cup OAuthApps \cup APIKeys,
|
||||
tenant: Tenants,
|
||||
timestamp: Nat
|
||||
])
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Permission Checks *)
|
||||
|
||||
\* Admin level (4+) required for integration management
|
||||
CanManageIntegrations(user, tenant) ==
|
||||
/\ userLevels[user] >= 4
|
||||
/\ userTenants[user] = tenant
|
||||
|
||||
\* User level (2+) required for API keys
|
||||
CanManageAPIKeys(user) ==
|
||||
userLevels[user] >= 2
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Helper Functions *)
|
||||
|
||||
\* Count webhooks for a tenant
|
||||
CountWebhooksForTenant(tenant) ==
|
||||
Cardinality({w \in webhookConfigs : w.tenantId = tenant})
|
||||
|
||||
\* Count API keys for a user
|
||||
CountKeysForUser(user) ==
|
||||
Cardinality({k \in apiKeys : k.userId = user /\ k.status = "active"})
|
||||
|
||||
\* Get API call count for current hour
|
||||
GetCallCount(identity, hour) ==
|
||||
IF <<identity, hour>> \in DOMAIN apiCallCounts
|
||||
THEN apiCallCounts[<<identity, hour>>]
|
||||
ELSE 0
|
||||
|
||||
\* Check if rate limit exceeded
|
||||
RateLimitExceeded(identity, hour) ==
|
||||
GetCallCount(identity, hour) >= RateLimitPerHour
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Initial State *)
|
||||
|
||||
Init ==
|
||||
/\ userLevels \in [Users -> PermissionLevel]
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ webhookConfigs = {}
|
||||
/\ webhookQueue = <<>>
|
||||
/\ webhookDeliveries = {}
|
||||
/\ oauthApps = {}
|
||||
/\ oauthTokens = {}
|
||||
/\ apiKeys = {}
|
||||
/\ apiCallCounts = [x \in (Users \cup OAuthApps) \X Nat |-> 0]
|
||||
/\ eventSubscriptions = {}
|
||||
/\ integrationAuditLog = <<>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Webhook Operations *)
|
||||
|
||||
\* Admin creates a webhook
|
||||
CreateWebhook(user, wid, url, events, secret) ==
|
||||
/\ CanManageIntegrations(user, userTenants[user])
|
||||
/\ wid \in Webhooks
|
||||
/\ wid \notin {w.id : w \in webhookConfigs}
|
||||
/\ CountWebhooksForTenant(userTenants[user]) < MaxWebhooksPerTenant
|
||||
/\ events \subseteq EventTypes
|
||||
/\ events /= {}
|
||||
/\ LET newWebhook == [
|
||||
id |-> wid,
|
||||
tenantId |-> userTenants[user],
|
||||
ownerId |-> user,
|
||||
url |-> url,
|
||||
status |-> "active",
|
||||
events |-> events,
|
||||
secret |-> secret,
|
||||
createdAt |-> Len(integrationAuditLog)
|
||||
] IN
|
||||
/\ webhookConfigs' = webhookConfigs \cup {newWebhook}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "create_webhook",
|
||||
targetId |-> wid,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookQueue, webhookDeliveries,
|
||||
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* Admin updates webhook status
|
||||
UpdateWebhookStatus(user, wid, newStatus) ==
|
||||
/\ \E w \in webhookConfigs :
|
||||
/\ w.id = wid
|
||||
/\ CanManageIntegrations(user, w.tenantId)
|
||||
/\ newStatus \in WebhookStatus
|
||||
/\ webhookConfigs' = (webhookConfigs \ {w}) \cup
|
||||
{[w EXCEPT !.status = newStatus]}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "update_webhook_status",
|
||||
targetId |-> wid,
|
||||
tenant |-> w.tenantId,
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookQueue, webhookDeliveries,
|
||||
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* System enqueues webhook delivery
|
||||
EnqueueWebhook(wid, eventType, payload, deliveryId) ==
|
||||
/\ \E w \in webhookConfigs :
|
||||
/\ w.id = wid
|
||||
/\ w.status = "active"
|
||||
/\ eventType \in w.events
|
||||
/\ deliveryId \notin {d.id : d \in webhookDeliveries}
|
||||
/\ LET delivery == [
|
||||
id |-> deliveryId,
|
||||
webhookId |-> wid,
|
||||
eventType |-> eventType,
|
||||
payload |-> payload,
|
||||
status |-> "pending",
|
||||
attempts |-> 0,
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
] IN
|
||||
/\ webhookQueue' = Append(webhookQueue, delivery)
|
||||
/\ webhookDeliveries' = webhookDeliveries \cup {delivery}
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
||||
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
||||
integrationAuditLog>>
|
||||
|
||||
\* System attempts webhook delivery
|
||||
AttemptDelivery(deliveryId) ==
|
||||
/\ Len(webhookQueue) > 0
|
||||
/\ \E d \in webhookDeliveries :
|
||||
/\ d.id = deliveryId
|
||||
/\ d.status \in {"pending", "retrying"}
|
||||
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
||||
{[d EXCEPT
|
||||
!.status = "success",
|
||||
!.attempts = @ + 1
|
||||
]}
|
||||
/\ webhookQueue' = Tail(webhookQueue)
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
||||
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
||||
integrationAuditLog>>
|
||||
|
||||
\* Webhook delivery fails
|
||||
FailDelivery(deliveryId) ==
|
||||
/\ \E d \in webhookDeliveries :
|
||||
/\ d.id = deliveryId
|
||||
/\ d.status \in {"pending", "retrying"}
|
||||
/\ d.attempts < 3
|
||||
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
||||
{[d EXCEPT
|
||||
!.status = "retrying",
|
||||
!.attempts = @ + 1
|
||||
]}
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
oauthApps, oauthTokens, apiKeys, apiCallCounts,
|
||||
eventSubscriptions, integrationAuditLog>>
|
||||
|
||||
\* Webhook delivery permanently fails
|
||||
PermanentFailDelivery(deliveryId) ==
|
||||
/\ \E d \in webhookDeliveries :
|
||||
/\ d.id = deliveryId
|
||||
/\ d.status = "retrying"
|
||||
/\ d.attempts >= 3
|
||||
/\ webhookDeliveries' = (webhookDeliveries \ {d}) \cup
|
||||
{[d EXCEPT !.status = "failed"]}
|
||||
/\ webhookQueue' = SelectSeq(webhookQueue, LAMBDA x : x.id /= deliveryId)
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, oauthApps,
|
||||
oauthTokens, apiKeys, apiCallCounts, eventSubscriptions,
|
||||
integrationAuditLog>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* OAuth Application Management *)
|
||||
|
||||
\* Admin creates OAuth app
|
||||
CreateOAuthApp(user, appId, name, scopes, redirectUri) ==
|
||||
/\ CanManageIntegrations(user, userTenants[user])
|
||||
/\ appId \in OAuthApps
|
||||
/\ appId \notin {a.id : a \in oauthApps}
|
||||
/\ LET newApp == [
|
||||
id |-> appId,
|
||||
tenantId |-> userTenants[user],
|
||||
ownerId |-> user,
|
||||
name |-> name,
|
||||
status |-> "active",
|
||||
scopes |-> scopes,
|
||||
redirectUri |-> redirectUri,
|
||||
clientId |-> "client_" \o appId,
|
||||
createdAt |-> Len(integrationAuditLog)
|
||||
] IN
|
||||
/\ oauthApps' = oauthApps \cup {newApp}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "create_oauth_app",
|
||||
targetId |-> appId,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthTokens, apiKeys, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* User authorizes OAuth app
|
||||
AuthorizeOAuthApp(user, appId, tokenId, scopes) ==
|
||||
/\ \E app \in oauthApps :
|
||||
/\ app.id = appId
|
||||
/\ userTenants[user] = app.tenantId
|
||||
/\ app.status = "active"
|
||||
/\ scopes \subseteq app.scopes
|
||||
/\ tokenId \notin {t.id : t \in oauthTokens}
|
||||
/\ LET
|
||||
currentTime == Len(integrationAuditLog)
|
||||
newToken == [
|
||||
id |-> tokenId,
|
||||
appId |-> appId,
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
accessToken |-> "token_" \o tokenId,
|
||||
scopes |-> scopes,
|
||||
expiresAt |-> currentTime + 3600,
|
||||
createdAt |-> currentTime
|
||||
]
|
||||
IN
|
||||
/\ oauthTokens' = oauthTokens \cup {newToken}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "authorize_oauth_app",
|
||||
targetId |-> appId,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> currentTime
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, apiKeys, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* Admin revokes OAuth app
|
||||
RevokeOAuthApp(user, appId) ==
|
||||
/\ \E app \in oauthApps :
|
||||
/\ app.id = appId
|
||||
/\ CanManageIntegrations(user, app.tenantId)
|
||||
/\ app.status /= "revoked"
|
||||
/\ oauthApps' = (oauthApps \ {app}) \cup
|
||||
{[app EXCEPT !.status = "revoked"]}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "revoke_oauth_app",
|
||||
targetId |-> appId,
|
||||
tenant |-> app.tenantId,
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthTokens, apiKeys, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* API Key Management *)
|
||||
|
||||
\* User creates API key
|
||||
CreateAPIKey(user, keyId, name, scopes, expiresAt) ==
|
||||
/\ CanManageAPIKeys(user)
|
||||
/\ keyId \in APIKeys
|
||||
/\ keyId \notin {k.id : k \in apiKeys}
|
||||
/\ CountKeysForUser(user) < MaxKeysPerUser
|
||||
/\ LET newKey == [
|
||||
id |-> keyId,
|
||||
userId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
name |-> name,
|
||||
key |-> "key_" \o keyId,
|
||||
status |-> "active",
|
||||
scopes |-> scopes,
|
||||
expiresAt |-> expiresAt,
|
||||
createdAt |-> Len(integrationAuditLog)
|
||||
] IN
|
||||
/\ apiKeys' = apiKeys \cup {newKey}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "create_api_key",
|
||||
targetId |-> keyId,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* User revokes API key
|
||||
RevokeAPIKey(user, keyId) ==
|
||||
/\ \E key \in apiKeys :
|
||||
/\ key.id = keyId
|
||||
/\ key.userId = user
|
||||
/\ key.status = "active"
|
||||
/\ apiKeys' = (apiKeys \ {key}) \cup
|
||||
{[key EXCEPT !.status = "revoked"]}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "revoke_api_key",
|
||||
targetId |-> keyId,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
||||
eventSubscriptions>>
|
||||
|
||||
\* System expires old API keys
|
||||
ExpireAPIKey(keyId) ==
|
||||
/\ \E key \in apiKeys :
|
||||
/\ key.id = keyId
|
||||
/\ key.status = "active"
|
||||
/\ Len(integrationAuditLog) >= key.expiresAt
|
||||
/\ apiKeys' = (apiKeys \ {key}) \cup
|
||||
{[key EXCEPT !.status = "expired"]}
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiCallCounts,
|
||||
eventSubscriptions, integrationAuditLog>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Rate Limiting *)
|
||||
|
||||
\* Record API call
|
||||
RecordAPICall(identity, hour) ==
|
||||
/\ ~RateLimitExceeded(identity, hour)
|
||||
/\ apiCallCounts' = [apiCallCounts EXCEPT
|
||||
![<<identity, hour>>] = @ + 1]
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
||||
eventSubscriptions, integrationAuditLog>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Event Subscriptions *)
|
||||
|
||||
\* Create event subscription
|
||||
SubscribeToEvent(user, subId, eventType, filters) ==
|
||||
/\ CanManageIntegrations(user, userTenants[user])
|
||||
/\ subId \notin {s.id : s \in eventSubscriptions}
|
||||
/\ eventType \in EventTypes
|
||||
/\ LET newSub == [
|
||||
id |-> subId,
|
||||
subscriberId |-> user,
|
||||
tenantId |-> userTenants[user],
|
||||
eventType |-> eventType,
|
||||
filters |-> filters,
|
||||
active |-> TRUE
|
||||
] IN
|
||||
/\ eventSubscriptions' = eventSubscriptions \cup {newSub}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "subscribe_event",
|
||||
targetId |-> subId,
|
||||
tenant |-> userTenants[user],
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
||||
apiCallCounts>>
|
||||
|
||||
\* Unsubscribe from event
|
||||
UnsubscribeFromEvent(user, subId) ==
|
||||
/\ \E sub \in eventSubscriptions :
|
||||
/\ sub.id = subId
|
||||
/\ sub.subscriberId = user
|
||||
/\ CanManageIntegrations(user, sub.tenantId)
|
||||
/\ eventSubscriptions' = (eventSubscriptions \ {sub}) \cup
|
||||
{[sub EXCEPT !.active = FALSE]}
|
||||
/\ integrationAuditLog' = Append(integrationAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "unsubscribe_event",
|
||||
targetId |-> subId,
|
||||
tenant |-> sub.tenantId,
|
||||
timestamp |-> Len(integrationAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, webhookConfigs, webhookQueue,
|
||||
webhookDeliveries, oauthApps, oauthTokens, apiKeys,
|
||||
apiCallCounts>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Next State Relation *)
|
||||
|
||||
Next ==
|
||||
\/ \E u \in Users, wid \in Webhooks, url \in STRING,
|
||||
events \in SUBSET EventTypes, secret \in STRING:
|
||||
CreateWebhook(u, wid, url, events, secret)
|
||||
\/ \E u \in Users, wid \in Webhooks, status \in WebhookStatus:
|
||||
UpdateWebhookStatus(u, wid, status)
|
||||
\/ \E wid \in Webhooks, et \in EventTypes, payload \in STRING, did \in Nat:
|
||||
EnqueueWebhook(wid, et, payload, did)
|
||||
\/ \E did \in Nat: AttemptDelivery(did)
|
||||
\/ \E did \in Nat: FailDelivery(did)
|
||||
\/ \E did \in Nat: PermanentFailDelivery(did)
|
||||
\/ \E u \in Users, aid \in OAuthApps, name \in STRING,
|
||||
scopes \in SUBSET STRING, uri \in STRING:
|
||||
CreateOAuthApp(u, aid, name, scopes, uri)
|
||||
\/ \E u \in Users, aid \in OAuthApps, tid \in Nat, scopes \in SUBSET STRING:
|
||||
AuthorizeOAuthApp(u, aid, tid, scopes)
|
||||
\/ \E u \in Users, aid \in OAuthApps: RevokeOAuthApp(u, aid)
|
||||
\/ \E u \in Users, kid \in APIKeys, name \in STRING,
|
||||
scopes \in SUBSET STRING, exp \in Nat:
|
||||
CreateAPIKey(u, kid, name, scopes, exp)
|
||||
\/ \E u \in Users, kid \in APIKeys: RevokeAPIKey(u, kid)
|
||||
\/ \E kid \in APIKeys: ExpireAPIKey(kid)
|
||||
\/ \E identity \in (Users \cup OAuthApps), hour \in Nat:
|
||||
RecordAPICall(identity, hour)
|
||||
\/ \E u \in Users, sid \in Nat, et \in EventTypes, f \in STRING:
|
||||
SubscribeToEvent(u, sid, et, f)
|
||||
\/ \E u \in Users, sid \in Nat: UnsubscribeFromEvent(u, sid)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Safety Properties *)
|
||||
|
||||
\* Admin-only integration management
|
||||
AdminOnlyIntegrationManagement ==
|
||||
\A event \in 1..Len(integrationAuditLog):
|
||||
LET action == integrationAuditLog[event].action IN
|
||||
action \in {"create_webhook", "update_webhook_status",
|
||||
"create_oauth_app", "revoke_oauth_app",
|
||||
"subscribe_event", "unsubscribe_event"} =>
|
||||
userLevels[integrationAuditLog[event].user] >= 4
|
||||
|
||||
\* Webhooks don't exceed tenant limit
|
||||
WebhookTenantLimit ==
|
||||
\A t \in Tenants:
|
||||
CountWebhooksForTenant(t) <= MaxWebhooksPerTenant
|
||||
|
||||
\* API keys don't exceed user limit
|
||||
APIKeyUserLimit ==
|
||||
\A u \in Users:
|
||||
CountKeysForUser(u) <= MaxKeysPerUser
|
||||
|
||||
\* Rate limits are enforced
|
||||
RateLimitEnforcement ==
|
||||
\A identity \in (Users \cup OAuthApps), hour \in Nat:
|
||||
GetCallCount(identity, hour) <= RateLimitPerHour
|
||||
|
||||
\* Tenant isolation for webhooks
|
||||
WebhookTenantIsolation ==
|
||||
\A w \in webhookConfigs:
|
||||
userTenants[w.ownerId] = w.tenantId
|
||||
|
||||
\* Tenant isolation for OAuth apps
|
||||
OAuthAppTenantIsolation ==
|
||||
\A app \in oauthApps:
|
||||
userTenants[app.ownerId] = app.tenantId
|
||||
|
||||
\* Tenant isolation for API keys
|
||||
APIKeyTenantIsolation ==
|
||||
\A key \in apiKeys:
|
||||
userTenants[key.userId] = key.tenantId
|
||||
|
||||
\* OAuth tokens match app tenants
|
||||
TokenTenantConsistency ==
|
||||
\A token \in oauthTokens:
|
||||
\E app \in oauthApps:
|
||||
app.id = token.appId /\ app.tenantId = token.tenantId
|
||||
|
||||
\* Active deliveries are in queue
|
||||
ActiveDeliveriesQueued ==
|
||||
\A d \in webhookDeliveries:
|
||||
d.status = "pending" =>
|
||||
\E i \in 1..Len(webhookQueue) : webhookQueue[i].id = d.id
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Liveness Properties *)
|
||||
|
||||
\* Webhook deliveries eventually complete or fail
|
||||
EventualDeliveryCompletion ==
|
||||
\A did \in Nat:
|
||||
\E d \in webhookDeliveries :
|
||||
d.id = did /\ d.status = "pending" ~>
|
||||
d.status \in {"success", "failed"}
|
||||
|
||||
\* Failed deliveries eventually retry or permanently fail
|
||||
EventualRetryOrFail ==
|
||||
\A did \in Nat:
|
||||
\E d \in webhookDeliveries :
|
||||
d.id = did /\ d.status = "retrying" ~>
|
||||
d.status \in {"success", "failed"}
|
||||
|
||||
\* Expired keys eventually get marked as expired
|
||||
EventualExpiration ==
|
||||
\A kid \in APIKeys:
|
||||
\E key \in apiKeys :
|
||||
key.id = kid /\ key.status = "active" /\
|
||||
Len(integrationAuditLog) >= key.expiresAt ~>
|
||||
key.status = "expired"
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* System Specification *)
|
||||
|
||||
Spec ==
|
||||
/\ Init
|
||||
/\ [][Next]_vars
|
||||
/\ \A did \in Nat: WF_vars(AttemptDelivery(did))
|
||||
/\ \A kid \in APIKeys: WF_vars(ExpireAPIKey(kid))
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Invariants *)
|
||||
|
||||
Invariants ==
|
||||
/\ TypeOK
|
||||
/\ AdminOnlyIntegrationManagement
|
||||
/\ WebhookTenantLimit
|
||||
/\ APIKeyUserLimit
|
||||
/\ RateLimitEnforcement
|
||||
/\ WebhookTenantIsolation
|
||||
/\ OAuthAppTenantIsolation
|
||||
/\ APIKeyTenantIsolation
|
||||
/\ TokenTenantConsistency
|
||||
/\ ActiveDeliveriesQueued
|
||||
|
||||
=============================================================================
|
||||
31
spec/workflow_system.cfg
Normal file
31
spec/workflow_system.cfg
Normal file
@@ -0,0 +1,31 @@
|
||||
SPECIFICATION Spec
|
||||
|
||||
CONSTANTS
|
||||
Users = {u1, u2, u3}
|
||||
Tenants = {t1, t2}
|
||||
WorkflowTemplates = {wf1, wf2, wf3}
|
||||
WorkflowSteps = {step1, step2, step3}
|
||||
MaxRetries = 3
|
||||
MaxConcurrentRuns = 2
|
||||
|
||||
INVARIANTS
|
||||
TypeOK
|
||||
GodOnlyTemplateCreation
|
||||
AdminOnlyExecution
|
||||
TenantIsolation
|
||||
ConcurrencyLimit
|
||||
RetryLimit
|
||||
NoOverlap
|
||||
DependencyEnforcement
|
||||
AuditCompleteness
|
||||
|
||||
PROPERTIES
|
||||
EventualStepExecution
|
||||
EventualCompletion
|
||||
EventualScheduleTrigger
|
||||
|
||||
\* Constraint to limit state space for model checking
|
||||
CONSTRAINT
|
||||
/\ Len(workflowAuditLog) <= 15
|
||||
/\ Cardinality(instances) <= 5
|
||||
/\ Cardinality(runningWorkflows) <= 3
|
||||
595
spec/workflow_system.tla
Normal file
595
spec/workflow_system.tla
Normal file
@@ -0,0 +1,595 @@
|
||||
---------------------------- MODULE workflow_system ----------------------------
|
||||
(***************************************************************************
|
||||
* Workflow System Specification for MetaBuilder *
|
||||
* *
|
||||
* This specification models workflow execution, scheduling, and state *
|
||||
* management for MetaBuilder's advanced workflow features. *
|
||||
* *
|
||||
* Features modeled: *
|
||||
* - Workflow definition and validation *
|
||||
* - Scheduled and manual workflow execution *
|
||||
* - Step dependencies and parallel execution *
|
||||
* - Error handling and retry logic *
|
||||
* - Workflow templates and instances *
|
||||
* - God-level (Level 5+) permission requirements *
|
||||
***************************************************************************)
|
||||
|
||||
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
||||
|
||||
CONSTANTS
|
||||
Users, \* Set of all users
|
||||
Tenants, \* Set of tenants
|
||||
WorkflowTemplates, \* Set of workflow templates
|
||||
WorkflowSteps, \* Set of possible workflow steps
|
||||
MaxRetries, \* Maximum retry attempts for failed steps
|
||||
MaxConcurrentRuns \* Maximum concurrent workflow executions per tenant
|
||||
|
||||
VARIABLES
|
||||
userLevels, \* User -> Permission Level
|
||||
userTenants, \* User -> Tenant
|
||||
templates, \* WorkflowTemplate -> Template Definition
|
||||
instances, \* WorkflowInstance -> Instance State
|
||||
scheduledRuns, \* Set of scheduled workflow runs
|
||||
runningWorkflows, \* Set of currently executing workflow instances
|
||||
completedWorkflows, \* Set of completed workflow instances
|
||||
workflowAuditLog \* Sequence of workflow events
|
||||
|
||||
vars == <<userLevels, userTenants, templates, instances, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows, workflowAuditLog>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Type Definitions *)
|
||||
|
||||
PermissionLevel == 1..6
|
||||
|
||||
WorkflowStatus == {"draft", "active", "paused", "archived"}
|
||||
StepStatus == {"pending", "running", "success", "failed", "skipped", "retrying"}
|
||||
InstanceStatus == {"queued", "running", "completed", "failed", "cancelled"}
|
||||
|
||||
TemplateRecord == [
|
||||
id: WorkflowTemplates,
|
||||
name: STRING,
|
||||
tenantId: Tenants,
|
||||
status: WorkflowStatus,
|
||||
steps: Seq(WorkflowSteps),
|
||||
dependencies: [WorkflowSteps -> SUBSET WorkflowSteps], \* Step dependencies
|
||||
trigger: {"manual", "scheduled", "event"}
|
||||
]
|
||||
|
||||
InstanceRecord == [
|
||||
id: Nat,
|
||||
templateId: WorkflowTemplates,
|
||||
tenantId: Tenants,
|
||||
status: InstanceStatus,
|
||||
startedBy: Users,
|
||||
startTime: Nat,
|
||||
stepStates: [WorkflowSteps -> StepStatus],
|
||||
retryCount: [WorkflowSteps -> Nat],
|
||||
result: STRING
|
||||
]
|
||||
|
||||
TypeOK ==
|
||||
/\ userLevels \in [Users -> PermissionLevel]
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ templates \subseteq TemplateRecord
|
||||
/\ instances \subseteq InstanceRecord
|
||||
/\ scheduledRuns \subseteq (WorkflowTemplates \X Tenants \X Nat) \* (template, tenant, timestamp)
|
||||
/\ runningWorkflows \subseteq Nat \* Instance IDs
|
||||
/\ completedWorkflows \subseteq Nat
|
||||
/\ workflowAuditLog \in Seq([
|
||||
user: Users \cup {"system"},
|
||||
action: STRING,
|
||||
templateId: WorkflowTemplates \cup {0},
|
||||
instanceId: Nat,
|
||||
tenant: Tenants,
|
||||
timestamp: Nat
|
||||
])
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Permission Checks *)
|
||||
|
||||
\* God level (5+) required for workflow authoring
|
||||
CanAuthorWorkflow(user, tenant) ==
|
||||
/\ userLevels[user] >= 5
|
||||
/\ userTenants[user] = tenant
|
||||
|
||||
\* Admin level (4+) required for workflow execution
|
||||
CanExecuteWorkflow(user, tenant) ==
|
||||
/\ userLevels[user] >= 4
|
||||
/\ userTenants[user] = tenant
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Helper Functions *)
|
||||
|
||||
\* Get template by ID
|
||||
GetTemplate(tid) ==
|
||||
CHOOSE t \in templates : t.id = tid
|
||||
|
||||
\* Get instance by ID
|
||||
GetInstance(iid) ==
|
||||
CHOOSE i \in instances : i.id = iid
|
||||
|
||||
\* Check if all dependencies of a step are satisfied
|
||||
StepDependenciesSatisfied(instance, step) ==
|
||||
LET
|
||||
template == GetTemplate(instance.templateId)
|
||||
deps == template.dependencies[step]
|
||||
IN
|
||||
\A dep \in deps :
|
||||
instance.stepStates[dep] \in {"success", "skipped"}
|
||||
|
||||
\* Count running workflows for a tenant
|
||||
CountRunningForTenant(tenant) ==
|
||||
Cardinality({i \in runningWorkflows : GetInstance(i).tenantId = tenant})
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Initial State *)
|
||||
|
||||
Init ==
|
||||
/\ userLevels \in [Users -> PermissionLevel]
|
||||
/\ userTenants \in [Users -> Tenants]
|
||||
/\ templates = {}
|
||||
/\ instances = {}
|
||||
/\ scheduledRuns = {}
|
||||
/\ runningWorkflows = {}
|
||||
/\ completedWorkflows = {}
|
||||
/\ workflowAuditLog = <<>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Workflow Template Operations *)
|
||||
|
||||
\* God user creates a new workflow template
|
||||
CreateTemplate(user, tid, tenant, steps, deps, trigger) ==
|
||||
/\ CanAuthorWorkflow(user, tenant)
|
||||
/\ tid \in WorkflowTemplates
|
||||
/\ tid \notin {t.id : t \in templates}
|
||||
/\ steps \in Seq(WorkflowSteps)
|
||||
/\ Len(steps) > 0
|
||||
/\ trigger \in {"manual", "scheduled", "event"}
|
||||
/\ LET newTemplate == [
|
||||
id |-> tid,
|
||||
name |-> "WorkflowTemplate",
|
||||
tenantId |-> tenant,
|
||||
status |-> "draft",
|
||||
steps |-> steps,
|
||||
dependencies |-> deps,
|
||||
trigger |-> trigger
|
||||
] IN
|
||||
/\ templates' = templates \cup {newTemplate}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "create_template",
|
||||
templateId |-> tid,
|
||||
instanceId |-> 0,
|
||||
tenant |-> tenant,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* God user activates a template
|
||||
ActivateTemplate(user, tid) ==
|
||||
/\ \E t \in templates :
|
||||
/\ t.id = tid
|
||||
/\ CanAuthorWorkflow(user, t.tenantId)
|
||||
/\ t.status = "draft"
|
||||
/\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "active"]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "activate_template",
|
||||
templateId |-> tid,
|
||||
instanceId |-> 0,
|
||||
tenant |-> t.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* God user archives a template
|
||||
ArchiveTemplate(user, tid) ==
|
||||
/\ \E t \in templates :
|
||||
/\ t.id = tid
|
||||
/\ CanAuthorWorkflow(user, t.tenantId)
|
||||
/\ t.status \in {"active", "paused"}
|
||||
/\ templates' = (templates \ {t}) \cup {[t EXCEPT !.status = "archived"]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "archive_template",
|
||||
templateId |-> tid,
|
||||
instanceId |-> 0,
|
||||
tenant |-> t.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, instances, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Workflow Execution *)
|
||||
|
||||
\* Admin user manually starts a workflow
|
||||
StartWorkflow(user, tid, iid) ==
|
||||
/\ \E t \in templates :
|
||||
/\ t.id = tid
|
||||
/\ CanExecuteWorkflow(user, t.tenantId)
|
||||
/\ t.status = "active"
|
||||
/\ CountRunningForTenant(t.tenantId) < MaxConcurrentRuns
|
||||
/\ iid \notin {i.id : i \in instances}
|
||||
/\ LET
|
||||
initialStepStates == [s \in WorkflowSteps |->
|
||||
IF s \in {t.steps[i] : i \in 1..Len(t.steps)}
|
||||
THEN "pending"
|
||||
ELSE "skipped"]
|
||||
initialRetryCount == [s \in WorkflowSteps |-> 0]
|
||||
newInstance == [
|
||||
id |-> iid,
|
||||
templateId |-> tid,
|
||||
tenantId |-> t.tenantId,
|
||||
status |-> "running",
|
||||
startedBy |-> user,
|
||||
startTime |-> Len(workflowAuditLog),
|
||||
stepStates |-> initialStepStates,
|
||||
retryCount |-> initialRetryCount,
|
||||
result |-> "in_progress"
|
||||
]
|
||||
IN
|
||||
/\ instances' = instances \cup {newInstance}
|
||||
/\ runningWorkflows' = runningWorkflows \cup {iid}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "start_workflow",
|
||||
templateId |-> tid,
|
||||
instanceId |-> iid,
|
||||
tenant |-> t.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
||||
completedWorkflows>>
|
||||
|
||||
\* System executes a workflow step
|
||||
ExecuteStep(iid, step) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.status = "running"
|
||||
/\ instance.stepStates[step] = "pending"
|
||||
/\ StepDependenciesSatisfied(instance, step)
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT !.stepStates[step] = "running"]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "execute_step",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* Step completes successfully
|
||||
CompleteStep(iid, step) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.stepStates[step] = "running"
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT !.stepStates[step] = "success"]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "complete_step",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* Step fails (may retry)
|
||||
FailStep(iid, step) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.stepStates[step] = "running"
|
||||
/\ LET
|
||||
newRetryCount == instance.retryCount[step] + 1
|
||||
shouldRetry == newRetryCount < MaxRetries
|
||||
newStatus == IF shouldRetry THEN "retrying" ELSE "failed"
|
||||
IN
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT
|
||||
!.stepStates[step] = newStatus,
|
||||
!.retryCount[step] = newRetryCount
|
||||
]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "fail_step",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* Retry a failed step
|
||||
RetryStep(iid, step) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.stepStates[step] = "retrying"
|
||||
/\ instance.retryCount[step] < MaxRetries
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT !.stepStates[step] = "pending"]}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "retry_step",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* Complete entire workflow
|
||||
CompleteWorkflow(iid) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.status = "running"
|
||||
/\ LET
|
||||
template == GetTemplate(instance.templateId)
|
||||
allStepsComplete == \A step \in {template.steps[i] : i \in 1..Len(template.steps)} :
|
||||
instance.stepStates[step] \in {"success", "skipped"}
|
||||
IN
|
||||
/\ allStepsComplete
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT
|
||||
!.status = "completed",
|
||||
!.result = "success"
|
||||
]}
|
||||
/\ runningWorkflows' = runningWorkflows \ {iid}
|
||||
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "complete_workflow",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
||||
|
||||
\* Fail entire workflow
|
||||
FailWorkflow(iid) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ instance.status = "running"
|
||||
/\ LET
|
||||
template == GetTemplate(instance.templateId)
|
||||
hasFailedStep == \E step \in {template.steps[i] : i \in 1..Len(template.steps)} :
|
||||
/\ instance.stepStates[step] = "failed"
|
||||
/\ instance.retryCount[step] >= MaxRetries
|
||||
IN
|
||||
/\ hasFailedStep
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT
|
||||
!.status = "failed",
|
||||
!.result = "failure"
|
||||
]}
|
||||
/\ runningWorkflows' = runningWorkflows \ {iid}
|
||||
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "fail_workflow",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
||||
|
||||
\* Admin user cancels a running workflow
|
||||
CancelWorkflow(user, iid) ==
|
||||
/\ iid \in runningWorkflows
|
||||
/\ \E instance \in instances :
|
||||
/\ instance.id = iid
|
||||
/\ CanExecuteWorkflow(user, instance.tenantId)
|
||||
/\ instance.status = "running"
|
||||
/\ instances' = (instances \ {instance}) \cup
|
||||
{[instance EXCEPT
|
||||
!.status = "cancelled",
|
||||
!.result = "cancelled"
|
||||
]}
|
||||
/\ runningWorkflows' = runningWorkflows \ {iid}
|
||||
/\ completedWorkflows' = completedWorkflows \cup {iid}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "cancel_workflow",
|
||||
templateId |-> instance.templateId,
|
||||
instanceId |-> iid,
|
||||
tenant |-> instance.tenantId,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, scheduledRuns>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Scheduling *)
|
||||
|
||||
\* Schedule a workflow run
|
||||
ScheduleWorkflow(user, tid, tenant, scheduledTime) ==
|
||||
/\ \E t \in templates :
|
||||
/\ t.id = tid
|
||||
/\ t.tenantId = tenant
|
||||
/\ CanExecuteWorkflow(user, tenant)
|
||||
/\ t.status = "active"
|
||||
/\ t.trigger \in {"scheduled", "manual"}
|
||||
/\ scheduledRuns' = scheduledRuns \cup {<<tid, tenant, scheduledTime>>}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> user,
|
||||
action |-> "schedule_workflow",
|
||||
templateId |-> tid,
|
||||
instanceId |-> 0,
|
||||
tenant |-> tenant,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, instances,
|
||||
runningWorkflows, completedWorkflows>>
|
||||
|
||||
\* System triggers a scheduled workflow
|
||||
TriggerScheduled(tid, tenant, scheduledTime, iid) ==
|
||||
/\ <<tid, tenant, scheduledTime>> \in scheduledRuns
|
||||
/\ Len(workflowAuditLog) >= scheduledTime
|
||||
/\ \E t \in templates :
|
||||
/\ t.id = tid
|
||||
/\ t.tenantId = tenant
|
||||
/\ t.status = "active"
|
||||
/\ CountRunningForTenant(tenant) < MaxConcurrentRuns
|
||||
/\ iid \notin {i.id : i \in instances}
|
||||
/\ LET
|
||||
initialStepStates == [s \in WorkflowSteps |->
|
||||
IF s \in {t.steps[i] : i \in 1..Len(t.steps)}
|
||||
THEN "pending"
|
||||
ELSE "skipped"]
|
||||
initialRetryCount == [s \in WorkflowSteps |-> 0]
|
||||
newInstance == [
|
||||
id |-> iid,
|
||||
templateId |-> tid,
|
||||
tenantId |-> tenant,
|
||||
status |-> "running",
|
||||
startedBy |-> CHOOSE u \in Users : userTenants[u] = tenant /\ userLevels[u] >= 5,
|
||||
startTime |-> Len(workflowAuditLog),
|
||||
stepStates |-> initialStepStates,
|
||||
retryCount |-> initialRetryCount,
|
||||
result |-> "in_progress"
|
||||
]
|
||||
IN
|
||||
/\ instances' = instances \cup {newInstance}
|
||||
/\ runningWorkflows' = runningWorkflows \cup {iid}
|
||||
/\ scheduledRuns' = scheduledRuns \ {<<tid, tenant, scheduledTime>>}
|
||||
/\ workflowAuditLog' = Append(workflowAuditLog, [
|
||||
user |-> "system",
|
||||
action |-> "trigger_scheduled",
|
||||
templateId |-> tid,
|
||||
instanceId |-> iid,
|
||||
tenant |-> tenant,
|
||||
timestamp |-> Len(workflowAuditLog)
|
||||
])
|
||||
/\ UNCHANGED <<userLevels, userTenants, templates, completedWorkflows>>
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Next State Relation *)
|
||||
|
||||
Next ==
|
||||
\/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants,
|
||||
steps \in Seq(WorkflowSteps),
|
||||
deps \in [WorkflowSteps -> SUBSET WorkflowSteps],
|
||||
trigger \in {"manual", "scheduled", "event"}:
|
||||
CreateTemplate(u, tid, t, steps, deps, trigger)
|
||||
\/ \E u \in Users, tid \in WorkflowTemplates: ActivateTemplate(u, tid)
|
||||
\/ \E u \in Users, tid \in WorkflowTemplates: ArchiveTemplate(u, tid)
|
||||
\/ \E u \in Users, tid \in WorkflowTemplates, iid \in Nat:
|
||||
StartWorkflow(u, tid, iid)
|
||||
\/ \E iid \in Nat, step \in WorkflowSteps: ExecuteStep(iid, step)
|
||||
\/ \E iid \in Nat, step \in WorkflowSteps: CompleteStep(iid, step)
|
||||
\/ \E iid \in Nat, step \in WorkflowSteps: FailStep(iid, step)
|
||||
\/ \E iid \in Nat, step \in WorkflowSteps: RetryStep(iid, step)
|
||||
\/ \E iid \in Nat: CompleteWorkflow(iid)
|
||||
\/ \E iid \in Nat: FailWorkflow(iid)
|
||||
\/ \E u \in Users, iid \in Nat: CancelWorkflow(u, iid)
|
||||
\/ \E u \in Users, tid \in WorkflowTemplates, t \in Tenants, time \in Nat:
|
||||
ScheduleWorkflow(u, tid, t, time)
|
||||
\/ \E tid \in WorkflowTemplates, t \in Tenants, time \in Nat, iid \in Nat:
|
||||
TriggerScheduled(tid, t, time, iid)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Safety Properties *)
|
||||
|
||||
\* Only God-level users can create templates
|
||||
GodOnlyTemplateCreation ==
|
||||
\A event \in 1..Len(workflowAuditLog):
|
||||
workflowAuditLog[event].action = "create_template" =>
|
||||
userLevels[workflowAuditLog[event].user] >= 5
|
||||
|
||||
\* Only Admin+ users can execute workflows
|
||||
AdminOnlyExecution ==
|
||||
\A event \in 1..Len(workflowAuditLog):
|
||||
workflowAuditLog[event].action \in {"start_workflow", "cancel_workflow"} =>
|
||||
userLevels[workflowAuditLog[event].user] >= 4
|
||||
|
||||
\* Workflow instances belong to exactly one tenant
|
||||
TenantIsolation ==
|
||||
\A i1, i2 \in instances:
|
||||
i1.id = i2.id => i1.tenantId = i2.tenantId
|
||||
|
||||
\* Running workflows don't exceed concurrency limit
|
||||
ConcurrencyLimit ==
|
||||
\A t \in Tenants:
|
||||
CountRunningForTenant(t) <= MaxConcurrentRuns
|
||||
|
||||
\* Failed steps don't exceed retry limit
|
||||
RetryLimit ==
|
||||
\A i \in instances, s \in WorkflowSteps:
|
||||
i.retryCount[s] <= MaxRetries
|
||||
|
||||
\* Completed workflows are not in running set
|
||||
NoOverlap ==
|
||||
runningWorkflows \cap completedWorkflows = {}
|
||||
|
||||
\* Step dependencies are respected
|
||||
DependencyEnforcement ==
|
||||
\A i \in instances, step \in WorkflowSteps:
|
||||
i.stepStates[step] \in {"running", "success"} =>
|
||||
StepDependenciesSatisfied(i, step)
|
||||
|
||||
\* All workflow events are audited
|
||||
AuditCompleteness ==
|
||||
Len(workflowAuditLog) >= Cardinality(instances)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Liveness Properties *)
|
||||
|
||||
\* Pending steps eventually execute (if dependencies are met)
|
||||
EventualStepExecution ==
|
||||
\A i \in instances, step \in WorkflowSteps:
|
||||
(i.stepStates[step] = "pending" /\ StepDependenciesSatisfied(i, step)) ~>
|
||||
i.stepStates[step] \in {"running", "success", "failed"}
|
||||
|
||||
\* Running workflows eventually complete or fail
|
||||
EventualCompletion ==
|
||||
\A iid \in Nat:
|
||||
iid \in runningWorkflows ~> iid \in completedWorkflows
|
||||
|
||||
\* Scheduled workflows eventually trigger
|
||||
EventualScheduleTrigger ==
|
||||
\A tid \in WorkflowTemplates, t \in Tenants, time \in Nat:
|
||||
<<tid, t, time>> \in scheduledRuns ~>
|
||||
(<<tid, t, time>> \notin scheduledRuns \/ CountRunningForTenant(t) >= MaxConcurrentRuns)
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* System Specification *)
|
||||
|
||||
Spec ==
|
||||
/\ Init
|
||||
/\ [][Next]_vars
|
||||
/\ \A iid \in Nat: WF_vars(CompleteWorkflow(iid))
|
||||
/\ \A iid \in Nat: WF_vars(FailWorkflow(iid))
|
||||
/\ \A iid \in Nat, step \in WorkflowSteps: WF_vars(ExecuteStep(iid, step))
|
||||
|
||||
-----------------------------------------------------------------------------
|
||||
(* Invariants *)
|
||||
|
||||
Invariants ==
|
||||
/\ TypeOK
|
||||
/\ GodOnlyTemplateCreation
|
||||
/\ AdminOnlyExecution
|
||||
/\ TenantIsolation
|
||||
/\ ConcurrencyLimit
|
||||
/\ RetryLimit
|
||||
/\ NoOverlap
|
||||
/\ DependencyEnforcement
|
||||
/\ AuditCompleteness
|
||||
|
||||
=============================================================================
|
||||
Reference in New Issue
Block a user