Sensor:
fps 28 11
Custom fps.srs
Sensor:
dest 27 119
Attribute dest 5 null 0 1
Sensor:
dos 99 206
Switch Off On doson dosoff null 0 1
Sensor:
dcs 94 275
Switch Off On dcson dcsoff null 0 1
Actuator:
lm 385 41
TwoWay Off Up Down goUp goOff goDown null 0 1
Actuator:
dm 387 189
TwoWay Off Opening Closing openDoor goOff closeDoor null 0 1
Safety Invariant:
fps = dest
lm = Off
Safety Invariant:
fps < dest & dcs = On
lm = Up
Safety Invariant:
fps > dest & dcs = On
lm = Down
Safety Invariant:
dest = fps & dos = Off
dm = Opening
Safety Invariant:
dest = fps & dos = On
dm = Off
Safety Invariant:
dest < fps & dcs = Off
dm = Closing
Safety Invariant:
dest < fps & dcs = On
dm = Off
Safety Invariant:
dest > fps & dcs = Off
dm = Closing
Safety Invariant:
dest > fps & dcs = On
dm = Off
Safety Invariant:
dcs = On
dos = Off