"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."
This is my spec, what am I doing wrong? Similar error comes in the FIFO spec lso. I have checked your earlier answer, but that doesn;t seem to provide a solution. I understand the Professor Lamport prefers us to use the Hyperbook, but that gives a lot fo permission errors etc on a mac.
Sorry to trouble you with this-- but since i am new to this I would really appreciate the help.
EXTENDS Naturals, Sequences
CONSTANT Message,N
VARIABLES in, out
ASSUME (N \in Nat) /\ (N > 0 )
Inner(q) == INSTANCE InnerFIFO
BNext(q) ==
/\ Inner(q)! Next
/\ Inner(q)! BufReceive => (Len(q) < N )
Spec == \E q: Inner(q)!Init /\ [][BNext(q)]_<<in,out,q>>