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

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

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.