why I cannot compare Nat with 0

[victor zhang]

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!

[Stephan Merz]

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

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

Stephan

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9a3c35b7-9168-4950-a65b-582b5919b293n%40googlegroups.com.

[victor zhang]

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
    ]

[Stephan Merz]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57c127ec-0a57-4585-bf04-5e56d7524da9n%40googlegroups.com.

[victor zhang]

Got it, thanks!