mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-25 06:14:59 +00:00
cbb257d914
- Created spec/metabuilder.tla with comprehensive formal specification - Modeled 6-level permission system (Public → User → Moderator → Admin → God → Supergod) - Defined multi-tenant data isolation invariants - Specified DBAL state machine with security properties - Included package management operations - Added safety properties: TenantIsolation, PermissionEnforcement, DataConsistency - Added liveness properties: EventualProcessing, EventualRecovery - Created spec/metabuilder.cfg for TLC model checker configuration - Added spec/README.md with comprehensive documentation and usage guide Co-authored-by: johndoe6345789 <224850594+johndoe6345789@users.noreply.github.com>
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
|