SPECIFICATION Spec

CONSTANTS
    Users = {u1, u2, u3, u4}
    Tenants = {t1, t2}
    Packages = {p1, p2, p3}
    DataRecords = {r1, r2, r3}
    MaxLevel = 6

INVARIANTS
    TypeOK
    TenantIsolation
    PermissionEnforcement
    DataConsistency
    PackageConsistency
    DBALSafety
    AuditCompleteness

PROPERTIES
    EventualProcessing
    EventualRecovery
    EventualPackageInstall

\* Constraint to limit state space for model checking
CONSTRAINT
    /\ Len(auditLog) <= 10
    /\ Cardinality(activeQueries) <= 5