Evaluate Constant Expression

This functionality may exist either constain on the Model Checking Results page of the Model Editor, or on its own page, depending on how the user has configured the Toolbox via the preferences.

Entering a constant expression in the Expression field of this section, and selecting the toggle button above and to the right of this field, will cause the value of that expression to appear in the Value field when TLC is run.  The expression can use any constant operators defined or declared in the spec or elsewhere in the model.  Used with the No behavior spec option on the Model Overview Page, this turns TLC into a mathematical calculator--one that computes arbitrary TLA+ expressions.