[tlaplus] running TLC on module imported with a parameterized INSTANCE

[tollotp@xxxxxxxxx]

Hello everyone, i've just started practising with TLA, running the example in chapter 4, bounded FIFO, i encountered this error from the TLC:

"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.
"

the configuration of the model is:

N <- 5
Message <- {"a","b"}

Temporal formula : Spec

the .tla file is exactly as defined in the book,

could someone tell me why i encountered this error and what i can do for solve it?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7ccd80c7-4c7b-4146-b1f9-a106972fda6f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.