[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*Ironport-hdrordr*: A9a23:tfCMnK7C3Ggon9iZFAPXwQWCI+orLtY04lQ7vn1ZYSd+NuSFisGjm+ka3xfoiDAXHEotg8yEJbPoex+sjqJdybI6eZOvRhPvtmftFoFt6oP+3ybtcheSh5Zg/I9aWexFBNX0ZGIR/L/HySO/FMstx8TCzbCwiY7lvgdQZCxJS4Ul1Qd2DQ6HDlZ7LTMoa6YROZKA6qN81k+dUFsNaMDTPAh1Y8HioJnxmIvicVo6AXccmX+zpBap8qO/OwOT3xcAX1p0sPIf2E3EiRG8x6mnqpiAu13h/krS9YkTuPaJ8KoMOOWoitIJbgzrkBvAXvUjZ5SmvCop5N2p8kogitPWoxwtVv4Dr0/5Wmm0pBvr1U3k0CwygkWShmOwpXf4u8T2SHYbBqN69MtkWz/Y70Zlg91myqJM2AuixulqJCrakC7w6tTOXR0CrDv5nVMYneQej2NSXOIlAdc73OtvhjIoYek9NRn34owmD+ViSPvky59tAC6nRkvUsWV1zNunUm5bJGbzfmE4ttWRw3xqmhlCvgYl7fYSmXoN7/sGK6Vs3fjOMahjidh1P70rRJ96bd1xNvefOyjnTR7KDWOfOliPLtBiB1v977DypJE4/vujdpBN9oY7hZipaiI6iUcCP2zpD8OK0Nln0DDoBF+8UzPk191E6/FC24HUdf7ENyuMTVxrvdCnv+xaIsCzYYfyBLtmR9HkK2XqFcJy2xDmH6NVNWIVXKQuy7QGcmPLhsrKL4Hw39arOMr7Ff7KCjYrWmT2Bz8qQCXzKMJc7kqiR3//h1zrV2nwf1HklKgAWpTyzqw004gCNopFt0wuhVO16trjE0wIjoUGOHBzKr/mja+3zFPGmBevnhpUEysYNF9c5PHLUn9BpwMGd2PyNZgZvcmHEFoinUe6Gg==*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):