tlaplus
diff --git a/‎specifications/Huang/DyadicRationals.tla
-53 b/‎specifications/Huang/DyadicRationals.tla
-53
diff --git a/‎specifications/Huang/Huang.tla
+1-1 b/‎specifications/Huang/Huang.tla
+1-1
@@ -114,7 +114,7 @@ THEOREM Spec => Live
 
 StateConstraint ==
     \* Prevent the weights from halving towards infinity.
-    \A p \in Procs : weight[p].dem <= 8
+    \A p \in Procs : weight[p].den <= 8
 
 Alias ==
     [
Original file line number	Diff line number	Diff line change
`@@ -114,7 +114,7 @@ THEOREM Spec => Live`
`114`	`114`
`115`	`115`	`StateConstraint ==`
`116`	`116`	`\* Prevent the weights from halving towards infinity.`
`117`		`- \A p \in Procs : weight[p].dem <= 8`
	`117`	`+ \A p \in Procs : weight[p].den <= 8`
`118`	`118`
`119`	`119`	`Alias ==`
`120`	`120`	`[`