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