running TLC on module imported with a parameterized INSTANCE

[tol...@gmail.com]

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?

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.