Show pageOld revisionsBacklinksBack to top This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong. ====== How to approach modeling time? ====== 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. Source: https://groups.google.com/g/tlaplus/c/IGbAcSOUUes learning/faq/modeling_time.txt Last modified: 2024/12/21 12:05by fponzi
fponzi