Hello,--TLC cannot handle specifications that involve unbounded quantification or quantification over state variables. In your case, `q' is a state variable and Spec should really be defined asSpec == \EE q: Inner(q)!Init /\ [][BNext(q)]_<<in,out,q>>
where \EE denotes quantification over a state variable (i.e., a sequence of values). Such specifications are not handled by any of the existing verification tools for TLA+.Regards,StephanOn 1 Sep 2022, at 06:27, Anand Kumar <akkeshavan@xxxxxxxxx> wrote:Hi,"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>>
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/eb83eb50-5e91-4330-9e1b-9999a530e268n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/aASP2cDy1-c/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7C62B09E-48AE-4447-B935-BC6C0EB403F3%40gmail.com.