ERROR in specifications/SpecifyingSystems/Composing/CompositeFIFO.tla: In evaluation, the identifier in is either undefined or not an operator. about examples

[muenchnerkindl]

Although you do not indicate which specification you are running TLC on, it appears that you try to run it on Sender. However the real system specification is meant to be Spec at the bottom of the module, which includes Sender as a sub-formula. In particular, that specification fixes the possible values of in through the conjunct []IsChannel(in). See also the explanations in chapter 10.3 of Specifying Systems.

The problem with formula Spec is that it is not a specification in standard form

Init /\ [][Next]_v /\ L

and can therefore not be handled by TLC. This examples illustrates a general TLA+ specification but is not meant to be used with TLC.