This project is read-only.
1

Closed

Sometimes Toolbox fails to report a TLC error arising from 'Evaluate Constant Expression'

description

(This is not terribly serious as there is a workaround, but it's clearly a bug so I'm reporting it anyway.)

I found a case in which the Toolbox does not show an error that is reported by TLC when doing ‘Evaluate Constant Expression’. I suspect this is related to the size of the error-output in the TLC console log.

The attached module contains a dumb bug; on line 52 the definition of the co-domain of a recursive function is too small.

When I use TLC to ‘Evaluate Constant Expression’ on the following:
TestAllShortestDistances
then

a. If the following values are used for constants, then the Toolbox fails to report the error, and does not print any output in “Value” box.
MaxNumEdgeWeights = 1
MaxNumNodes = 3

b. If the following smaller values are used for constants, then the Toolbox correctly reports the error.
MaxNumEdgeWeights = 1
MaxNumNodes = 2

In both cases, the TLC console log does contain the correct error.
I suspect this problem is related to the size of the error output in the log, as in case (a) above, the error report in the TLC console log is quite large, due to the combinatorics of this function definition.
In the extract from the log below, the “… snip lots of output ..” part hides the large part.

Version info

Windows 7 Enterprise

OS is 64-bit, but software is 32-bit.

32-bit Oracle Java 1.7:
java version "1.7.0_25"
Java(TM) SE Runtime Environment (build 1.7.0_25-b16)
Java HotSpot(TM) Client VM (build 23.25-b01, mixed mode)

32-bit Toolbox & TLC (TLAToolbox-1.4.7-win32.win32.x86)

This is Version 1.4.7 of 24 April 2013 and includes:
  • SANY Version 2.1 of 27 March 2013
  • TLC Version 2.05 of 24 October 2012
  • PlusCal Version 1.8 of 2 April 2013
  • TLATeX Version 1.0 of 12 April 2013
Chris

Starting... (2013-07-14 08:56:53)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2105:1 @!@!@
Evaluating assumption line 20, col 8 to line 20, col 66 of module MC failed.
In applying the function
[args \in ({(<<1, 1>> :> 1 @@ ... snip lots of output ...} X {{}, {1}, {2}, {3}, {1, 2}, {1, 3}, {2, 3}, {1, 2, 3}}) |-> <expression line 53, col 13 to line 66, col 62 of module ToolboxBug_FailureToReportErrorEvaluatingConstantExpression>],
the first argument is:
<< ( <<1, 1>> :> 999999999 @@
 <<1, 2>> :> 1 @@
 <<1, 3>> :> 999999999 @@
 <<2, 1>> :> 1 @@
 <<2, 2>> :> 2 @@
 <<2, 3>> :> 999999999 @@
 <<3, 1>> :> 999999999 @@
 <<3, 2>> :> 999999999 @@
 <<3, 3>> :> 999999999 ),
{2, 3} >>
which is not in its domain.

file attachments

Closed Oct 7, 2016 at 5:00 PM by mku
Closed as per last comment

comments

lamport wrote Jul 20, 2013 at 2:45 AM

This problem is fixed in the version of the source code that I checked in at about 18:40 PDT on 19 July 2013. The fix will appear in the next release.