mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
johndoe6345789
3ec49cfe8c
- Added `package_system.tla` to model the schema-driven package system, including multi-source loading, validation, dependency resolution, and permission filtering. - Created `package_system.cfg` for TLC model checker configuration, defining constants and invariants for bounded model checking. - Updated `metabuilder.tla` to reflect the core specification of MetaBuilder, emphasizing the package lifecycle and related specifications.
80 lines
2.4 KiB
INI
80 lines
2.4 KiB
INI
\* Package System Model Configuration
|
|
\* =================================
|
|
\* Configuration for TLC model checker for the schema-driven package system.
|
|
\*
|
|
\* Aligned with:
|
|
\* - schemas/package-schemas/*.json (16+ schemas)
|
|
\* - docs/packages/package-sources.md
|
|
\* - packages/*/package.json structure
|
|
|
|
SPECIFICATION Spec
|
|
|
|
\* Constants for bounded model checking
|
|
CONSTANTS
|
|
\* Users in the system
|
|
Users = {u1, u2, u3, u4}
|
|
|
|
\* Tenants (multi-tenant isolation)
|
|
Tenants = {tenant1, tenant2}
|
|
|
|
\* Package IDs (sample packages from the packages/ directory)
|
|
Packages = {dashboard, data_table, ui_auth, ui_permissions}
|
|
|
|
\* Package versions (semver)
|
|
PackageVersions = {"1.0.0", "1.1.0", "2.0.0"}
|
|
|
|
\* Package sources (local, remote, and potential custom registries)
|
|
PackageSources = {local, remote}
|
|
|
|
\* Schema types from schemas/package-schemas/
|
|
SchemaTypes = {metadata, entities, components, scripts, types, validation}
|
|
|
|
\* Maximum permission level (6-level system)
|
|
MaxLevel = 6
|
|
|
|
\* Safety invariants to check
|
|
INVARIANT TypeOK
|
|
INVARIANT AdminOnlyPackageManagement
|
|
INVARIANT SupergodOnlySourceManagement
|
|
INVARIANT EnabledImpliesInstalled
|
|
INVARIANT DependencyIntegrity
|
|
|
|
\* For larger state spaces, use relaxed invariants:
|
|
\* INVARIANT RelaxedInvariants
|
|
|
|
\* Liveness properties (temporal)
|
|
\* Uncomment to check liveness (requires more time)
|
|
\* PROPERTY EventualOperationCompletion
|
|
\* PROPERTY EventualValidation
|
|
\* PROPERTY EventualConflictResolution
|
|
\* PROPERTY EventualIndexRefresh
|
|
|
|
\* State constraints to bound model checking
|
|
CONSTRAINT
|
|
\* Limit audit log length to keep state space manageable
|
|
Len(packageAuditLog) <= 10
|
|
|
|
\* Limit pending operations
|
|
/\ Cardinality(pendingOperations) <= 5
|
|
|
|
\* Limit conflicts tracked
|
|
/\ Cardinality(packageConflicts) <= 4
|
|
|
|
\* Limit schema validations
|
|
/\ Cardinality(schemaValidations) <= 12
|
|
|
|
\* Symmetry sets for faster model checking
|
|
\* (TLC can explore symmetric states once instead of multiple times)
|
|
SYMMETRY symUsers, symTenants, symPackages
|
|
|
|
\* Define symmetry sets
|
|
symUsers == Permutations(Users)
|
|
symTenants == Permutations(Tenants)
|
|
symPackages == Permutations(Packages)
|
|
|
|
\* Action constraints to focus on interesting behaviors
|
|
\* Uncomment to add action-specific bounds
|
|
\* ACTION_CONSTRAINT
|
|
\* \* Only allow one install at a time
|
|
\* Cardinality({op \in pendingOperations: op.type = "install"}) <= 1
|