Dear Mr. Moll,
The Hyperbook tells you to write specs that consist of either (a) two
formulas, an initial predicate I that specifies the initial values of
the variables and a next-state relation N that specifies the relation
between the values of the variables in the current and next state, or
(b) the single formula I /\ [][N]_vars where vars is the tuple of all
variables. If you write specs that do not have that form, then you
should understand the meaning of those specs, which is explained in
the "Temporal Logic" section in the Math part of the Hyperbook, and in
Chapter 8 of "Specifying Systems". You will see that all your Specs
except 4 and 6 are satisfied by an uncountably infinite number of
behaviors, so you should not have expected TLC to do anything sensible
with them. Spec6 is not a legal TLA+ formula; the parser does not
accept it. I don't know how you got TLC to even get as far as
complaining about the spec. Spec 6 is a sensible TLA+ spec that
allows precisely the set of behaviors that I think you expect it to.
However, TLC cannot handle all sensible specs. For example, the
following two specs are completely equivalent
(x=0) /\ [](x'= x+1) (x=0) /\ [](x+1=x')
but TLC can handle the first and not the second. If you replace prop'
in that spec by the equivalent formula x' \in {1,2,3}, then TLC can
handle it. To understand why, see Section 14.2 of "Specifying
Systems".
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
**)