### Steps to Run

1. Download the VSCode Extension (https://marketplace.visualstudio.com/items?itemName=tlaplus.vscode-ide)
2. Put `WireAsync.tla` and `WireAsync.cfg` in the same file
3. Run VSCode command `TLA+ > Check Model With TLC`