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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 4 Feb 2020 13:34:04 +0100*References*: <2051d601-952a-434a-a93a-ebccb87843b9@googlegroups.com>

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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2A642E4C-42AA-40F4-B181-EFE289138E9E%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Existential quantifier over integers***From:*Igor Konnov

**Re: [tlaplus] Existential quantifier over integers***From:*Abel Nieto

**References**:**[tlaplus] Existential quantifier over integers***From:*abel . nieto90

- Prev by Date:
**[tlaplus] Existential quantifier over integers** - Next by Date:
**Re: [tlaplus] Existential quantifier over integers** - Previous by thread:
**[tlaplus] Existential quantifier over integers** - Next by thread:
**Re: [tlaplus] Existential quantifier over integers** - Index(es):