Re: [tlaplus] Modeling leases

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Yes, the idea was to demonstrate how Apalache could naturally check
TLA+ specs over unbounded integers, since SMT solvers are good at it.
In case of TLC, I think you would have to bound the sets Int and Nat.

Best,
Igor

On Thu, Feb 29, 2024 at 2:13 AM A. Jesse Jiryu Davis
<jesse@xxxxxxxxxxxxxxx> wrote:
>
> I've now read the TLA+ spec but I haven't tried to model-check it yet. The spec uses infinite sets such as Int and Nat, it doesn't constrain these to finite sets and it doesn't use the techniques described in Lamport's "Real Time Is Really Simple" to make the state space finite. I don't think spec could be model-checked with TLC. Is this a demonstration of Apalache's advantages over TLC?
>
> On Tue, Feb 27, 2024 at 9:23 AM A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:
>>
>> Thank you!
>>
>> On Tue, Feb 27, 2024 at 8:22 AM Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
>>>
>>> Hi Jesse,
>>>
>>> I used Apalache to check a clock synchronization algorithm a few years
>>> ago. You can have a look at the TLA+ specification [1] and the talk
>>> from the TLA+ Tutorial 2021 [2].
>>>
>>> [1] https://github.com/informalsystems/tla-apalache-workshop/blob/main/examples/clock-sync/ClockSync7.tla
>>> [2] https://youtu.be/NXLJoUKJnDQ?t=5821
>>>
>>> Best,
>>> Igor
>>>
>>> On Mon, Feb 26, 2024 at 1:18 AM A. Jesse Jiryu Davis
>>> <jesse@xxxxxxxxxxxxxxx> wrote:
>>> >
>>> > Hello! Murat Demirbas and I are designing a Raft variant that uses timed leader leases for stronger consistency. We plan to write a TLA+ spec, and it will involve clocks. We're interested in examples in addition to Lamport's "Real Time Is Really Simple" paper. Has anyone worked with time/clocks in TLA+, or could you point us to example specs?
>>> >
>>> > --
>>> > 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/CAFRUCtYYwU8mrQ_3mNqb%2BCYd5xK1ObUuFBRENv34WXMFjFrYNw%40mail.gmail.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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
>>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACooHMAmhdEOAXfnvd1y_5q-CfuG3dg%3Dc5wOm-MC5HQjorE%3D7w%40mail.gmail.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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtaeE%2BCeRULB0cx8HeOu%2BoykfetRyyosC9iJ83aJYm4tgw%40mail.gmail.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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACooHMCSJM3Y4BsnMyM2%3Dh932KhyFfDv77CkA2A_9c2PEejSMg%40mail.gmail.com.