mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
Update TLA+ specifications and validation scripts
- Revised architecture alignment in README.md to reference JSON package format. - Enhanced SUMMARY.md with detailed specifications for workflow, collaboration, and integration systems. - Updated package_system.tla to include JSON package format and manifest path. - Modified validate-specs.sh to include package_system.tla in validation checks.
This commit is contained in:
@@ -365,9 +365,9 @@ ExecuteWorkflow(user, workflow) ==
|
||||
```
|
||||
|
||||
## Architecture Alignment
|
||||
|
||||
`storybook/JSON_PACKAGES.md` → JSON package format and discovery
|
||||
This specification aligns with the MetaBuilder architecture documentation:
|
||||
|
||||
`storybook/JSON_PACKAGES.md` → JSON package format and discovery
|
||||
- `docs/architecture/security-docs/5-level-system.md` → Permission model (extended to 6 levels)
|
||||
- `schemas/package-schemas/` → **16+ JSON schemas defining package structure**
|
||||
- `docs/packages/package-sources.md` → **Multi-source package loading architecture**
|
||||
|
||||
516
spec/SUMMARY.md
516
spec/SUMMARY.md
@@ -1,258 +1,258 @@
|
||||
# TLA+ Specifications Summary
|
||||
|
||||
## Overview
|
||||
|
||||
This directory contains formal TLA+ specifications for MetaBuilder, including both the current core system and three major future functionality areas. All specifications have been validated with TLA+ tools.
|
||||
|
||||
## What Was Created
|
||||
|
||||
### New Specifications (December 2025)
|
||||
|
||||
Three comprehensive TLA+ modules for future functionality:
|
||||
|
||||
| Specification | Lines | Operations | Properties | Status |
|
||||
|---------------|-------|------------|------------|--------|
|
||||
| `workflow_system.tla` | 595 | 22 | 12 (9 safety + 3 liveness) | ✅ Validated |
|
||||
| `collaboration.tla` | 546 | 26 | 13 (10 safety + 3 liveness) | ✅ Validated |
|
||||
| `integrations.tla` | 644 | 28 | 13 (10 safety + 3 liveness) | ✅ Validated |
|
||||
| **Total** | **1,785** | **76** | **38** | |
|
||||
|
||||
### Supporting Files
|
||||
|
||||
- **Configuration Files**: 3 `.cfg` files for model checking
|
||||
- **Documentation**: Updated `README.md` with comprehensive module documentation
|
||||
- **Quick Reference**: `QUICK_REFERENCE.md` for developer workflows
|
||||
- **Validation Script**: `validate-specs.sh` for automated syntax checking
|
||||
- **Known Issues**: `KNOWN_ISSUES.md` documenting pre-existing core spec issue
|
||||
|
||||
## Specifications Detail
|
||||
|
||||
### 1. Workflow System (`workflow_system.tla`)
|
||||
|
||||
**Purpose**: Formal specification for advanced workflow execution features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- Template lifecycle (create, activate, archive)
|
||||
- Manual and scheduled execution
|
||||
- Step dependencies with parallel execution
|
||||
- Configurable retry logic (MaxRetries)
|
||||
- Per-tenant concurrency limits (MaxConcurrentRuns)
|
||||
|
||||
**Safety Properties**:
|
||||
1. GodOnlyTemplateCreation - Only Level 5+ can author templates
|
||||
2. AdminOnlyExecution - Only Level 4+ can execute workflows
|
||||
3. TenantIsolation - Workflows isolated by tenant
|
||||
4. ConcurrencyLimit - Per-tenant execution limits enforced
|
||||
5. RetryLimit - Failed steps don't exceed retry threshold
|
||||
6. NoOverlap - Running and completed workflows don't overlap
|
||||
7. DependencyEnforcement - Step dependencies respected
|
||||
8. AuditCompleteness - All operations logged
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualStepExecution - Pending steps eventually execute
|
||||
2. EventualCompletion - Running workflows eventually complete/fail
|
||||
3. EventualScheduleTrigger - Scheduled workflows eventually trigger
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 3 workflow templates, 3 steps
|
||||
- Max 3 retries, max 2 concurrent runs per tenant
|
||||
- Bounded to 15 audit log entries, 5 instances
|
||||
|
||||
### 2. Collaboration System (`collaboration.tla`)
|
||||
|
||||
**Purpose**: Formal specification for real-time collaboration features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- User session states (active, idle, disconnected)
|
||||
- Concurrent document editing
|
||||
- Comments and @mentions
|
||||
- Real-time presence tracking
|
||||
- Notification system
|
||||
- Document version history
|
||||
|
||||
**Safety Properties**:
|
||||
1. DocumentTenantIsolation - Editors only access own tenant docs
|
||||
2. ConcurrentEditorLimit - Max concurrent editors enforced
|
||||
3. CommentTenantConsistency - Comments belong to doc tenant
|
||||
4. MentionTenantIsolation - Mentions within tenant boundaries
|
||||
5. NotificationLimit - Pending notifications don't exceed limit
|
||||
6. ActiveEditorsOnly - Only active users can edit
|
||||
7. DisconnectedNotEditing - Disconnected users auto-stop editing
|
||||
8. OperationAuthorship - All ops from authorized editors
|
||||
9. VersionConsistency - Version snapshots preserve content
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualNotificationHandling - Notifications eventually read/cleared
|
||||
2. EventualMentionRead - Mentions eventually seen
|
||||
3. EventualStopEditing - Active editors eventually stop/disconnect
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 2 documents
|
||||
- Max 3 concurrent editors, max 10 notifications
|
||||
- Bounded to 5 comments, 5 mentions, 12 activity feed entries
|
||||
|
||||
### 3. Integration Ecosystem (`integrations.tla`)
|
||||
|
||||
**Purpose**: Formal specification for integration features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- Webhook management and delivery
|
||||
- OAuth application framework
|
||||
- API key lifecycle management
|
||||
- Event subscriptions and filtering
|
||||
- Rate limiting per identity
|
||||
- Retry logic for webhook delivery
|
||||
|
||||
**Safety Properties**:
|
||||
1. AdminOnlyIntegrationManagement - Only Level 4+ manage integrations
|
||||
2. WebhookTenantLimit - Webhooks per tenant limited
|
||||
3. APIKeyUserLimit - API keys per user limited
|
||||
4. RateLimitEnforcement - Rate limits enforced
|
||||
5. WebhookTenantIsolation - Webhooks isolated by tenant
|
||||
6. OAuthAppTenantIsolation - OAuth apps isolated by tenant
|
||||
7. APIKeyTenantIsolation - API keys isolated by tenant
|
||||
8. TokenTenantConsistency - OAuth tokens match app tenants
|
||||
9. ActiveDeliveriesQueued - Active deliveries properly queued
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualDeliveryCompletion - Deliveries eventually complete/fail
|
||||
2. EventualRetryOrFail - Failed deliveries retry or permanently fail
|
||||
3. EventualExpiration - Expired keys eventually marked expired
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 3 webhooks, 2 OAuth apps, 3 API keys, 3 event types
|
||||
- Max 2 webhooks/tenant, 2 keys/user, 100 calls/hour
|
||||
- Bounded to 15 audit entries, 5 queue items, 6 deliveries
|
||||
|
||||
## Common Properties Across All Specs
|
||||
|
||||
### Multi-Tenant Isolation
|
||||
Every specification enforces strict tenant isolation:
|
||||
- Users can only access resources in their tenant
|
||||
- All operations filter by tenantId
|
||||
- Cross-tenant access is impossible by design
|
||||
|
||||
### Permission Hierarchy
|
||||
All specs respect the 6-level hierarchy:
|
||||
1. Public (Level 1) - Unauthenticated, read-only
|
||||
2. User (Level 2) - Basic authenticated operations
|
||||
3. Moderator (Level 3) - Content moderation
|
||||
4. Admin (Level 4) - Integration management, workflow execution
|
||||
5. God (Level 5) - Workflow authoring, advanced features
|
||||
6. Supergod (Level 6) - Complete system control
|
||||
|
||||
### Audit Logging
|
||||
Every privileged operation is logged with:
|
||||
- User performing the action
|
||||
- Action type
|
||||
- Target resource
|
||||
- Tenant context
|
||||
- Timestamp
|
||||
|
||||
## Validation Status
|
||||
|
||||
Validated using TLA+ tools v1.8.0 (tla2tools.jar):
|
||||
|
||||
```bash
|
||||
./validate-specs.sh
|
||||
```
|
||||
|
||||
**Results**:
|
||||
- ✅ workflow_system.tla: PASSED
|
||||
- ✅ collaboration.tla: PASSED
|
||||
- ✅ integrations.tla: PASSED
|
||||
- ⚠️ metabuilder.tla: Pre-existing syntax error (line 323)
|
||||
|
||||
The pre-existing error in metabuilder.tla is documented in `KNOWN_ISSUES.md` and does not affect the new specifications.
|
||||
|
||||
## Using These Specifications
|
||||
|
||||
### For Design Review
|
||||
1. Review state transitions before implementation
|
||||
2. Identify race conditions and deadlocks
|
||||
3. Verify permission enforcement is complete
|
||||
4. Ensure multi-tenant isolation is maintained
|
||||
|
||||
### For Implementation
|
||||
1. Map specification states to code structures
|
||||
2. Use operations as API contract definitions
|
||||
3. Implement invariants as runtime assertions
|
||||
4. Follow state transition logic
|
||||
|
||||
### For Testing
|
||||
1. Use safety properties as test requirements
|
||||
2. Create property-based tests from invariants
|
||||
3. Test edge cases identified in specifications
|
||||
4. Validate liveness properties with integration tests
|
||||
|
||||
### Running Model Checker
|
||||
|
||||
```bash
|
||||
# Download TLA+ tools
|
||||
wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
|
||||
|
||||
# Check syntax
|
||||
java -cp tla2tools.jar tla2sany.SANY spec/workflow_system.tla
|
||||
|
||||
# Run model checker (may take several minutes)
|
||||
java -cp tla2tools.jar tlc2.TLC spec/workflow_system.tla -config spec/workflow_system.cfg
|
||||
```
|
||||
|
||||
## Architecture Alignment
|
||||
|
||||
These specifications align with MetaBuilder's architecture:
|
||||
|
||||
| Specification | Architecture Docs |
|
||||
|---------------|-------------------|
|
||||
| `workflow_system.tla` | `docs/todo/improvements/20-FUTURE-FEATURES-TODO.md` (Workflow Features) |
|
||||
| `collaboration.tla` | `docs/todo/improvements/20-FUTURE-FEATURES-TODO.md` (Collaboration Features) |
|
||||
| `integrations.tla` | `docs/todo/improvements/20-FUTURE-FEATURES-TODO.md` (Integration Ecosystem) |
|
||||
| All specs | `docs/architecture/security-docs/5-level-system.md` (Permissions) |
|
||||
| All specs | `docs/architecture/data/data-driven-architecture.md` (Multi-tenancy) |
|
||||
|
||||
## Benefits
|
||||
|
||||
These formal specifications provide:
|
||||
|
||||
1. **Early Bug Detection**: Find race conditions before implementation
|
||||
2. **Clear Contracts**: Precise API behavior definitions
|
||||
3. **Security Validation**: Verify permission and isolation properties
|
||||
4. **Implementation Guide**: Clear state machines to implement
|
||||
5. **Test Blueprint**: Property-based testing requirements
|
||||
6. **Documentation**: Precise system behavior description
|
||||
7. **Design Tool**: Explore alternatives before coding
|
||||
8. **Regression Prevention**: Detect when changes violate invariants
|
||||
|
||||
## Resources
|
||||
|
||||
- **Main Documentation**: `spec/README.md`
|
||||
- **Quick Reference**: `spec/QUICK_REFERENCE.md`
|
||||
- **Known Issues**: `spec/KNOWN_ISSUES.md`
|
||||
- **Validation Script**: `spec/validate-specs.sh`
|
||||
- **TLA+ Homepage**: https://lamport.azurewebsites.net/tla/tla.html
|
||||
- **Learn TLA+**: https://learntla.com/
|
||||
|
||||
## Maintenance
|
||||
|
||||
When implementing these features:
|
||||
|
||||
1. ✅ Review the relevant TLA+ specification first
|
||||
2. ✅ Use state transitions as requirements
|
||||
3. ✅ Implement property-based tests
|
||||
4. ✅ Validate multi-tenant isolation
|
||||
5. ✅ Update spec if design changes
|
||||
|
||||
When modifying specifications:
|
||||
|
||||
1. Update the `.tla` file with changes
|
||||
2. Run `./validate-specs.sh` to check syntax
|
||||
3. Run model checker to verify properties still hold
|
||||
4. Update documentation if needed
|
||||
5. Document any new invariants or properties
|
||||
|
||||
---
|
||||
|
||||
*Created*: 2025-12-27
|
||||
*Status*: Complete and Validated
|
||||
*TLA+ Version*: 1.8.0
|
||||
*MetaBuilder Version*: Iteration 25+
|
||||
# TLA+ Specifications Summary
|
||||
|
||||
## Overview
|
||||
|
||||
This directory contains formal TLA+ specifications for MetaBuilder, including both the current core system and three major future functionality areas. All specifications have been validated with TLA+ tools.
|
||||
|
||||
## What Was Created
|
||||
|
||||
### New Specifications (December 2025)
|
||||
|
||||
Three comprehensive TLA+ modules for future functionality:
|
||||
|
||||
| Specification | Lines | Operations | Properties | Status |
|
||||
|---------------|-------|------------|------------|--------|
|
||||
| `workflow_system.tla` | 595 | 22 | 12 (9 safety + 3 liveness) | ✅ Validated |
|
||||
| `collaboration.tla` | 546 | 26 | 13 (10 safety + 3 liveness) | ✅ Validated |
|
||||
| `integrations.tla` | 644 | 28 | 13 (10 safety + 3 liveness) | ✅ Validated |
|
||||
| **Total** | **1,785** | **76** | **38** | |
|
||||
|
||||
### Supporting Files
|
||||
|
||||
- **Configuration Files**: 3 `.cfg` files for model checking
|
||||
- **Documentation**: Updated `README.md` with comprehensive module documentation
|
||||
- **Quick Reference**: `QUICK_REFERENCE.md` for developer workflows
|
||||
- **Validation Script**: `validate-specs.sh` for automated syntax checking
|
||||
- **Known Issues**: `KNOWN_ISSUES.md` documenting pre-existing core spec issue
|
||||
|
||||
## Specifications Detail
|
||||
|
||||
### 1. Workflow System (`workflow_system.tla`)
|
||||
|
||||
**Purpose**: Formal specification for advanced workflow execution features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- Template lifecycle (create, activate, archive)
|
||||
- Manual and scheduled execution
|
||||
- Step dependencies with parallel execution
|
||||
- Configurable retry logic (MaxRetries)
|
||||
- Per-tenant concurrency limits (MaxConcurrentRuns)
|
||||
|
||||
**Safety Properties**:
|
||||
1. GodOnlyTemplateCreation - Only Level 5+ can author templates
|
||||
2. AdminOnlyExecution - Only Level 4+ can execute workflows
|
||||
3. TenantIsolation - Workflows isolated by tenant
|
||||
4. ConcurrencyLimit - Per-tenant execution limits enforced
|
||||
5. RetryLimit - Failed steps don't exceed retry threshold
|
||||
6. NoOverlap - Running and completed workflows don't overlap
|
||||
7. DependencyEnforcement - Step dependencies respected
|
||||
8. AuditCompleteness - All operations logged
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualStepExecution - Pending steps eventually execute
|
||||
2. EventualCompletion - Running workflows eventually complete/fail
|
||||
3. EventualScheduleTrigger - Scheduled workflows eventually trigger
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 3 workflow templates, 3 steps
|
||||
- Max 3 retries, max 2 concurrent runs per tenant
|
||||
- Bounded to 15 audit log entries, 5 instances
|
||||
|
||||
### 2. Collaboration System (`collaboration.tla`)
|
||||
|
||||
**Purpose**: Formal specification for real-time collaboration features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- User session states (active, idle, disconnected)
|
||||
- Concurrent document editing
|
||||
- Comments and @mentions
|
||||
- Real-time presence tracking
|
||||
- Notification system
|
||||
- Document version history
|
||||
|
||||
**Safety Properties**:
|
||||
1. DocumentTenantIsolation - Editors only access own tenant docs
|
||||
2. ConcurrentEditorLimit - Max concurrent editors enforced
|
||||
3. CommentTenantConsistency - Comments belong to doc tenant
|
||||
4. MentionTenantIsolation - Mentions within tenant boundaries
|
||||
5. NotificationLimit - Pending notifications don't exceed limit
|
||||
6. ActiveEditorsOnly - Only active users can edit
|
||||
7. DisconnectedNotEditing - Disconnected users auto-stop editing
|
||||
8. OperationAuthorship - All ops from authorized editors
|
||||
9. VersionConsistency - Version snapshots preserve content
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualNotificationHandling - Notifications eventually read/cleared
|
||||
2. EventualMentionRead - Mentions eventually seen
|
||||
3. EventualStopEditing - Active editors eventually stop/disconnect
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 2 documents
|
||||
- Max 3 concurrent editors, max 10 notifications
|
||||
- Bounded to 5 comments, 5 mentions, 12 activity feed entries
|
||||
|
||||
### 3. Integration Ecosystem (`integrations.tla`)
|
||||
|
||||
**Purpose**: Formal specification for integration features (from TODO 20).
|
||||
|
||||
**Key Features**:
|
||||
- Webhook management and delivery
|
||||
- OAuth application framework
|
||||
- API key lifecycle management
|
||||
- Event subscriptions and filtering
|
||||
- Rate limiting per identity
|
||||
- Retry logic for webhook delivery
|
||||
|
||||
**Safety Properties**:
|
||||
1. AdminOnlyIntegrationManagement - Only Level 4+ manage integrations
|
||||
2. WebhookTenantLimit - Webhooks per tenant limited
|
||||
3. APIKeyUserLimit - API keys per user limited
|
||||
4. RateLimitEnforcement - Rate limits enforced
|
||||
5. WebhookTenantIsolation - Webhooks isolated by tenant
|
||||
6. OAuthAppTenantIsolation - OAuth apps isolated by tenant
|
||||
7. APIKeyTenantIsolation - API keys isolated by tenant
|
||||
8. TokenTenantConsistency - OAuth tokens match app tenants
|
||||
9. ActiveDeliveriesQueued - Active deliveries properly queued
|
||||
|
||||
**Liveness Properties**:
|
||||
1. EventualDeliveryCompletion - Deliveries eventually complete/fail
|
||||
2. EventualRetryOrFail - Failed deliveries retry or permanently fail
|
||||
3. EventualExpiration - Expired keys eventually marked expired
|
||||
|
||||
**Model Checking Configuration**:
|
||||
- 3 users, 2 tenants, 3 webhooks, 2 OAuth apps, 3 API keys, 3 event types
|
||||
- Max 2 webhooks/tenant, 2 keys/user, 100 calls/hour
|
||||
- Bounded to 15 audit entries, 5 queue items, 6 deliveries
|
||||
|
||||
## Common Properties Across All Specs
|
||||
|
||||
### Multi-Tenant Isolation
|
||||
Every specification enforces strict tenant isolation:
|
||||
- Users can only access resources in their tenant
|
||||
- All operations filter by tenantId
|
||||
- Cross-tenant access is impossible by design
|
||||
|
||||
### Permission Hierarchy
|
||||
All specs respect the 6-level hierarchy:
|
||||
1. Public (Level 1) - Unauthenticated, read-only
|
||||
2. User (Level 2) - Basic authenticated operations
|
||||
3. Moderator (Level 3) - Content moderation
|
||||
4. Admin (Level 4) - Integration management, workflow execution
|
||||
5. God (Level 5) - Workflow authoring, advanced features
|
||||
6. Supergod (Level 6) - Complete system control
|
||||
|
||||
### Audit Logging
|
||||
Every privileged operation is logged with:
|
||||
- User performing the action
|
||||
- Action type
|
||||
- Target resource
|
||||
- Tenant context
|
||||
- Timestamp
|
||||
|
||||
## Validation Status
|
||||
|
||||
Validated using TLA+ tools v1.8.0 (tla2tools.jar):
|
||||
|
||||
```bash
|
||||
./validate-specs.sh
|
||||
```
|
||||
|
||||
**Results**:
|
||||
- ✅ workflow_system.tla: PASSED
|
||||
- ✅ collaboration.tla: PASSED
|
||||
- ✅ integrations.tla: PASSED
|
||||
- ⚠️ metabuilder.tla: Pre-existing syntax error (line 323)
|
||||
|
||||
The pre-existing error in metabuilder.tla is documented in `KNOWN_ISSUES.md` and does not affect the new specifications.
|
||||
|
||||
## Using These Specifications
|
||||
|
||||
### For Design Review
|
||||
1. Review state transitions before implementation
|
||||
2. Identify race conditions and deadlocks
|
||||
3. Verify permission enforcement is complete
|
||||
4. Ensure multi-tenant isolation is maintained
|
||||
|
||||
### For Implementation
|
||||
1. Map specification states to code structures
|
||||
2. Use operations as API contract definitions
|
||||
3. Implement invariants as runtime assertions
|
||||
4. Follow state transition logic
|
||||
|
||||
### For Testing
|
||||
1. Use safety properties as test requirements
|
||||
2. Create property-based tests from invariants
|
||||
3. Test edge cases identified in specifications
|
||||
4. Validate liveness properties with integration tests
|
||||
|
||||
### Running Model Checker
|
||||
|
||||
```bash
|
||||
# Download TLA+ tools
|
||||
wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
|
||||
|
||||
# Check syntax
|
||||
java -cp tla2tools.jar tla2sany.SANY spec/workflow_system.tla
|
||||
|
||||
# Run model checker (may take several minutes)
|
||||
java -cp tla2tools.jar tlc2.TLC spec/workflow_system.tla -config spec/workflow_system.cfg
|
||||
```
|
||||
|
||||
## Architecture Alignment
|
||||
|
||||
These specifications align with MetaBuilder's architecture:
|
||||
|
||||
| Specification | Architecture Docs |
|
||||
|---------------|-------------------|
|
||||
| `workflow_system.tla` | `storybook/JSON_PACKAGES.md` (Workflow Features & JSON packages) |
|
||||
| `collaboration.tla` | `storybook/JSON_PACKAGES.md` (Collaboration Features & JSON packages) |
|
||||
| `integrations.tla` | `storybook/JSON_PACKAGES.md` (Integration Ecosystem & JSON packages) |
|
||||
| All specs | `docs/architecture/security-docs/5-level-system.md` (Permissions) |
|
||||
| All specs | `docs/architecture/data/data-driven-architecture.md` (Multi-tenancy) |
|
||||
|
||||
## Benefits
|
||||
|
||||
These formal specifications provide:
|
||||
|
||||
1. **Early Bug Detection**: Find race conditions before implementation
|
||||
2. **Clear Contracts**: Precise API behavior definitions
|
||||
3. **Security Validation**: Verify permission and isolation properties
|
||||
4. **Implementation Guide**: Clear state machines to implement
|
||||
5. **Test Blueprint**: Property-based testing requirements
|
||||
6. **Documentation**: Precise system behavior description
|
||||
7. **Design Tool**: Explore alternatives before coding
|
||||
8. **Regression Prevention**: Detect when changes violate invariants
|
||||
|
||||
## Resources
|
||||
|
||||
- **Main Documentation**: `spec/README.md`
|
||||
- **Quick Reference**: `spec/QUICK_REFERENCE.md`
|
||||
- **Known Issues**: `spec/KNOWN_ISSUES.md`
|
||||
- **Validation Script**: `spec/validate-specs.sh`
|
||||
- **TLA+ Homepage**: https://lamport.azurewebsites.net/tla/tla.html
|
||||
- **Learn TLA+**: https://learntla.com/
|
||||
|
||||
## Maintenance
|
||||
|
||||
When implementing these features:
|
||||
|
||||
1. ✅ Review the relevant TLA+ specification first
|
||||
2. ✅ Use state transitions as requirements
|
||||
3. ✅ Implement property-based tests
|
||||
4. ✅ Validate multi-tenant isolation
|
||||
5. ✅ Update spec if design changes
|
||||
|
||||
When modifying specifications:
|
||||
|
||||
1. Update the `.tla` file with changes
|
||||
2. Run `./validate-specs.sh` to check syntax
|
||||
3. Run model checker to verify properties still hold
|
||||
4. Update documentation if needed
|
||||
5. Document any new invariants or properties
|
||||
|
||||
---
|
||||
|
||||
*Created*: 2025-12-27
|
||||
*Status*: Complete and Validated
|
||||
*TLA+ Version*: 1.8.0
|
||||
*MetaBuilder Version*: Iteration 25+
|
||||
|
||||
@@ -12,8 +12,8 @@
|
||||
* *
|
||||
* Aligned with: *
|
||||
* - schemas/package-schemas/*.json *
|
||||
* - docs/packages/package-sources.md *
|
||||
* - packages/*/package.json structure *
|
||||
* - storybook/JSON_PACKAGES.md (JSON package format and discovery) *
|
||||
* - packages/*/package.json or packages/*/seed/metadata.json *
|
||||
***************************************************************************)
|
||||
|
||||
EXTENDS Naturals, Sequences, FiniteSets, TLC
|
||||
@@ -112,7 +112,9 @@ PackageIndexEntry == [
|
||||
minLevel: PermissionLevel,
|
||||
category: PackageCategory,
|
||||
source: PackageSources,
|
||||
dependencies: SUBSET Packages
|
||||
dependencies: SUBSET Packages,
|
||||
format: {"json"}, \* Package format (JSON-based packages)
|
||||
manifestPath: STRING \* Path to package manifest (package.json or seed metadata)
|
||||
]
|
||||
|
||||
\* Full package entry in registry
|
||||
@@ -125,13 +127,16 @@ PackageEntry == [
|
||||
source: PackageSources,
|
||||
state: PackageState,
|
||||
dependencies: SUBSET Packages,
|
||||
\* For JSON-based packages the manifest contains exports and metadata
|
||||
manifestPath: STRING,
|
||||
exports: [
|
||||
components: SUBSET STRING,
|
||||
scripts: SUBSET STRING,
|
||||
types: SUBSET STRING
|
||||
],
|
||||
validated: BOOLEAN,
|
||||
installedAt: Nat \cup {0}
|
||||
installedAt: Nat \cup {0},
|
||||
format: {"json"}
|
||||
]
|
||||
|
||||
\* Pending operation
|
||||
|
||||
@@ -1,94 +1,95 @@
|
||||
#!/bin/bash
|
||||
# Validate TLA+ Specifications
|
||||
# This script checks the syntax of all TLA+ specifications in the spec directory
|
||||
|
||||
set -e
|
||||
|
||||
SPEC_DIR="$(dirname "$0")"
|
||||
TLA_TOOLS="${TLA_TOOLS:-/tmp/tla2tools.jar}"
|
||||
|
||||
# Color output
|
||||
RED='\033[0;31m'
|
||||
GREEN='\033[0;32m'
|
||||
YELLOW='\033[1;33m'
|
||||
NC='\033[0m' # No Color
|
||||
|
||||
echo "TLA+ Specification Validator"
|
||||
echo "============================="
|
||||
echo ""
|
||||
|
||||
# Check if TLA+ tools are available
|
||||
if [ ! -f "$TLA_TOOLS" ]; then
|
||||
echo -e "${YELLOW}TLA+ tools not found at $TLA_TOOLS${NC}"
|
||||
echo "Downloading TLA+ tools..."
|
||||
wget -q -O "$TLA_TOOLS" https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
|
||||
if [ $? -eq 0 ]; then
|
||||
echo -e "${GREEN}✓ Downloaded TLA+ tools${NC}"
|
||||
else
|
||||
echo -e "${RED}✗ Failed to download TLA+ tools${NC}"
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
|
||||
# Check Java
|
||||
if ! command -v java &> /dev/null; then
|
||||
echo -e "${RED}✗ Java not found. Please install Java 11 or later.${NC}"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
echo "Using TLA+ tools: $TLA_TOOLS"
|
||||
echo ""
|
||||
|
||||
# List of specifications to validate
|
||||
SPECS=(
|
||||
"metabuilder.tla"
|
||||
"workflow_system.tla"
|
||||
"collaboration.tla"
|
||||
"integrations.tla"
|
||||
)
|
||||
|
||||
FAILED=0
|
||||
PASSED=0
|
||||
|
||||
# Validate each specification
|
||||
for spec in "${SPECS[@]}"; do
|
||||
spec_path="$SPEC_DIR/$spec"
|
||||
|
||||
if [ ! -f "$spec_path" ]; then
|
||||
echo -e "${YELLOW}⚠ Skipping $spec (file not found)${NC}"
|
||||
continue
|
||||
fi
|
||||
|
||||
echo "Validating $spec..."
|
||||
|
||||
# Run SANY (syntax and semantic analyzer)
|
||||
output=$(java -cp "$TLA_TOOLS" tla2sany.SANY "$spec_path" 2>&1)
|
||||
|
||||
# Check for errors
|
||||
if echo "$output" | grep -q "Semantic errors:" || echo "$output" | grep -q "Parsing or semantic analysis failed."; then
|
||||
echo -e "${RED}✗ $spec: FAILED${NC}"
|
||||
echo "$output" | grep -A 10 "Semantic errors:"
|
||||
FAILED=$((FAILED + 1))
|
||||
else
|
||||
echo -e "${GREEN}✓ $spec: PASSED${NC}"
|
||||
PASSED=$((PASSED + 1))
|
||||
fi
|
||||
|
||||
echo ""
|
||||
done
|
||||
|
||||
# Summary
|
||||
echo "============================="
|
||||
echo "Validation Summary"
|
||||
echo "============================="
|
||||
echo -e "${GREEN}Passed: $PASSED${NC}"
|
||||
echo -e "${RED}Failed: $FAILED${NC}"
|
||||
echo ""
|
||||
|
||||
if [ $FAILED -eq 0 ]; then
|
||||
echo -e "${GREEN}All specifications are valid!${NC}"
|
||||
exit 0
|
||||
else
|
||||
echo -e "${RED}Some specifications have errors. Please review the output above.${NC}"
|
||||
exit 1
|
||||
fi
|
||||
#!/bin/bash
|
||||
# Validate TLA+ Specifications
|
||||
# This script checks the syntax of all TLA+ specifications in the spec directory
|
||||
|
||||
set -e
|
||||
|
||||
SPEC_DIR="$(dirname "$0")"
|
||||
TLA_TOOLS="${TLA_TOOLS:-/tmp/tla2tools.jar}"
|
||||
|
||||
# Color output
|
||||
RED='\033[0;31m'
|
||||
GREEN='\033[0;32m'
|
||||
YELLOW='\033[1;33m'
|
||||
NC='\033[0m' # No Color
|
||||
|
||||
echo "TLA+ Specification Validator"
|
||||
echo "============================="
|
||||
echo ""
|
||||
|
||||
# Check if TLA+ tools are available
|
||||
if [ ! -f "$TLA_TOOLS" ]; then
|
||||
echo -e "${YELLOW}TLA+ tools not found at $TLA_TOOLS${NC}"
|
||||
echo "Downloading TLA+ tools..."
|
||||
wget -q -O "$TLA_TOOLS" https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
|
||||
if [ $? -eq 0 ]; then
|
||||
echo -e "${GREEN}✓ Downloaded TLA+ tools${NC}"
|
||||
else
|
||||
echo -e "${RED}✗ Failed to download TLA+ tools${NC}"
|
||||
exit 1
|
||||
fi
|
||||
fi
|
||||
|
||||
# Check Java
|
||||
if ! command -v java &> /dev/null; then
|
||||
echo -e "${RED}✗ Java not found. Please install Java 11 or later.${NC}"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
echo "Using TLA+ tools: $TLA_TOOLS"
|
||||
echo ""
|
||||
|
||||
# List of specifications to validate
|
||||
SPECS=(
|
||||
"metabuilder.tla"
|
||||
"workflow_system.tla"
|
||||
"collaboration.tla"
|
||||
"integrations.tla"
|
||||
"package_system.tla"
|
||||
)
|
||||
|
||||
FAILED=0
|
||||
PASSED=0
|
||||
|
||||
# Validate each specification
|
||||
for spec in "${SPECS[@]}"; do
|
||||
spec_path="$SPEC_DIR/$spec"
|
||||
|
||||
if [ ! -f "$spec_path" ]; then
|
||||
echo -e "${YELLOW}⚠ Skipping $spec (file not found)${NC}"
|
||||
continue
|
||||
fi
|
||||
|
||||
echo "Validating $spec..."
|
||||
|
||||
# Run SANY (syntax and semantic analyzer)
|
||||
output=$(java -cp "$TLA_TOOLS" tla2sany.SANY "$spec_path" 2>&1)
|
||||
|
||||
# Check for errors
|
||||
if echo "$output" | grep -q "Semantic errors:" || echo "$output" | grep -q "Parsing or semantic analysis failed."; then
|
||||
echo -e "${RED}✗ $spec: FAILED${NC}"
|
||||
echo "$output" | grep -A 10 "Semantic errors:"
|
||||
FAILED=$((FAILED + 1))
|
||||
else
|
||||
echo -e "${GREEN}✓ $spec: PASSED${NC}"
|
||||
PASSED=$((PASSED + 1))
|
||||
fi
|
||||
|
||||
echo ""
|
||||
done
|
||||
|
||||
# Summary
|
||||
echo "============================="
|
||||
echo "Validation Summary"
|
||||
echo "============================="
|
||||
echo -e "${GREEN}Passed: $PASSED${NC}"
|
||||
echo -e "${RED}Failed: $FAILED${NC}"
|
||||
echo ""
|
||||
|
||||
if [ $FAILED -eq 0 ]; then
|
||||
echo -e "${GREEN}All specifications are valid!${NC}"
|
||||
exit 0
|
||||
else
|
||||
echo -e "${RED}Some specifications have errors. Please review the output above.${NC}"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
Reference in New Issue
Block a user