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

Re: [tlaplus] Re: How to use configuration file and how to set a specific model value

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.


On Jul 7, 2015, at 4:26 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

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
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.