mirror of
https://github.com/johndoe6345789/metabuilder.git
synced 2026-04-24 13:54:57 +00:00
43 lines
1.2 KiB
Markdown
43 lines
1.2 KiB
Markdown
# Known Issues
|
|
|
|
## metabuilder.tla
|
|
|
|
**Issue**: Syntax error at line 323 in the PackageConsistency invariant.
|
|
|
|
**Error**:
|
|
```
|
|
line 323, col 47 to line 323, col 47 of module metabuilder
|
|
Unknown operator: `t'.
|
|
```
|
|
|
|
**Root Cause**: The quantification over `installedPackages[t]` assumes the function is defined for all tenants, but TLA+ requires explicit guarding.
|
|
|
|
**Status**: Pre-existing issue in the original specification. Not introduced by new specifications.
|
|
|
|
**Workaround**: The issue is in the core specification and should be addressed separately. The new future functionality specifications (workflow_system.tla, collaboration.tla, integrations.tla) all pass validation successfully.
|
|
|
|
**Suggested Fix**:
|
|
```tla
|
|
\* Current (line 322-324)
|
|
PackageConsistency ==
|
|
\A t \in Tenants, p \in installedPackages[t]:
|
|
packageStates[p] \in {"installed", "disabled", "installing"}
|
|
|
|
\* Suggested fix
|
|
PackageConsistency ==
|
|
\A t \in Tenants:
|
|
\A p \in installedPackages[t]:
|
|
packageStates[p] \in {"installed", "disabled", "installing"}
|
|
```
|
|
|
|
## Future Functionality Specifications
|
|
|
|
All new specifications pass validation:
|
|
- ✓ workflow_system.tla: PASSED
|
|
- ✓ collaboration.tla: PASSED
|
|
- ✓ integrations.tla: PASSED
|
|
|
|
---
|
|
|
|
*Last Updated*: 2025-12-27
|