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

On Thursday, January 12, 2023 at 1:03:32 AM UTC-8 Stephan Merz wrote:

TLC cannot evaluate expressions that require it to enumerate infinite sets. However, although it cannot evaluate Nat, TLC can evaluate x \in Nat and similar expressions.

Stephan

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

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