[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: joandrade@xxxxxxxxx*Date*: Thu, 27 May 2021 19:48:35 -0300*Ironport-hdrordr*: A9a23:GsJZ9agJ0yJ1O9BKPRjQZRDTUHBQX4R13DAbv31ZSRFFG/FwyPrD7Y8mPE7P5UdoZJh/o7rwQZVoIEmsg6KdhLN/U4tKMzOWzVdAQLsSnrcKhgeQbxEXGIZmpOJdm4YXMqyzMbE4t7e13OGAe+xQg+VviZrYwds2rE0dBT2D3spbnkhE42SgYzxLrVJ9dNYE/fOnj6It1l3QAwVqH7qG62E+LpX+Tp/w5eXbiHg9dlMaASa17Q9Ag4SKYyRwsC1uIQ+njY1SuFQsUmTCl8GeWjKAu3zhPq3ojqi/KLDau5t+7QC3+6oowjiGsHfjWGyQMIfy9wzdadvfjSdN4abxiiZlBd167zf6f22+oxfhnynmlBg07WP6oGXowEfenQ==*References*: <b36a24e7-f78c-4983-a776-16d56a09fd64n@googlegroups.com> <773cd524-608c-4b8d-8735-aaba45583df6n@googlegroups.com>*User-agent*: Evolution 3.36.4-0ubuntu1

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) - 128Next == VS_Pitch_Wheel_RotationSpec == 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_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_ex1 Thanks 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?-- 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/a1067e851cd095295bd84c3f7c6b3ab4daa47cc6.camel%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Next by Date:
**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Previous by thread:
**[tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Next by thread:
**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+** - Index(es):