Controller Name
|
Controller File
|
Message Injector File
|
States / Transitions Tested
|
Number of passed assertions
|
Number of failed assertions
|
Test Results
|
Notes
|
| HallButtonControl |
hallbuttoncontrol.cf
|
hallbuttoncontrol_test1.mf
|
8.S.1, 8.S.2, 8.S.3, 8.T.1, 8.T.2, 8.T.3
|
8 |
0 |
hallbuttoncontrol_test1.stats
|
|
| CarButtonControl |
carbuttoncontrol.cf
|
carbuttoncontrol_test1.mf
|
9.S.1, 9.S.2, 9.T.1, 9.T.2,
|
8 |
0 |
carbuttoncontrol_test1.stats
|
|
DoorControl
|
doorcontrol.cf |
doorcontrol_test1.mf |
5.S.1, 5.S.2, 5.S.3, 5.S.4, 5.S.5, 5.S.6, 5.T.1, 5.T.2, 5.T.3, 5.T.4, 5.T.5, 5.T.6, 5.T.7, 5.T.8
|
18
|
0
|
doorcontrol_test1.stats
|
|
DoorControl
|
doorcontrol.cf |
doorcontrol_test2.mf |
5.S.1, 5.S.2, 5.S.3, 5.S.4, 5.S.5, 5.S.6, 5.T.1, 5.T.2, 5.T.3, 5.T.4, 5.T.5, 5.T.6, 5.T.7, 5.T.9
|
18
|
0
|
doorcontrol_test2.stats
|
|
LanternControl
|
lanterncontrol.cf
|
lanterncontrol_test1.mf
|
7.S.1, 7.S.2, 7.S.3, 7.T.1, 7.T.2, 7.T.3, 7.T.4
|
10
|
0
|
lanterncontrol_test1.stats
|
|
CarPositionControl
|
carpositioncontrol.cf
|
carpositioncontrol_test1.mf
|
10.S.1, 10.S.2, 10.T.1, 10.T.2
|
6
|
0
|
carpositioncontrol_test1.stats
|
|
Dispatcher
|
dispatcher.cf
|
dispatcher_test1.mf
|
11.S.1, 11.S.2, 11.S.3, 11.S.4, 11.S.5, 11.S.6, 11.T.1, 11.T.2, 11.T.3, 11.T.4, 11.T.5, 11.T.6, 11.T.7,
11.T.8, 11.T.9, 11.T.10
|
65
|
0
|
dispatcher_test1.stats
|
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test1.mf
|
6.S.1, 6.S.2, 6.S.3, 6.S.4, 6.T.1, 6.T.2, 6.T.3, 6.T.4, 6.T.5, 6.T.6
|
42
|
0
|
drivecontrol_test1.stats
|
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test2.mf
|
6.S.1, 6.S.2, 6.S.3, 6.S.4, 6.T.1, 6.T.2, 6.T.3, 6.T.4, 6.T.5, 6.T.6
|
42
|
0
|
drivecontrol_test2.stats
|
Take OR of transition 6.T.2 and 6.T.6
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test3.mf
|
6.S.1, 6.S.2, 6.S.3, 6.S.4, 6.T.1, 6.T.2, 6.T.3, 6.T.4, 6.T.5, 6.T.6
|
42
|
0
|
drivecontrol_test3.stats
|
Take last OR of transition 6.T.6
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test4.mf
|
6.S.1, 6.S.2, 6.S.3, 6.T.1, 6.T.2, 6.T.16
|
24
|
0
|
drivecontrol_test4.stats
|
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test5.mf
|
6.S.1, 6.S.2, 6.S.3, 6.S.4, 6.T.1, 6.T.2, 6.T.3, 6.T.13
|
30
|
0
|
drivecontrol_test5.stats
|
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test6.mf
|
6.S.1, 6.S.5, 6.S.6, 6.S.7, 6.T.7, 6.T.8, 6.T.9, 6.T.10, 6.T.11, 6.T.12
|
42
|
0
|
drivecontrol_test6.stats
|
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test7.mf
|
6.S.1, 6.S.5, 6.S.6, 6.S.7, 6.T.7, 6.T.8, 6.T.9, 6.T.10, 6.T.11, 6.T.12
|
42
|
0
|
drivecontrol_test7.stats
|
Take OR of transition 6.T.7 and 6.T.12
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test8.mf
|
6.S.1, 6.S.5, 6.S.6, 6.S.7, 6.T.7, 6.T.8, 6.T.9, 6.T.10, 6.T.11, 6.T.12
|
42
|
0
|
drivecontrol_test8.stats
|
Take last OR of transition 6.T.12
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test9.mf
|
6.S.1, 6.S.5, 6.S.6, 6.T.7, 6.T.8, 6.T.14
|
24
|
0
|
drivecontrol_test9.stats
|
Emergency stop
|
DriveControl
|
drivecontrol.cf
|
drivecontrol_test10.mf
|
6.S.1, 6.S.5, 6.S.6, 6.S.7, 6.T.7, 6.T.8, 6.T.9, 6.T.15
|
30
|
0
|
drivecontrol_test10.stats
|
Emergency stop
|