In my previous post, when I wrote "Spec 6 is a sensible TLA+ spec" I
meant Spec4. Sorry about that.Leslie Lamport
On Thursday, January 23, 2014 2:59:14 AM UTC-8, Oscar Ricardo Moll wrote:Hi there,I've looked through the basic track of the hyperbook, but when trying to write my own specs, I run into some behaviors of TLC that still puzzle me.
For each of the specs below, I ran the model specified by that spec, and simply checked for deadlock. For each, I added a comment explaining what I thought they mean, and the reaction from TLC when I run them.
I would help me if someone ran through them and explained to me whether my expectations of the spec meaning are off, and if possible some clue to be able to understand the observed behavior when running TLC with them.
The spec I care most about is Spec4 because I run into this sort of error in larger specs.
------------------------------- MODULE basic ------------------------------ -
VARIABLE xSpec1 == (x = 1)
(**
meaning to me: all behaviors where x is 1 (at the start),
and anything at all later. Not very constrained but has meaning.TLC:
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.NullPointerException
(nothing on User Output)
**)prop == x \in {1,2,3}
Spec2 == [][prop]_x
(**
meaning to me: again, starts with, but additionally, all states
are in {1,2,3}, and all transitions are possible.TLC:
The configuration file did not specify the initial state predicate.
Can also be caused by trying to run TLC on a specification from
a module imported with a parameterized INSTANCE statement.
**)Spec3 == prop /\ [][prop]_x
(**
meaning to me: same as above, since [] includes the initial state.TLC:
Successor state is not completely specified by the next-state action.
Why do we consider it not specified for any x, x', prop holds as long as x \in {1,2,3} (ie x' can be anything)
**)
Spec4 == prop /\ [][prop /\ prop']_x
(**
meaning to me: now we are restricting the next state a bit more. both x before and x after are in {1,2,3} but
they aren't really related.TLC:
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. <--- weird, it is declared, but undefined.
line 18, col 9 to line 18, col 9 of module basic
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 40, column 21 to line 40, column 24 in basic
1. Line 40, column 29 to line 40, column 33 in basic
2. Line 40, column 29 to line 40, column 32 in basic
3. Line 18, column 9 to line 18, column 9 in basic
**)Spec5 == prop /\ prop'
(**
meaning to me: there is no temporal statement here, so it may complain like in Spec1
What is the meaning of the primed variables outside of a [] formula?TLC:
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:
TLC cannot handle this conjunct of the spec:
line 59, col 18 to line 59, col 22 of module basic
note: no user output
**)Spec6 == prop /\ prop' /\ [][prop /\ prop']_x
(**
same as above
**)