Re: Most often constants are model values

I would find that feature very inconvenient. Few of the constants in
my specs are model values, and assuming them to be by default would
make it hard to see if I've assigned proper values to all constants.

It wouldn't be hard to create a preference to do that, but I would

need some evidence that others would find it useful--or a proposal to

provide a choice of several such options.

Once you've created one model with assignments to all constants, it's
easy to create other models by cloning that model.

If you have so many constants that entering values for them is a problem,
you can write

   CONSTANT AllConstants
   Constant1 == AllConstants[1]
   ...
   Constant42 == AllConstants[42]

You can then assign AllConstants the value

<<ModelValue1, ... , ModelValue42>>

and in the Model Values section of the Advanced Options page add the set

{ModelValue1, ... , ModelValue42}

of model values. If your spec has so many constant parameters, it
might be made easier to understand by grouping those parameters in
some way.

Leslie Lamport

On Saturday, November 16, 2013 7:52:59 AM UTC-8, fl wrote:

A feature that I would find convenient is that every constant is assumed to be
a model value by default in the TLC model checker panel of toolbox.

Because I don't know if it is the case for you but my constants are in
most cases model values. And there are many of them and entering
them by hand is a nightmare.

--
FL