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

{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 <zhavictor@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+unsubscribe@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/2912A264-779F-4559-A85B-E47DC9F453DB%40gmail.com.