|
Example Properties for TLC
Example Properties for TLC
- Invariant : It is never the case that both the highway and farm road have green simultaneously. The CTL formula saying this is
- If a car is waiting on the farm road, then eventually the farm road light turns green. The CTL formula saying this is
AG(!(hwy_light = green * farm_light = green))
AG(car_waiting -> AF(farm_light = green))
|
