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

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



Hi,

I've some beginner's questions about the configuration file.

First, for the configuration file shown here:
http://research.microsoft.com/en-us/um/people/lamport/tla/DCAS.cfg

How should I use it with the TLA+ Toolbox? I searched for a while but couldn't find any instruction. I know there is a cfg file in the Spec's saving folder, but still replacing that file seems no obvious effect to me.

Second is that I know this configuration file just contains values for the CONSTANTS. So I think I can just assign these values to the constants under "What is the model?" in Model Overview. My problem is that I don't know how to set Dummy to be the Model value a1; the GUI dialog simply doesn't allow me to assign a value to Dummy if I chose Model value as its type.

Thanks!

--
Elliot