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

*From*: Isaac DeFrain <isaacdefrain@xxxxxxxxx>*Date*: Thu, 27 May 2021 19:45: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>

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

/\ 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

/\ 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

On Thu, May 27, 2021 at 5:22 PM Leslie Lamport <tlaplus.ll@xxxxxxxxx> 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.Leslie--On 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 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...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/773cd524-608c-4b8d-8735-aaba45583df6n%40googlegroups.com.

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/045f1f3a-4951-452c-a3bc-48738e4d2e6cn%40googlegroups.com.

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/CAM3xQxEHrw0GdeubSZiJdfZ9DR%2BTy4q30rt%2BDJaXpSUTeFMsGA%40mail.gmail.com.

**Follow-Ups**:

**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

- Prev by Date:
- Next by Date:
- Previous by thread:
- Next by thread:
- Index(es):