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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 2 May 2021 11:22:11 +0200*References*: <e8418ec5-830c-4fb3-a968-28295857c59dn@googlegroups.com>

Hello, TLC will be able to handle your second spec if you restrict the choice of y' to a finite set, such as B == y' \in 0..10 /\ x < y' 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/CF5A09AB-3B45-4780-8E85-38161F17E3CF%40gmail.com. |

**References**:

- Prev by Date:
**Re: [tlaplus] Re: SANY debugging mode** - Next by Date:
**[tlaplus] Modelling "eventually, with probability 1"** - Previous by thread:
**[tlaplus] TLC Error that had me puzzled for a while** - Next by thread:
**[tlaplus] Modelling "eventually, with probability 1"** - Index(es):