Re: [tlaplus] Re: How to approach modelling time?

Here's an example of "view symmetry" (discussed in Lamport's "Real Time is Really Simple"):

I have a "clock" variable, an integer that can be incremented by the "Tick" action. Other actions may read the clock and store the current clock value somewhere, e.g. the "ClientWrite" action adds the current clock value to a list called "replicationTimes". I simply constrain the max clock value to 8 in mcLeaseRaftWithTimers.cfg, and hope that provides enough model-checking depth.

The interesting part of my spec is in leaseRaftWithTimers.tla, where I define a VIEW called "ClockAbstractionView". This VIEW reduces the state space dramatically. A state with a list of clock values like [1, 2, 3] is the same as one where the list is [6, 7, 8], since my spec only cares about the differences between times, not absolute clock values. (In other words my spec uses timers, not times-of-day.) This reduces model-checking time from days to hours for my spec. I still need to constrain the max clock value to something (I chose 8), but the VIEW also helps.

On Wed, Oct 16, 2024 at 11:10 AM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

See Lamport's paper Real Time is Really Simple: https://www.microsoft.com/en-us/research/publication/real-time-is-really-simple/

Basic idea: instead of having a monotonically-increasing time variable, you keep track of a set of upper-bound timers (action must happen before timer reaches zero) and lower-bound timers (action cannot happen until timer reaches zero) that always initialize to some finite value then tick down to zero instead of tracking an infinitely-increasing clock time.

Andrew Helwer

On Wednesday, October 16, 2024 at 9:04:24 AM UTC-4 Benjamin Parsons-Willis wrote:
Hi all!

I am working with TLA+/pluscal, although potentially this is not the appropriate tool for what I want to test.

I am creating a specification for a system to achieve consistency OR report of failure, in a constrained environment where a total ordering of events (mutations/assignments) cannot always be derived.

For instance, we may receive events in time, that look like:
Event1: assignment of state to value 3; occurred between t=2 and t=3
Event2: assignment of state to value 2; occurred between t=2 and t=4

With the above, it would not be possible to derive an output value, and this would raise a failure condition.

Regardless; to model this I need to be able to model the passage of time.
Events are generated by 'polling' processes, which generate events at a fixed time-incremenent.

A synchronised clock can be assumed for all processes.

I have run into difficulty representing this clock variable without resulting in infinite state space.

Having read about VIEW, I understand that I can instruct TLC to ignore the global clock, but this clock leaks into the specification regardless, as the clock is included in events.

I have another process 'coordinator' which will take these events, establish a partial ordering, and then resolve all ordered cases (or mergable cases like unordered mutations), to either establish a consensus value, or note that consensus was unable to be reached (overlapping assignments)

Is TLA the best tool for this task?
If so, what are some approaches to consider? I have looked at Real-Time is easy, but I have not been able to match it to my use case, perhaps I am not understanding?

Thanks for any insight you could offer.

--
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/88ae86ad-2bda-4889-8730-6b228e5e9ca1n%40googlegroups.com.