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