def state_invariant():
    # p => q can be expressed:  not p or q
    return power == 'Off' or door == 'Closed'
Safety requirement: power == 'On' => door == 'Closed'
dataset/ETHPy150Open jon-jacky/PyModel/samples/safety/oven.py/state_invariant