Existential quantifier over integers

[abel.n...@gmail.com]

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

Int.

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? 

Thanks!

Abel

[Stephan Merz]

Hello,

TLC cannot enumerate infinite sets. A typical workaround for quantifier bounds involving infinite sets is to override a set such as Int by a small finite set such as -2 .. 2 if appropriate. (See "Additional Spec Options" -> "Definition Override").

For the snippet shown in the message, I suggest that you avoid quantification altogether and write something like

ServerResponse ==

  /\ serverSt.status = "processing"

  /\ serverSt' = [serverSt EXCEPT !.status = "idle"]

  /\ msgs' = msgs \cup {[type |-> "response", to |-> serverSt.from, res |-> (serverSt.a + serverSt.b)]}

  /\ UNCHANGED clientSt

Note that here the value of serverSt stays a record even when the status is "idle" so that the first conjunct makes sense (and evaluates to FALSE) even if the server is idle. You may want to reset the other record fields to default values so that TLC doesn't generate distinct states that differ only in values of irrelevant record fields.

I believe that you can similarly rewrite the actions ServerReceive and ClientReceive. You still need quantification over integers in ClientSend for expressing non-determinism, and here you will have to use a finite set instead for model checking.

Hope this helps,

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

[Abel Nieto]

Thanks! A follow-up question: if I _don't_ do what you suggest and keep the server state in a record, then I get

: Attempted to check equality of string "idle" with non-string:
[status |-> "processing", from |-> "a", a |-> -5..5, b |-> -5..5]

The error occurred when TLC was evaluating the nested

I'll end up doing what you suggested, but I'm curious if there's a way to compare values of different types.

On Tuesday, February 4, 2020 at 1:34:08 PM UTC+1, Stephan Merz wrote:

Hello,

TLC cannot enumerate infinite sets. A typical workaround for quantifier bounds involving infinite sets is to override a set such as Int by a small finite set such as -2 .. 2 if appropriate. (See "Additional Spec Options" -> "Definition Override").

For the snippet shown in the message, I suggest that you avoid quantification altogether and write something like

ServerResponse ==

  /\ serverSt.status = "processing"

  /\ serverSt' = [serverSt EXCEPT !.status = "idle"]

  /\ msgs' = msgs \cup {[type |-> "response", to |-> serverSt.from, res |-> (serverSt.a + serverSt.b)]}

  /\ UNCHANGED clientSt

Note that here the value of serverSt stays a record even when the status is "idle" so that the first conjunct makes sense (and evaluates to FALSE) even if the server is idle. You may want to reset the other record fields to default values so that TLC doesn't generate distinct states that differ only in values of irrelevant record fields.

I believe that you can similarly rewrite the actions ServerReceive and ClientReceive. You still need quantification over integers in ClientSend for expressing non-determinism, and here you will have to use a finite set instead for model checking.

Hope this helps,

Stephan

On 4 Feb 2020, at 13:09, abel....@gmail.com wrote:

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

Int.

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? 

Thanks!

Abel

--
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 tla...@googlegroups.com.

[Stephan Merz]

In TLA+, we do not know if 42 = {} or if "idle" = [status |-> "processing", from |-> "clientA", a |-> -23, b |-> 4711], that's why TLC complains about being unable to compare such values.

If you want to use an atomic value for the state where the server is idle, you can do something like

idle == CHOOSE x : x \notin ServerState

(where ServerState is the set of records representing states where the status is "processing"). By the axioms of set theory, we know that some such value exists and by definition it is different from any of the ServerState records. TLC should automatically override this definition by a model value and will know that the comparison yields FALSE. If it doesn't do this automatically, use a manual definition override to achieve this.

Stephan

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/ec4db371-64d1-49f2-946e-45a0f422add8%40googlegroups.com.

[Igor Konnov]

Hi Abel,

Depending on the properties that you like to check, you might want to try the Apalache model checker [1]. Although the theory and the tool are not that mature as with TLC, Apalache can handle existential quantifiers over Int and Nat, as long as the checker can replace a quantifier with an integer constant. As long as the model checker has to reason about finite sets, even though their elements may be integers, it should work.

I have added tool-specific type annotations in your specification and replaced an infinite set of records with a set filter in ClientReceive, so apalache could digest the spec. (Stephan already mentioned the issue with “idle”, which I have replaced with [status |-> “idle”].) The next question is the kind of property you like to check. At the moment, we can check inductive invariants and safety, by unrolling the transition relation.


[1] https://github.com/konnov/apalache/tree/unstable


Best regards,
Igor

[Leslie Lamport]

A minor correction to Stephan's post.  TLC does not automatically override any definition. 
What Stephan meant is that TLC can be directed to override the definition and consider `idle' 
to be a model value.   When you create a new model in the Toolbox, it will automatically
add the override directive to what the model tells TLC to do.

Leslie

On Tuesday, February 4, 2020 at 7:00:29 AM UTC-8, Stephan Merz wrote:

In TLA+, we do not know if 42 = {} or if "idle" = [status |-> "processing", from |-> "clientA", a |-> -23, b |-> 4711], that's why TLC complains about being unable to compare such values.

If you want to use an atomic value for the state where the server is idle, you can do something like

idle == CHOOSE x : x \notin ServerState

(where ServerState is the set of records representing states where the status is "processing"). By the axioms of set theory, we know that some such value exists and by definition it is different from any of the ServerState records. TLC should automatically override this definition by a model value and will know that the comparison yields FALSE. If it doesn't do this automatically, use a manual definition override to achieve this.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2051d601-952a-434a-a93a-ebccb87843b9%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 

[Michael Leuschel]

Hi Abel and Igor,

you can also try using our ProB validation tool.

It can handle Addition2.tla that Igor sent. It can also deal with the commented out version of the existential quantifier without filter set:

  \E m \in (msgs \intersect ServerMsgs); see the screenshot below.

(Note: The orange infinity symbol states that not all transitions for ClientSend were computed due to an unbounded quantification.)

ProB, however, requires that its type inference can infer a type for all variables.

The original Addition.tla from Abel raises a type error.

The TLA mode would also benefit from making it more accessible to persons not familier with B (the TLA models are translated to the

B language, and this shines through in various places in the tool).

Greetings,

Michael