Go backward to TLA Go up to Top Go forward to Liveness as TLA Formulas

Adding Liveness

• Modified Phi also not acceptable:
  • x,y might be never changed!
  • Phi only expresses safety property.
  • Program must not execute other than described steps.
• Liveness properties:
  • Something does eventually happen.
  • Program must eventually perform described steps.
• Dijkstra semantics:
  • Infinitely many steps increase x or y.
  • Phi <=> Init_Phi and always A_<x, y> and always eventually A.
• Add fairness requirement:
  • Infinitely many steps increase x and y.
  • Phi <=> Init_Phi and always A_<x, y> and always eventually A₁ and always eventually A₂.

Problem: Both are not TLA formulas!