# TLC Restrictions
## Metadata
**Status**:: #x
**Zettel**:: #zettel/fleeting
**Created**:: [[2026-01-12]]
**Parent**:: [[TLC Model Checker]]
## 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
```