# TLC Restrictions ## Parameterized Instantiation Wrong ❌ ```tla IM(x) == INSTANCE M ISpec == IM(xbar)!Spec ``` Workaround ```tla IM == INSTANCE M WITH x <- xbar ISpec == IM!Spec ``` ## Unbound Quantifiers Wrong ❌ ```tla ASSUME \A p, d, miOld, miNew: /\ Send(p, d, miOld, miNew) \in BOOLEAN /\ Reply(p, d, miOld, miNew) \in BOOLEAN ``` ## Unbound `CHOOSE` Wrong ❌ ``` NotANat == CHOOSE n : n \notin Nat ``` Substitute a model value for `NotANat` in the model config file under `CONSTANTS`: ``` CONSTANTS NotANat = NotANat ```