mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
547 lines
20 KiB
Plaintext
547 lines
20 KiB
Plaintext
---------------------------- 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:
|
|
Len(documentContent[d]) > 0 =>
|
|
\A 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:
|
|
Len(versionHistory[d]) > 0 =>
|
|
\A 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
|
|
|
|
=============================================================================
|