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

[tlaplus] Existential quantifier over integers

I'm getting started with TLA+ and wrote a spec for a simple server that adds two integers: https://pastebin.com/Yc8qfwa7

When I run TLC, I get the following error:

The exception was a java.lang.RuntimeException

: TLC encountered a non-enumerable quantifier bound


line 46, col 34 to line 46, col 36 of module Addition

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 46, column 3 to line 50, column 27 in Addition

1. Line 46, column 6 to line 49, column 84 in Addition

 The errors refers to a "non-enumerable quantifier bound Int", but `Int` is an enumerable set.

The relevant snippet of my code reads

ServerResponse == \* server responds
  /\ \E fromV \in CLIENT, aV \in Int, bV \in Int :
       /\ serverSt = [status |-> "processing", from |-> fromV, a |-> aV, b |-> bV]
       /\ serverSt' = "idle"
       /\ msgs' = msgs \cup {[type |-> "response", to |-> fromV, res |-> (aV + bV)]}
  /\ UNCHANGED <<clientSt>>

What am I doing wrong here? And what's the idiomatic way to "deconstruct" records in TLA? 



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/2051d601-952a-434a-a93a-ebccb87843b9%40googlegroups.com.