Dear All:
I am learning TLA+ from the book "Specifying Systems" by Leslie Lamport.
I am stuck with the specification of MemoryInterface, InternalMemory in Chapter 5 "A Caching Memory".
Specifically, when I created a model for InternalMemory, I was asked to specify the values of declared constants,
including 'Val', 'Proc', 'InitMemInt', 'Adr', 'Send(, , ,)', and 'Reply(, , ,)', as shown in the picture below (also in the attachment).
Problem 1: I have specified 'Val <- {1,2,3,4}', 'Proc <- {p1, p2, p3}', and 'Adr <- {a1, a2, a3}'. Are they OK?
However, I did not know how to specify 'InitMemInt', 'Send(, , ,)', or 'Reply(, , ,)'.
In the text (Page 47), it reads
"A specication that uses the memory interface can use the operators Send
and Reply to specify how the variable memInt changes. The specication must
also describememInt 's initial value. We therefore declare a constant parameter
InitMemInt that is the set of possible initial values of memInt ."
Problem 2: What is InitMemInt like?
As for 'Send(, , ,)' and 'Reply(, , ,)', the dialog for specifying values is shown in the picture below (also in the attachment).
Problem 3: How should I specify values for them?
Moreover, the second paragraph explains why we write 'Send(p, d, memInt, memInt')' instead of 'Send(p, d)'.
I am confused by the notion of "parameters".
Problem 4: Why is 'Send(p,d)' an action parameter, and why is not 'Send(p, d, memInt, memInt')'?
Best Regards.
hengxin