model/elevator: -- specification  G ( F c.e.cabin_at = 0)  is true