AG(movement=MOVING -> door=CLOSED);
AG(buttons<*0*>=ON -> AF((door=OPEN) * location<0>=0 * location<1>=0));