[tlaplus] Re: Priming TLA+ formulas

On Tuesday, April 11, 2023 at 12:36:53 PM UTC-7 n s wrote:

Thanks Stephan, yes I mis-spoke, I did mean SANY and not a compiler! I re-read that section in SS and I understand why TLC places the restrictions it does. I was hoping that TLC would be able to handle this kind of feature since it doesn't require any change to how TLC evaluates but more of a pre-processing step in which (a=1/\b=2)' ---> (a'=1 /\ b'=2), but then I'm saying that without having thought through what complications might arise in practice.

thanks

On Tuesday, April 11, 2023 at 1:17:49 AM UTC-7 Stephan Merz wrote:
Your formula is legal TLA+, that's why SANY (I guess that's what you call the "compiler") accepts it. TLC expects you to write

a' = 1 /\ b' = 2

because it interprets Foo' as a formula to evaluate over the next state, which it has not constructed yet. Look at chapter 14 of Specifying Systems,
and in particular section 14.2.6 for a discussion on how TLC computes states.

Stephan

On Monday, April 10, 2023 at 10:00:07 PM UTC+2 nedsr...@xxxxxxxxx wrote:
Hello again, in the example below I want to use Foo' to mean a'=1 /\ b'=2. The compiler accepts this but TLC complains. Why is that?

VARIABLE a,b
Foo == a=1 /\ b=2
Init == Foo
Next == Foo /\ Foo'

Spec == Init /\ [][Next]_<<a,b>>

TLC complains
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 a is either undefined or not an operator.
line 6, col 8 to line 6, col 8 of module test