Re: Definition override in configuration file?

[Leslie Lamport <tlapl...@xxxxxxxxx>]

The use of TLC from a command line is described in the documentation of TLC in "Specifying Systems".  But it's easier to run TLC from the command line on the spec that the Toolbox runs for a model.  It is the spec named MC in a subdirectory of the .Toolbox directory whose name is derived from the model name.

Leslie

On Saturday, October 25, 2014 5:51:21 AM UTC-7, Christopher Meiklejohn wrote:

When running into the "Error: TLC encountered a non-enumerable quantifier bound" error, I've used the toolbox GUI to specify a specific bound for Nats.  However, I can not figure out how to specify the definition override in the .cfg file when running using the TLC model checker from the command line.

I'm assuming this is possible, but I just can't find how to do this in the documentation.

Any advice would be appreciated.

- Chris