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 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 blockedTime ?
2 blockedTimesProcessed ?
3 held_airplanes ?
4 landing_sequence ?
5 scheduledAirplanes ?
6 selectedAirplane ?
7 timeout ?
8 zoomLevel ?
Nr Name Value
1 AIRPLANE_POINTS_BY_ZOOM (/*@symbolic*/ %zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|(300 .. 474) ** ((%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|735 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) .. ((%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|735 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) + 40) - 1)))
2 DIST (/*@symbolic*/ %x|->y.x : INT & y : INT|max({y - x,x - y}))
3 ZOOM_SLIDER_HEIGHT 40
4 BLOCK_SLOT_WIDTH 15
5 BLOCK_SLOT_X 201
6 TIME_YS_BY_ZOOM (%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|755 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))
7 ZOOM_SLIDER_Y 50
8 HOLD_POINTS ((650 .. 769) ** (500 .. 529))
9 SCREEN_HEIGHT 800
10 HEIGHTS (10 .. 799)
11 HOLD_WIDTH 120
12 Y_COORDS (0 .. 799)
13 HOLD_Y 500
14 HOLD_X 650
15 POINTS ((0 .. 999) ** (0 .. 799))
16 X_COORDS (0 .. 999)
17 BLOCK_SLOT_POINTS_BY_ZOOM (%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|(201 .. 215) ** ((%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|(%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|755 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) - {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) .. ((%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|(%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|755 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) - {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) + {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)) - 1)))
18 AIRPLANE_YS_BY_ZOOM (%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|735 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))
19 SCREEN_WIDTH 1000
20 ZOOM_SLIDER_XS (%z.z : {x|x : (15 .. 45) & x mod 5 = 0}|708 + ((z - 15) / 5) * 40)
21 TIME_SLOT_YS_BY_ZOOM (%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|(%zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. zoom|755 - time * {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))(zoom)(time) - {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}(zoom)))
22 ZOOM_SLIDER_POINTS (%z.z : {x|x : (15 .. 45) & x mod 5 = 0}|((%z.z : {x|x : (15 .. 45) & x mod 5 = 0}|708 + ((z - 15) / 5) * 40)(z) .. ((%z.z : {x|x : (15 .. 45) & x mod 5 = 0}|708 + ((z - 15) / 5) * 40)(z) + 40) - 1) ** (50 .. 89))
23 AIRPLANE_X 300
24 ZOOM_SLIDER_WIDTH 40
25 AIRPLANE_HEIGHT 40
26 AIRPLANE_WIDTH 175
27 TIME_SLOT_HEIGHT_BY_ZOOM {(15|->42),(20|->33),(25|->27),(30|->23),(35|->19),(40|->18),(45|->15)}
28 WIDTHS (10 .. 999)
29 HOLD_HEIGHT 30
30 AIRCRAFT_SEPARATION_MIN 3
31 PLANNING_HORIZON 45
32 PLANNING_INTERVAL (1 .. 45)
33 MAX_ZOOM 45
34 ZOOM_LEVELS {x|x : (15 .. 45) & x mod 5 = 0}
35 MIN_ZOOM 15
Nr Name Value
1 AIRPLANES {AIRPLANES1,AIRPLANES2,AIRPLANES3,AIRPLANES4,AIRPLANES5,AIRPLANES6,AIRPLANES7,AIRPLANES8,AIRPLANES9,AIRPLANES10,AIRPLANES11,AIRPLANES12,AIRPLANES13,AIRPLANES14,AIRPLANES15}
2 mouse_positions {hold_button_pos,zoom_slider_pos,airplane_pos,block_time_pos,nothing_pos}
Nr Event Target State ID
1SETUP_CONSTANTS(AIRPLANE_POINTS_BY_ZOOM=(/*@symbolic*/ %zoom.zoom : {x|x : (15 .. 45) & x mod 5 = 0}|(%time.time : 1 .. ...State 0
2INITIALISATION(blockedTime={},blockedTimesProcessed=TRUE,held_airplanes={},landing_sequence={},scheduledAirplanes={},sel...
3AMAN_Update_AddPlanes({(AIRPLANES1|->3),(AIRPLANES2|->9)},0,{})
4AMAN_Update_AddPlanes({(AIRPLANES1|->3),(AIRPLANES2|->9),(AIRPLANES3|->15)},0,{})
5AMAN_Update_UnchangedPlanes({(AIRPLANES1|->3),(AIRPLANES2|->9),(AIRPLANES3|->15)},0,{})
6AMAN_Update_DeletePlanes({(AIRPLANES2|->9),(AIRPLANES3|->15)},0,{})
Generated on 2/2/2023 at 14:19 using ProB version 1.12.0-nightly
Main specification package: event_b_project
Main specification name: M6_Select_Airplane_vis
Main VisB JSON file: ../visualization/AMAN_vis.json (modified on 31/12/2022 at 1:43)
VisB SVG file: ../visualization/AMAN.svg (modified on 9/12/2022 at 9:52)