Re: Bug in TLC when checking if integer record field is element of integer range

[Andrew Helwer <andrew...@xxxxxxxxx>]

Ha, you're right. Error is Range == {1 .. 3} when I should have defined Range == 1 .. 3.

On Thursday, July 16, 2015 at 1:15:24 PM UTC-7, Leslie Lamport wrote:

Hi Andres,

TLC has been in use for over a dozen years.  It is very unlikely that
it has a bug that would manifest itself on such a simple task as
computing if a simple value is an element of a simple finite set.
TLC is correctly reporting an error.  Please try to figure out what
that error is.

Cheers,

Leslie