[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Specifying Systems- BoundedFIFO error- Figure 4.2



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.