Hello,
the specification from module BoundedFIFO is defined as
\EE q : Inner(q)!Init /\ [][BNext(q)]_<<in,out,q>>
and TLC does not support \EE, i.e. quantification over state variables. (I agree that the error message is not ideal.)
You'd typically launch TLC from module InnerFIFO and add a state constraint (see Model -> Advanced Options) in order to restrict the length of the queue in the states that TLC considers. To do this, add a predicate such as
Len(q) < 5
in the "State Constraint" field.
Regards,
Stephan