Cannot supply tuple as constant

[dgpv]

While strings, numbers and sets work when supplied via --constant, tuples dont. (giving the error Error: TLC found an error in the configuration file at line 1. It was expecting = or <- and didn't find it.)

It has to be done via separate .tla file: https://stackoverflow.com/a/61564501/12029829

TLA+ toolbox generates MC.tla file in addition to MC.cfg and specifies all the values for constants inside MC.tla.

Readme for tlacli currently says that you can supply tuples via --constant. If this is desireable to be able to supply tuples via command line, it seems that tlacli has to generate temporary.tla file in addition to temporary.cfg. (btw, I think that they should be placed into TemporaryDirectory() instead of having hardcoded names, if paths are not specified explicitly.

[hwayne]

IIRC the problem with the TemporaryDirectory() I had was that it was hard to make sure the directory stayed available for the entire run of TLC, but I'll have to check my notes on that.