#From every state, every path will visit floor 0 (1,2, and 3, respectively) eventually AG(AF(position<1>=0 * position<0>=0)); AG(AF(position<1>=0 * position<0>=1)); AG(AF(position<1>=1 * position<0>=0)); AG(AF(position<1>=1 * position<0>=1)); #the four formulas have the same meaning #AG(AF(position[1:0]=0)); #AG(AF(position[1:0]=1)); #AG(AF(position[1:0]=2)); #AG(AF(position[1:0]=3)); #From every state there is a path to reach floor 0 (1, 2, and 3) AG(EF(position[1:0]=0)); AG(EF(position[1:0]=1)); AG(EF(position[1:0]=2)); AG(EF(position[1:0]=3)); #there is a path from the initial state in which the elevator stays in floor 0 forever EG(position[1:0]=0); #In all reachable states, we can find a path to a state from which there is a path along with the elevator does not move AG(EF(EG(moving=0))); #whenever there is no outstanding request, the elevator does not move. AG(outstanding=0 -> AX(moving=0)); #whenever floor 0 is requests, we will reach floor 0 on all possible paths AG(requests[0]=1 -> AF(position[1:0]=0)); AG(requests[1]=1 -> AF(position[1:0]=1)); AG(requests[2]=1 -> AF(position[1:0]=2)); AG(requests[3]=1 -> AF(position[1:0]=3));