button E array 1..3 of boolean Request button at floor i floor S 1..3 The floor the cabin is located door S {open,closed} The status of the cabin door direction S {standing,moving} The status of the elevator service S array 1..3 of boolean Elevator services a request at floor i R1 forall i in {1:3} : G (service[i] <-> (floor=i && door=open)) G The definition of service 1 R2 forall i in {1:3} : G(button[i] -> F(service[i])) G A request if eventually serviced 1 R3 G (door=open -> direction=standing) G The door is open only if the elevator is standing 1 R4 forall i in {1:3} : G(floor=i -> (next(floor) <= i + 1) && next(floor) >= i - 1) G Elevator can move at most one floor at a time 1 R5 forall i in {1:3} : G((direction=standing && floor = i) -> (next(floor) = i)) G The floor does not change when the elevator is standing 1 R6 forall i in {1:3} : G((direction=moving && floor = i) -> (next(floor) != i)) G If the elevator is moving, the floor changes 1 R7 forall i in {1:3} : G(button[i] -> [button[i] U service[i]]) G A request can be reset only after service 1 R8 forall i in {1:3} : G(service[i] -> next(!button[i])) G Service resets the corresponding request 1 R9 forall i in {1:3} : [!service[i] U button[i]] G No service is granted unless there is a request (FLAWED) 1 R10 forall i in {1:3} : G(service[i] -> next([!service[i] U button[i]])) G No further service is granted unless there is a request (FLAWED) 1 R9-2 forall i in {1:3} : [!service[i] W button[i]] G No service is granted unless there is a request (CORRECT) 0 R10-2 forall i in {1:3} : G(service[i] -> next([!service[i] W button[i]])) G No further service is granted unless there is a request (CORRECT) 0 P1 forall i in {1:3} : (!button[i]) passed Initially there are no requests 0 P2 forall i in {1:3} : G(!button[i]) passed There are no request at all 0 P3 forall i in {1:3} : F G(!button[i]) passed Eventually there are no requests 0 A1 forall i in {1:3} : G(service[i] -> direction=standing) passed Service is granted only if the elevator is standing 0 A2 forall i in {1:3} : G(service[i] -> next(!service[i])) passed A service is never followed by another service 0 New no This is the category of those traces that have been just created Default no This is the default category for traces Out of Date no Contains the traces whose dependencies might be no longer consistent Trash no Contains the traces that have been deleted Trace_0 R1 R2 R3 R4 R5 R6 R7 R8 A2 9 button[1] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 button[2] boolean 0 1 1 1 2 1 3 1 4 1 5 0 6 0 7 0 8 0 9 0 button[3] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 0 floor enumerative 0 3 1 3 2 3 3 3 4 3 5 2 6 2 7 3 8 3 9 3 door enumerative 0 open 1 closed 2 open 3 open 4 closed 5 open 6 closed 7 open 8 closed 9 closed direction enumerative 0 standing 1 standing 2 standing 3 standing 4 moving 5 standing 6 moving 7 standing 8 standing 9 standing service[1] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 0 service[2] boolean 0 0 1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 0 service[3] boolean 0 1 1 0 2 1 3 1 4 0 5 0 6 0 7 1 8 0 9 0 Created by 'NuSMV' on Sun Mar 15 17:39:21 2009 Checking command was: 'check_pslspec' (((forall i in {1:3} : G (service[i] <-> (floor=i && door=open))) & (forall i in {1:3} : G(button[i] -> F(service[i]))) & (G (door=open -> direction=standing)) & (forall i in {1:3} : G(floor=i -> (next(floor) <= i + 1) && next(floor) >= i - 1)) & (forall i in {1:3} : G((direction=standing && floor = i) -> (next(floor) = i))) & (forall i in {1:3} : G((direction=moving && floor = i) -> (next(floor) != i))) & (forall i in {1:3} : G(button[i] -> [button[i] U service[i]])) & (forall i in {1:3} : G(service[i] -> next(!button[i])))) -> (forall i in {1:3} : G(service[i] -> next(!service[i])))) Added to category 'New'\Removed from category 'New'\Added to category 'Trash' Trace_1 R1 R2 R3 R4 R5 R6 R7 R8 R9 R10 P1 1, 2 button[1] boolean 0 0 1 0 2 0 3 0 4 1 5 1 6 1 7 1 8 1 9 0 10 0 11 0 12 0 13 0 14 0 15 0 16 1 17 0 18 0 button[2] boolean 0 0 1 0 2 1 3 0 4 1 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 1 15 0 16 0 17 0 18 0 button[3] boolean 0 0 1 0 2 1 3 1 4 1 5 1 6 0 7 0 8 0 9 0 10 0 11 1 12 0 13 0 14 0 15 0 16 0 17 0 18 0 floor enumerative 0 2 1 2 2 2 3 2 4 2 5 2 6 3 7 3 8 2 9 1 10 1 11 2 12 3 13 3 14 2 15 2 16 1 17 1 18 2 door enumerative 0 closed 1 closed 2 open 3 closed 4 open 5 closed 6 open 7 closed 8 closed 9 open 10 closed 11 closed 12 open 13 closed 14 open 15 closed 16 open 17 closed 18 closed direction enumerative 0 standing 1 standing 2 standing 3 standing 4 standing 5 moving 6 standing 7 moving 8 moving 9 standing 10 moving 11 moving 12 standing 13 moving 14 standing 15 moving 16 standing 17 moving 18 standing service[1] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 12 0 13 0 14 0 15 0 16 1 17 0 18 0 service[2] boolean 0 0 1 0 2 1 3 0 4 1 5 0 6 0 7 0 8 0 9 0 10 0 11 0 12 0 13 0 14 1 15 0 16 0 17 0 18 0 service[3] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 0 10 0 11 0 12 1 13 0 14 0 15 0 16 0 17 0 18 0 Created by 'NuSMV' on Sun Mar 15 17:41:52 2009 Checking command was: 'check_pslspec' !((forall i in {1:3} : G (service[i] <-> (floor=i && door=open))) & (forall i in {1:3} : G(button[i] -> F(service[i]))) & (G (door=open -> direction=standing)) & (forall i in {1:3} : G(floor=i -> (next(floor) <= i + 1) && next(floor) >= i - 1)) & (forall i in {1:3} : G((direction=standing && floor = i) -> (next(floor) = i))) & (forall i in {1:3} : G((direction=moving && floor = i) -> (next(floor) != i))) & (forall i in {1:3} : G(button[i] -> [button[i] U service[i]])) & (forall i in {1:3} : G(service[i] -> next(!button[i]))) & (forall i in {1:3} : [!service[i] U button[i]]) & (forall i in {1:3} : G(service[i] -> next([!service[i] U button[i]]))) & (forall i in {1:3} : (!button[i]))) Added to category 'New'\Removed from category 'New'\Added to category 'Trash' Trace_2 R1 R2 R3 R4 R5 R6 R7 R8 R9-2 R10-2 P2 1 button[1] boolean 0 0 1 0 button[2] boolean 0 0 1 0 button[3] boolean 0 0 1 0 floor enumerative 0 2 1 2 door enumerative 0 closed 1 closed direction enumerative 0 standing 1 standing service[1] boolean 0 0 1 0 service[2] boolean 0 0 1 0 service[3] boolean 0 0 1 0 Created by 'NuSMV' on Sun Mar 15 17:42:42 2009 Checking command was: 'check_pslspec' !((forall i in {1:3} : G (service[i] <-> (floor=i && door=open))) & (forall i in {1:3} : G(button[i] -> F(service[i]))) & (G (door=open -> direction=standing)) & (forall i in {1:3} : G(floor=i -> (next(floor) <= i + 1) && next(floor) >= i - 1)) & (forall i in {1:3} : G((direction=standing && floor = i) -> (next(floor) = i))) & (forall i in {1:3} : G((direction=moving && floor = i) -> (next(floor) != i))) & (forall i in {1:3} : G(button[i] -> [button[i] U service[i]])) & (forall i in {1:3} : G(service[i] -> next(!button[i]))) & (forall i in {1:3} : [!service[i] W button[i]]) & (forall i in {1:3} : G(service[i] -> next([!service[i] W button[i]]))) & (forall i in {1:3} : G(!button[i]))) Added to category 'New'\Removed from category 'New'\Added to category 'Trash' Trace_3 R1 R2 R3 R4 R5 R6 R7 R8 R9-2 R10-2 P3 11 button[1] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 1 9 0 10 0 11 0 button[2] boolean 0 0 1 0 2 0 3 0 4 0 5 1 6 0 7 0 8 0 9 0 10 0 11 0 button[3] boolean 0 1 1 0 2 1 3 0 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 floor enumerative 0 3 1 3 2 2 3 3 4 3 5 2 6 2 7 2 8 2 9 1 10 1 11 1 door enumerative 0 open 1 closed 2 closed 3 open 4 closed 5 closed 6 open 7 closed 8 closed 9 open 10 closed 11 closed direction enumerative 0 standing 1 moving 2 moving 3 standing 4 moving 5 standing 6 standing 7 standing 8 moving 9 standing 10 standing 11 standing service[1] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 0 7 0 8 0 9 1 10 0 11 0 service[2] boolean 0 0 1 0 2 0 3 0 4 0 5 0 6 1 7 0 8 0 9 0 10 0 11 0 service[3] boolean 0 1 1 0 2 0 3 1 4 0 5 0 6 0 7 0 8 0 9 0 10 0 11 0 Created by 'NuSMV' on Sun Mar 15 17:42:49 2009 Checking command was: 'check_pslspec' !((forall i in {1:3} : G (service[i] <-> (floor=i && door=open))) & (forall i in {1:3} : G(button[i] -> F(service[i]))) & (G (door=open -> direction=standing)) & (forall i in {1:3} : G(floor=i -> (next(floor) <= i + 1) && next(floor) >= i - 1)) & (forall i in {1:3} : G((direction=standing && floor = i) -> (next(floor) = i))) & (forall i in {1:3} : G((direction=moving && floor = i) -> (next(floor) != i))) & (forall i in {1:3} : G(button[i] -> [button[i] U service[i]])) & (forall i in {1:3} : G(service[i] -> next(!button[i]))) & (forall i in {1:3} : [!service[i] W button[i]]) & (forall i in {1:3} : G(service[i] -> next([!service[i] W button[i]]))) & (forall i in {1:3} : F G(!button[i]))) Added to category 'New'\Removed from category 'New'\Added to category 'Trash' pa