Re: [tlaplus] why I cannot compare Nat with 0

[victor zhang <zhavictor@xxxxxxxxx>]

Thank you!  This worked.  The reason I used {Nat} is that TLC _expression_ evaluator threw an error if I do

ThreadStateVal == 
    [
        read_index: Nat,
        write_index: Nat
    ]

On Wednesday, January 11, 2023 at 11:58:34 PM UTC-8 Stephan Merz wrote:

{Nat} is the singleton set that contains Nat as its only element. You want to write 

ThreadStateVal == 
    [
        read_index: Nat,
        write_index: Nat
    ]

Stephan

On 12 Jan 2023, at 06:48, victor zhang <zhav...@xxxxxxxxx> wrote:

I have the following TLA+ code

```

Threads == {"t1", "t2"}

VARIABLE thread_states

ThreadStateVal ==
    [
        read_index: {Nat},
        write_index: {Nat}
    ]
   
Init ==

    thread_states [ t \in Threads |-> [ read_index |-> 0, write_index |-> 0] ]

TypeOK ==

    thread_states \in [Threads -> ThreadStateVal]

....

```

When I run the model, I got "Attempted to compare integer 0 with non-integer: Nat", not sure how to fix it, any help will be greatly appreciated.

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9a3c35b7-9168-4950-a65b-582b5919b293n%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/57c127ec-0a57-4585-bf04-5e56d7524da9n%40googlegroups.com.