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

Confusion about the model of the specification of InternalMemory in Chapter 5 "A Caching Memory" of the book "Specifying Systems"

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 speci cation that uses the memory interface can use the operators Send
and Reply to specify how the variable memInt changes. The speci cation must
also describe
memInt '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.


Attachment: InternalMemoryModel.png
Description: PNG image

Attachment: InternalMemoryModel-Send.png
Description: PNG image