A few issues with TLC

[Giuliano <giulia...@xxxxxxx>]

Hello,

I have used TLC quite a bit in the past few weeks and it has been incredibly useful to understand my specs and find errors.

Many thanks to those who developed it.

I only stumbled on a few issues that did not prevent me from checking my specifications but which were unpleasant to work around. Here they are:

* TLC cannot evaluate x' = something when x is not a variable and it would be handy to do it when x it is a sequence or record composed of variables for example.

* Evaluating UNCHANGED x when a formula of the form "x' = something" has been evaluated before by TLC causes an error. This is useful to spot actions of the form

/\ x' = x + 1

/\ UNCHANGED x',

which are probably an error in the specification.

However, when composing specification interacting through variable x,  I often write actions of the form

/\  \/ Next1

    \/ UNCHANGED <<vars1,x>>

/\  \/ Next2

    \/ UNCHANGED <<vars2,x>>

where Next1 contains actions of the form "x' = something".

In this case TLC will report an error when I would like it not to.

Writing the second conjunct as "[Next2]_<<vars2,x>>" results in the same outcome.

Therefore one has to write

/\  \/ Next1

    \/ UNCHANGED <<vars1,x>>

/\  \/ Next2

    \/ /\ x' = x

       /\ v2_1' = v2_1

       /\ v2_2' = v2_2

       /\ ...

* Finally, I stumbled on a strange bug, possibly the same as reported there: 

http://bbpress.tlaplus.net/topic/possible-bug-in-tlc.

The following specification causes TLC, when asked to check I!Spec, to stop with the error 

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException: In evaluation, the identifier x is either undefined or not an operator.

TLC indicates that the error occurred when evaluating "{r \in [{0} -> {0}] : x}".

The module Test seems to be a minimal one that triggers the error.

---------------------- MODULE Test ----------------------

----------------------------- MODULE M -----------------------------

VARIABLE x

ASet == {r \in [{0} -> {0}] : x}

Spec == x = TRUE /\ [][x' = ASet]_x

=============================================================================

VARIABLE y

I == INSTANCE M WITH

    x <- y

    

=============================================================================

This last issue is the most annoying because it is hard to understand where it will creep in.

Giuliano