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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Thu, 18 Jan 2024 18:23:13 -0800 (PST)*References*: <ae8ae8c1-0036-4a7d-ad3e-458676c81b99n@googlegroups.com> <356dc20e-7da1-436c-8631-3c4b81b8e2b9n@googlegroups.com> <66e3614c-2e74-417e-ac48-61549e8b524dn@googlegroups.com>

The fundamental assumption of our way of modeling digital systems is

that their execution can be modeled as a sequence of atomically

changing states. No digital system reads a clock and gets a value of

sqrt(2). What I expect matters is not the actual numbers read by the

clock but the ordering of events in the different processes that those

numbers cause. The airplane is not going to crash because a process

read 1.41421 rather than 1.41420 or 1.41422.

Approximating sqrt(2) by a number with finite fractional places will

cause a drift at some point.

If you model real time by variable t whose value is an integer, then

this is the case only if you model a clock as ticking once for a fixed

number of ticks of t. But you can add nondeterminism to how much t

has to advance for a process's clock to tick. The clocks of different

processes are probably synchronized so they never drift too far apart.

If so, the nondeterminism can be such as to ensure that this is the

case. But it works just as well if the actual clocks can drift

arbitrarily far apart.

It's possible to model a real-time system using nondetermism so that

every execution allowed by physics is described by an execution of the

model. I expect that modeling the real numbers of physics by integers

would cause the model to allow executions that eventually diverge from

ones that are physically possible. But "eventually" could in

principle be made to mean after a million years.

In short, using integers instead of real numbers is not the problem.

The problem is whether you can get a good enough approximation with

few enough states to make model checking feasible. I have no idea how

likely this is to be the case for real system designs.

On Tuesday, January 16, 2024 at 8:57:33 PM UTC-8 abhish...@xxxxxxxxx wrote:

Time can be modeled as integers if we are interested in events for one clock, but distributed systems may have more than one clock. Consider a system with two clocks, where the second clock ticks faster than the first clock by a ratio of sqrt(2). In this case, no way exists to force events to occur at integral times on a common clock as far as I know. Approximating sqrt(2) by a number with finite fractional places will cause a drift at some point. Some security protocols may require the use of dense time in analysis -- so using integers instead of reals here may cause a "loss of consistency". If the spec is about a closed system, i.e., the environment is also modeled in the spec, then there is usually no reason for the environmental events to occur on "ticks" -- using integral time here may also be inaccurate.Using integral time may be ok in basic specs.-AbhishekOn Tuesday, January 16, 2024 at 8:20:21 PM UTC-6 Andrew Helwer wrote:Real-time spec models work fine when using natural numbers. Just think of 1 as the smallest time resolution you care about. You don't actually need Reals to represent time in any real-world system, because real-world systems don't care about an infinite number of decimal places in the elapsed time.When you quantify over Int or Nat like that you are quantifying over an infinite set, which TLC can't handle (since it is a finite model checker). You have to use a definition override in your model to restrict Int or Nat to something like 0 .. 10 or whatever. Since this affects all usage of Int or Nat in your spec that can be a bit annoying, so you might want to define something like TimeIncrement == Real in your spec then override TimeIncrement == 0 .. 10 in your model, then use \E d \in TimeIncrement instead of \E d \in Real.AndrewOn Tuesday, January 16, 2024 at 11:07:12 AM UTC-5 Andrew Samokish wrote:Hello everyone,I`m trying to understand if I can emulate some timers with TLA,practically, i would like to study some requirements like'if A stays for 200 ms'in the context of some other triggers depending on time.There is a nice book 'Real Time is Really Simple' by Leslie Lamport, but when I tried to rewrite the proposed example with TLA+ toolbox, I found that Real numbers are not really supported with TLA , yet mentioned in the book (btw, it is interesting if code sources for this book are available somewhere..).for example, here is the Tick definition:Tick == \E d \in Real: d > 0

/\ \A t \in Thread : ubTimer[t] > d

/\ now' = now + d

/\ (ubTimer' = [ta \in Thread |->

IF ubTimer[ta] = 2147483647 THEN 2147483647

ELSE ubTimer[ta] - d])

/\ (lbTimer' = [tb \in Thread |-> Max(0, lbTimer[tb] -d)])

/\ UNCHANGED << x, PC>>Can you please tell me if I can substitute Reals with Integers without losing consistency? Also, with\E d \in IntTLA reports, that i`m using uncountable definitions....And, in general, is it possible to implement a timer reacting at the exact time?Thanks for the help in advanceSincerely yours, Andrei

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/9d2e5798-5dbf-4ee9-aaef-03e1d4d3584an%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: timers***From:*Andrew Samokish

**References**:**[tlaplus] timers***From:*Andrew Samokish

**[tlaplus] Re: timers***From:*Andrew Helwer

**[tlaplus] Re: timers***From:*Abhishek Singh

- Prev by Date:
**[tlaplus] Re: timers** - Next by Date:
**[tlaplus] Re: timers** - Previous by thread:
**[tlaplus] Re: timers** - Next by thread:
**[tlaplus] Re: timers** - Index(es):