fix: guard package consistency quantifier

2026-04-25 06:14:59 +00:00 · 2025-12-27 15:27:21 +00:00
1 changed files with 3 additions and 2 deletions
--- a/spec/metabuilder.tla
+++ b/spec/metabuilder.tla
@@ -320,8 +320,9 @@ DataConsistency ==
 \* Package consistency: installed packages must be in installed or disabled state
 PackageConsistency ==
-    \A t \in Tenants, p \in installedPackages[t]:
+    \A t \in Tenants:
-        packageStates[p] \in {"installed", "disabled", "installing"}
+        \A p \in installedPackages[t]:
            packageStates[p] \in {"installed", "disabled", "installing"}
 \* DBAL safety: no queries processed in error state
 DBALSafety ==