\* 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