any TLA+ specification describes the evolution of a universe that contains the system we are interested in. Its basic form
Init /\ [Next]_vars
allows for infinite stuttering on "vars": although the universe doesn't stop, it may be too busy for making our little system advance. This is true independently of the level of abstraction at which the specification is written. If you are only interested in evolutions of the universe in which certain (enabled) actions of the system do occur, you need to use fairness conditions to specify which actions should occur, and of course these fairness conditions should reflect the environment in which the system is run.
At a more down-to-earth level, your question actually contains the answer:
If the support of your write-through cache may be unfair to a processor, you should probably not assert the fairness condition. Or only assert it as a formal exercise to ensure that such potential unfairness is the only reason why your liveness property could be violated.
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.