fix: guard package consistency quantifier

2026-04-24 13:54:57 +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]:
-        packageStates[p] \in {"installed", "disabled", "installing"}
+    \A t \in Tenants:
+        \A p \in installedPackages[t]:
+            packageStates[p] \in {"installed", "disabled", "installing"}

 \* DBAL safety: no queries processed in error state
 DBALSafety ==