I'm trying to model an operation in TLA+.
To generally summarize the way that this operation works, our system has hard requirements to remove assets within specific time frames.
For example, imagine that we buy some eggs for a restaurant. Eggs have an expiration date and we must purge them out of our inventory before that date. Let's call that expiration date "eggDate".
Valid states for eggDate are any date between now and the eggDate. While the eggDate cannot change we don't know what it will be until we acquire the eggs. How do I model this in TLA+? Oddly I don't see many questions about this on here. Am I thinking about this in the wrong way? Thanks.
Searching Stack overflow.
Time constraints are covered thoroughly in Lamport’s paper Real Time is Really Simple, but in general the approach is to work with relative - not absolute - values. So instead of having a variable with the value eggDate you would have a variable timeUntilEggExpired that counts down until 0 as time advances in a Tick action (you don’t use a now variable). If the timer reaches 0 and the eggs are still in the inventory then perhaps this constitutes a failure. Alternatively if you want to make purging the eggs before expiry an assumption of your system rather than a consequence, you would restrict the Tick action so that it can’t actually advance enough for the timeUntilEggExpired variable to reach zero. Perhaps this would lead to deadlock in your system as some other action that needs time to occur cannot fire, exposing a possible bug. This is the concept of an upper-bound timer as defined in the Lamport paper mentioned above.
Real time constraints have also been discussed on the TLA+ google group, which has a larger corpus of questions & answers than stackoverflow.