TLC bug or TLA+ subtlety?

[Hillel Wayne]

Take the following spec:

VARIABLES x, y

vars == <<x, y>>

Init ==
  /\ x = FALSE
  /\ y = FALSE

Next ==
  /\ x' \in BOOLEAN
  /\ y' = (x \/ x')

Spec == /\ Init /\ [][Next]_vars

This checks with 7 states generated. Now remove the parenthesis in Next,
giving

Next ==
  /\ x' \in BOOLEAN
  /\ y' = x \/ x'

This now fails, with a not fully specified successor state:

State 2: <Next line 11, col 3 to line 12, col 17 of module problem>
/\ x = TRUE
/\ y = null

This seems to me like a bug with TLC, but I wanted to check if the two
Nexts aren't actually different semantically, and if so, what makes them
different.

H

[Alexander Bakst]

I’m no TLA+/TLC expert, but I think in the second version, since the second conjunct must be parsed as (y' = x) \/ x’, y’ could be anything (which would satisfy the since there is no type invariant. In the first version, y’ must be TRUE or FALSE. So it seems there is a semantic difference.

—Alexander

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit https://urldefense.proofpoint.com/v2/url?u=https-3A__groups.google.com_d_msgid_tlaplus_b2139e63-2D9e12-2Df82c-2D4935-2D2077a148f7ef-2540gmail.com&d=DwIFaQ&c=-35OiAkTchMrZOngvJPOeA&r=K2l4mPc1D0iv68sbdBufTMtzoJU_1KNLlayaL2SDXyM&m=8LYpsEoab1BwkFSb0asQPySqAcjrT4e8LOpWxVsSXn6o2ItRMoDUKXXH57UBZe1-&s=WBDXH0D7duJXGwd7L__dZJIR6RymR5fEaJSyT6TmLm8&e= .

[tlaplus-go...@lemmster.de]

----- MODULE Foo -----
VARIABLES x, y

A ==

/\ x' \in BOOLEAN
/\ y' = x \/ x'

B ==
/\ x' \in BOOLEAN
/\ \/ y' = x
\/ x'

THEOREM A <=> B BY DEF A, B

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

-> % tlapm Foo.tla
** Unexpanded symbols: ---

(* created new "Foo.tla.tlaps/Foo.tla.thy" *)
(* fingerprints written in "Foo.tla.tlaps/fingerprints" *)

M.

> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/690ABB47-97F4-43D7-819F-E1ACFDEF37BB%40gmail.com.

[Andrew Helwer]

Per page 271 in Specifying Systems the \/ operator has precedence 3-3 and the = operator has precedence 5-5, so the = binds more tightly to the expression and it is parsed ((y = x) \/ x').

Andrew