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.On Thu, 2021-05-27 at 16:22 -0700, Leslie Lamport wrote: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.LeslieOn Thursday, May 27, 2021 at 3:56:56 PM UTC-7 Leslie Lamport wrote:And what do you expect the possible executions of that spec starting with y = 0 to be?On Thursday, May 27, 2021 at 3:48:40 PM UTC-7 joan...@xxxxxxxxx wrote:The minimal spec follows.---------------------------- MODULE minimal_ex1 ----------------------------EXTENDS Integers, RealsVARIABLES x, yTypeOK == /\ x \in -128..127          /\ y \in -128..127Init == ((x \in -128..127) /\ (y = 0))VS_Pitch_Wheel_Rotation ==     y' = ((x' - x + 128) % 256) - 128                             Next == VS_Pitch_Wheel_Rotation      Spec == Init /\ [][Next]_<> =============================================================================\* Modification History\* Last modified Thu May 27 19:45:21 BRT 2021 by jefferson\* Created Thu May 27 19:45:08 BRT 2021 by jeffersonWhen 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_ex1The error occurred when TLC was evaluating the nestedexpressions at the following positions:0. Line 11, column 5 to line 11, column 37 in minimal_ex11. Line 11, column 10 to line 11, column 37 in minimal_ex12. Line 11, column 11 to line 11, column 30 in minimal_ex13. Line 11, column 12 to line 11, column 23 in minimal_ex14. Line 11, column 12 to line 11, column 17 in minimal_ex15. Line 11, column 12 to line 11, column 13 in minimal_ex16. Line 11, column 12 to line 11, column 12 in minimal_ex1Thanks for your help.On Thu, 2021-05-27 at 14:35 -0700, Andrew Helwer wrote:Can you post a minimal functional spec which reproduces this error?On Thursday, May 27, 2021 at 4:11:15 PM UTC-4 joan...@xxxxxxxxx wrote: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. -- 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d3e74b921d7c193e74563f1992f76260d0088940.camel%40gmail.com.