Thank you, Leslie. Actually I figured out the answer to my second question without declaring other model values; after setting the model values {a1, a2, a3} to Address, I can just set a1 to Dummy as an ordinary value.
— Elliot
Open the Help Contents page, click on the "+" next to "TLA+ Toolbox
User Guide" and then the "+"s next to "Model Checking" and its
subsections. You will see a page called "Model Values and Symmetry".
Open it. About one screenful down you will find this paragraph
(underlined text is a link):
There are some uses of model values that can't be specified with the
What is the model? section of the Model Overview Page. If you
encounter such a problem, you can declare your own set of model values
with the Additional Definitions section of the Advanced Options Page
and then use them as ordinary values in expressions of the model.
Leslie
|