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