mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
28 lines
522 B
INI
28 lines
522 B
INI
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
|