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

*From*: Isaac DeFrain <isaacdefrain@xxxxxxxxx>*Date*: Fri, 28 May 2021 16:03:50 -0600*References*: <b36a24e7-f78c-4983-a776-16d56a09fd64n@googlegroups.com> <773cd524-608c-4b8d-8735-aaba45583df6n@googlegroups.com> <a1067e851cd095295bd84c3f7c6b3ab4daa47cc6.camel@gmail.com> <e4fc0073-07f4-4fed-b3d6-8a30d75fd9b8n@googlegroups.com> <045f1f3a-4951-452c-a3bc-48738e4d2e6cn@googlegroups.com> <d3e74b921d7c193e74563f1992f76260d0088940.camel@gmail.com>

Hey Jefferson,

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

Best,

Isaac

On Fri, May 28, 2021 at 2:23 PM <joandrade@xxxxxxxxx> wrote:

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) - 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 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' - xBut 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.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAM3xQxH7%2BGKJM-RwccZum4RuDf%3DniF3D6FZ_NXttxtTDZ5TA3g%40mail.gmail.com.

**References**:**[tlaplus] Doing arithmetic with current state value and next state value of a variable in TLA+***From:*Jefferson Andrade

**[tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+***From:*Andrew Helwer

**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+***From:*joandrade

**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+***From:*Leslie Lamport

**Re: [tlaplus] Re: Doing arithmetic with current state value and next state value of a variable in TLA+***From:*Leslie Lamport

*From:*joandrade

- Prev by Date:
- Next by Date:
**[tlaplus] Q about the existential quantifier** - Previous by thread:
- Next by thread:
**[tlaplus] Q about the existential quantifier** - Index(es):