Checking FIFO module

[Y2i <yur...@xxxxxxxxx>]

When I run TLC Model checker on FIFO module from the Specifying Systems book, I get the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException: 
The configuration file did not specify the initial state predicate.
Can also be caused by trying to run TLC on a specification from
a module imported with a parameterized INSTANCE statement.

My configuration specified Temporal Formula: Spec and Message <- {1, 2}

Did I need to specify initial state predicate or is it because TLC does not support modules imported with parameterized INSTANCE statement?

I was able to run TLC on InnerFIFO which uses parameterized instantiation of Channel and my config file also did not have initial state predicate specified.  May be the reason is that FIFO uses  existential temporal quantifier?

Thank you in advance for your help.

Yuri

-------------------------------- MODULE FIFO --------------------------------
CONSTANT Message
VARIABLES in, out
Inner(q) == INSTANCE InnerFIFO
Spec == \EE q : Inner(q)!Spec
=============================================================================