Example: Dining Philosophers Problem

Browse: DP.csv

Add: Philo:1.state,Philo:2.state,Philo:3.state,Philo:4.state,Philo:5.state

Abbreviations: Philo:1.state= p1,Philo:2.state = p2,Philo:3.state = p3,Philo:4.state = p4,Philo:5.state = p5

Properties:

// Safety Property - will hold for all runs

G [ (p1 = "E" -> p2 != "E") &&
    (p2 = "E" -> p3 != "E") &&
    (p3 = "E" -> p4 != "E") &&
    (p4 = "E" -> p5 != "E") &&
    (p5 = "E" -> p1 != "E")
] 

// Liveness - need not hold for every run

G [ (p1 = "H" -> F [ p1 = "E" ]) &&
    (p2 = "H" -> F [ p2 = "E" ]) &&
    (p3 = "H" -> F [ p3 = "E" ]) &&
    (p4 = "H" -> F [ p4 = "E" ]) &&
    (p5 = "H" -> F [ p5 = "E" ])
  ]