5 10 15 20 25 30 35 40 45 AIRPLANE1 AIRPLANE2 AIRPLANE3 AIRPLANE4 AIRPLANE5 AIRPLANE6 AIRPLANE7 AIRPLANE8 AIRPLANE9 AIRPLANE10 AIRPLANE11 AIRPLANE12 AIRPLANE13 AIRPLANE14 AIRPLANE15 HOLD Time 15 20 25 30 35 40 45 AMAN is not functioning! :01 :02 :03 :04 :05 :06 :07 :08 :09 :10 :11 :12 :13 :14 :15 :16 :17 :18 :19 :20 :21 :22 :23 :24 :25 :26 :27 :28 :29 :30 :31 :32 :33 :34 :35 :36 :37 :38 :39 :40 :41 :42 :43 :44 :45

Nr Name Value
1 arrivalH_T ?
2 arrivalM_T ?
3 blockedZones_T ?
4 clickedElement ?
5 curTimeH ?
6 curTimeM ?
7 curTimeS ?
8 diplayedLabels ?
9 holdLabels_T ?
10 isStopped ?
11 labels_T ?
12 mousePosition ?
13 mouseState ?
14 newArrivalH_T ?
15 newArrivalM_T ?
16 requests_T ?
17 selectedElement ?
18 zoomLevel ?
Nr Name Value
1 Minutes {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59}
2 zoomLevels {15,20,25,30,35,40,45}
3 Hours {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23}
4 Seconds {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59}
5 Labels {Elements4,Elements5,Elements6,Elements7,Elements8,Elements9,Elements10,Elements11,Elements12,Elements13}
6 sep 3
7 step 10
Nr Name Value
1 Elements {nothing,hold,zoom,Elements4,Elements5,Elements6,Elements7,Elements8,Elements9,Elements10,Elements11,Elements12,Elements13}
2 mouseStates {released,clicked}
Nr Event Description Target State ID
1SETUP_CONSTANTS(Minutes={0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,...State 0
2INITIALISATION(zoomLevel=15)
3addLabel(Elements4,0)add plane Elements4 (at time 0 secs)
4display({},{},10,10,{},{},10,0,0,{})update display after AMAN updates for {}, advance time to 0h:0m 10s, {} landed
5addRequest(1,0,Elements4,1,1,10)add a request to AMAN to add plane Elements4 to the landing sequence
6display({(Elements4|->4)},{},20,20,{Elements4},{Elements4},20,0,0,{})update display after AMAN updates for {Elements4}, advance time to 0h:0m 20s, {} landed
7addBlockedZone(0,4,20)block time slot 0h:4m for planes
8addBlockedZone(0,5,20)block time slot 0h:5m for planes
9display({(Elements4|->3)},{},30,30,{Elements4},{Elements4},30,0,0,{})update display after AMAN updates for {Elements4}, advance time to 0h:0m 30s, {} landed
10addBlockedZone(0,3,30)block time slot 0h:3m for planes
11addBlockedZone(0,2,30)block time slot 0h:2m for planes
12addBlockedZone(0,1,30)block time slot 0h:1m for planes
13display({(Elements4|->6)},{},40,40,{Elements4},{Elements4},40,0,0,{})update display after AMAN updates for {Elements4}, advance time to 0h:0m 40s, {} landed
14display({(Elements4|->6)},{},50,50,{Elements4},{Elements4},50,0,0,{})update display after AMAN updates for {Elements4}, advance time to 0h:0m 50s, {} landed
15display({(Elements4|->6)},{},0,60,{Elements4},{Elements4},60,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 0s, {} landed
16display({(Elements4|->6)},{},10,70,{Elements4},{Elements4},70,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 10s, {} landed
17display({(Elements4|->6)},{},20,80,{Elements4},{Elements4},80,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 20s, {} landed
18display({(Elements4|->6)},{},30,90,{Elements4},{Elements4},90,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 30s, {} landed
19display({(Elements4|->6)},{},40,100,{Elements4},{Elements4},100,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 40s, {} landed
20display({(Elements4|->6)},{},50,110,{Elements4},{Elements4},110,0,1,{})update display after AMAN updates for {Elements4}, advance time to 0h:1m 50s, {} landed
21display({(Elements4|->6)},{},0,120,{Elements4},{Elements4},120,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 0s, {} landed
22display({(Elements4|->6)},{},10,130,{Elements4},{Elements4},130,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 10s, {} landed
23deleteBlockedZone(0,5,130)unblock a time slot 0h:5m
24display({(Elements4|->6)},{},20,140,{Elements4},{Elements4},140,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 20s, {} landed
25display({(Elements4|->6)},{},30,150,{Elements4},{Elements4},150,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 30s, {} landed
26deleteBlockedZone(0,4,150)unblock a time slot 0h:4m
27addBlockedZone(0,6,150)block time slot 0h:6m for planes
28display({(Elements4|->4)},{},40,160,{Elements4},{Elements4},160,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 40s, {} landed
29display({(Elements4|->4)},{},50,170,{Elements4},{Elements4},170,0,2,{})update display after AMAN updates for {Elements4}, advance time to 0h:2m 50s, {} landed
30display({(Elements4|->4)},{},0,180,{Elements4},{Elements4},180,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 0s, {} landed
31addLabel(Elements13,180)add plane Elements13 (at time 180 secs)
32addBlockedZone(0,5,180)block time slot 0h:5m for planes
33display({(Elements4|->4)},{},10,190,{Elements4},{Elements4},190,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 10s, {} landed
34display({(Elements4|->4)},{},20,200,{Elements4},{Elements4},200,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 20s, {} landed
35display({(Elements4|->4)},{},30,210,{Elements4},{Elements4},210,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 30s, {} landed
36display({(Elements4|->4)},{},40,220,{Elements4},{Elements4},220,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 40s, {} landed
37display({(Elements4|->4)},{},50,230,{Elements4},{Elements4},230,0,3,{})update display after AMAN updates for {Elements4}, advance time to 0h:3m 50s, {} landed
38display({},{Elements4},0,240,{},{},240,0,4,{})update display after AMAN updates for {}, advance time to 0h:4m 0s, {Elements4} landed
Generated on 13/2/2024 at 14:17 using ProB version 1.13.0-nightly
Main specification file: M8_mch.eventb (modified on 13/2/2024 at 14:17)
Main specification name: M8
Main VisB JSON file: visualization/AMAN_M8_vis.json (modified on 6/2/2024 at 14:46)
VisB SVG file: visualization/AMAN.svg (modified on 23/1/2023 at 20:03)