Cannot supply tuple as constant

Open dgpv opened this issue 5 years ago • 1 comments

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.

May 02 '20 18:05 dgpv

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.

Jul 20 '20 22:07 hwayne