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