Doing arithmetic with current state value and next state value of a variable in TLA+

46 views
Skip to first unread message

Jefferson Andrade

unread,
May 27, 2021, 4:11:15 PM5/27/21
to tlaplus
Hello,

I want to write a (piece of a) formula like this:

y' = x' - x

But every time I try to run the model I get the error, «In evaluation, the identifier x is either undefined or not an operator.»

What is going on? Is it really not possible to write such formulas? why? How can I work around this?

Thanks.

Andrew Helwer

unread,
May 27, 2021, 5:35:20 PM5/27/21
to tlaplus
Can you post a minimal functional spec which reproduces this error?

joan...@gmail.com

unread,
May 27, 2021, 6:48:40 PM5/27/21
to tla...@googlegroups.com
The minimal spec follows.

---------------------------- MODULE minimal_ex1 ----------------------------
EXTENDS Integers, Reals
VARIABLES x, y

TypeOK == /\ x \in -128..127
          /\ y \in -128..127

Init == ((x \in -128..127) /\ (y = 0))

VS_Pitch_Wheel_Rotation == 
    y' = ((x' - x + 128) % 256) - 128
                             
Next == VS_Pitch_Wheel_Rotation      

Spec == Init /\ [][Next]_<<x,y>> 
=============================================================================
\* Modification History
\* Last modified Thu May 27 19:45:21 BRT 2021 by jefferson
\* Created Thu May 27 19:45:08 BRT 2021 by jefferson

When the model is run, it produces the following error messages:

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.
line 11, col 12 to line 11, col 12 of module minimal_ex1

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 11, column 5 to line 11, column 37 in minimal_ex1
1. Line 11, column 10 to line 11, column 37 in minimal_ex1
2. Line 11, column 11 to line 11, column 30 in minimal_ex1
3. Line 11, column 12 to line 11, column 23 in minimal_ex1
4. Line 11, column 12 to line 11, column 17 in minimal_ex1
5. Line 11, column 12 to line 11, column 13 in minimal_ex1
6. Line 11, column 12 to line 11, column 12 in minimal_ex1

Thanks for your help.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/RavL524UeqM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/773cd524-608c-4b8d-8735-aaba45583df6n%40googlegroups.com.

Leslie Lamport

unread,
May 27, 2021, 6:56:56 PM5/27/21
to tlaplus
And what do you expect the possible executions of that spec starting with y = 0 to be?

Leslie Lamport

unread,
May 27, 2021, 7:22:05 PM5/27/21
to tlaplus
I'm sorry, I meant executions starting with x = y = 0.   Actually, you just need to list the possible second states of such an execution.

Leslie

Isaac DeFrain

unread,
May 27, 2021, 9:46:09 PM5/27/21
to tla...@googlegroups.com
Hello Jefferson,

It seems that the issue stems from the evaluation semantics of TLC. In VS_Pitch_Wheel_Rotation, you use the value x', however, TLC evaluates each conjunct in order (from first to last). Unfortunately, there is no value given for x' since we have not said how the value of x changes (this is what the cryptic "the identifier x is either undefined" bit is about). For example, admittedly this is not very interesting, but it should bring the point home, changing the action to

VS_Pitch_Wheel_Rotation ==
    /\ UNCHANGED x
    /\ y' = ((x' - x + 128) % 256) - 128

results in a successful model run. You must say how the value of x evolves before you can use the value of x in the successor state, i.e. x'.

To be clear, this is a TLC thing and not a TLA+ thing (there are no evaluation semantics for TLA+; it's math). Strictly speaking,

/\ UNCHANGED x
/\ y' = ((x' - x + 128) % 256) - 128

and

/\ y' = ((x' - x + 128) % 256) - 128
/\ UNCHANGED x

are equivalent in TLA+ (because conjunction is commutative), but they are not treated as equivalent by TLC.

I hope this helps!


Best,

Isaac DeFrain


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://groups.google.com/d/msgid/tlaplus/045f1f3a-4951-452c-a3bc-48738e4d2e6cn%40googlegroups.com.

joan...@gmail.com

unread,
May 28, 2021, 2:23:48 PM5/28/21
to tla...@googlegroups.com
Hi Isaac,

Thank you immensely for your help. You were very kind of you to take the time to explain the problem to me. Really appreciate it.

Regards,
Jefferson Andrade.

joan...@gmail.com

unread,
May 28, 2021, 4:23:17 PM5/28/21
to tla...@googlegroups.com
Hello,

This was the smallest exert I could put together to reproduce the error I was having. The entire module is much larger and is intended to model how a set of sensors react to the inputs of a set of actuators. I am sorry if the example makes no sense.

But thanks for your reply and your input. I problem has been fixed now.

Regards,
Jefferson.

Isaac DeFrain

unread,
May 28, 2021, 6:04:04 PM5/28/21
to tla...@googlegroups.com
Hey Jefferson,

You’re very welcome! I’m glad you got things working properly.


Best,

Isaac

--
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://groups.google.com/d/msgid/tlaplus/d3e74b921d7c193e74563f1992f76260d0088940.camel%40gmail.com.
--
Isaac DeFrain
Reply all
Reply to author
Forward
0 new messages