Download as a PDF

farm_light:RED
hwy_light:GREEN
timer.state:LONG
fails ((car_present=YES * timer.state=LONG) -> AF(farm_light=GREEN))
--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG
passes (car_present=YES * timer.state=LONG)
--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG
passes car_present=YES
--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG
passes timer.state=LONG
--State
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG
fails AF(farm_light=GREEN)
--A fair path on which farm_light=GREEN is always false:
--Fair path stem:
--State 0:
car_present:YES
farm_light:RED
hwy_light:GREEN
timer.state:LONG
--Goes to state 1:
hwy_light:YELLOW
timer.state:START
--On input:
sensor.rand_choice:1
timer.rand_choice:0
--Fair path cycle:
--State 0:
car_present:YES
farm_light:RED
hwy_light:YELLOW
timer.state:START
--Goes to state 1:
<Unchanged>
32