1 2 3 4 5 1 2 3 4 5

Nr Name Value Previous Value
1 battery ? ?
2 battery_actual ? ?
3 concrete_position ? ?
4 current_position ? ?
5 current_time ? ?
6 cycle ? ?
7 emergency_mode ? ?
8 field ? ?
9 init ? ?
10 last_time ? ?
11 mission_failed ? ?
12 mode ? ?
13 position_actual ? ?
14 reward ? ?
15 sensor_data_actual ? ?
16 socket ? ?
17 visited ? ?
Nr Name Value
1 BATTERY_STEP 2
2 WIDTH 5
3 DEPTH 5
4 BASE_POSITION (2|->1)
5 CONCRETE_DEPTH 3000
6 MAP_TO_ABSTRACT_POS /*@symbolic*/ %p.(p : INTEGER|(IF p >= 0 THEN p / 600 + 1 ELSE p / 600 END))
7 SAFETY_DISTANCE 0
8 GRID_SIZE 600
9 CONCRETE_WIDTH 3000
10 DroneCommunicator_Param_replay.drone_url "Drone"
Nr Name Value
1 MODES {LANDED,FLYING,FINISHED}
2 INT (-1 .. 3)
Nr Name Enabled
1 MAIN_TAKEOFF ?
2 MAIN_LEFT ?
3 MAIN_RIGHT ?
4 MAIN_FORWARD ?
5 MAIN_BACKWARD ?
6 MAIN_LAND ?
7 MAIN_OBSERVE ?
8 MAIN_SYNCHRONIZE_BATTERY ?
9 MAIN_UPDATE_POSITION ?
Nr Event Target State ID
1SETUP_CONSTANTS(BASE_POSITION=(2↦1))State 1
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(600↦0),current_position=(2↦1),current_time=0,cycle=1,...
3MAIN_SYNCHRONIZE_BATTERY(current_time=7759)
4MAIN_TAKEOFF(current_time=11320,last_time=7759)
5MAIN_SYNCHRONIZE_BATTERY(current_time=12079,last_time=11320)
6MAIN_UPDATE_POSITION(current_time=12991,last_time=12079)
7MAIN_SYNCHRONIZE_BATTERY(current_time=13913,last_time=12991)
8MAIN_OBSERVE(current_time=14953,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
9MAIN_SYNCHRONIZE_BATTERY(current_time=15621,last_time=14953)
10MAIN_LEFT(concrete_position=(1200↦573),current_time=18664,last_time=15621,reward=4.5)
11MAIN_SYNCHRONIZE_BATTERY(current_time=19604,last_time=18664)
12MAIN_UPDATE_POSITION(current_time=20961,last_time=19604)
13MAIN_SYNCHRONIZE_BATTERY(current_time=21465,last_time=20961)
14MAIN_OBSERVE(current_time=21936,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
15MAIN_SYNCHRONIZE_BATTERY(current_time=22343,last_time=21936)
16MAIN_LEFT(concrete_position=(1800↦517),current_time=24735,last_time=22343,reward=3.140816326530612)
17MAIN_SYNCHRONIZE_BATTERY(current_time=26054,last_time=24735)
18MAIN_UPDATE_POSITION(current_time=27631,last_time=26054)
19MAIN_SYNCHRONIZE_BATTERY(current_time=28402,last_time=27631)
20MAIN_OBSERVE(current_time=29031,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
21MAIN_SYNCHRONIZE_BATTERY(current_time=29556,last_time=29031)
22MAIN_RIGHT(concrete_position=(1200↦462),current_time=31894,last_time=29556,reward=-0.3125)
23MAIN_SYNCHRONIZE_BATTERY(current_time=32675,last_time=31894)
24MAIN_UPDATE_POSITION(current_time=33632,last_time=32675)
25MAIN_SYNCHRONIZE_BATTERY(current_time=34006,last_time=33632)
26MAIN_OBSERVE(current_time=34361,last_time=34006)
27MAIN_SYNCHRONIZE_BATTERY(current_time=34663,last_time=34361)
28MAIN_FORWARD(concrete_position=(1289↦600),current_time=36609,last_time=34663,reward=4.32127659574468)
29MAIN_SYNCHRONIZE_BATTERY(current_time=37525,last_time=36609)
30MAIN_UPDATE_POSITION(current_time=38606,last_time=37525)
31MAIN_SYNCHRONIZE_BATTERY(current_time=39131,last_time=38606)
32MAIN_OBSERVE(current_time=39610,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
33MAIN_SYNCHRONIZE_BATTERY(current_time=40021,last_time=39610)
34MAIN_FORWARD(concrete_position=(1348↦1200),current_time=41997,last_time=40021,reward=17.347826086956523)
35MAIN_SYNCHRONIZE_BATTERY(current_time=43102,last_time=41997)
36MAIN_UPDATE_POSITION(current_time=43493,last_time=43102)
37MAIN_SYNCHRONIZE_BATTERY(current_time=44333,last_time=43493)
38MAIN_OBSERVE(current_time=44725,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦1),(2↦4↦0),(2↦5↦0),(...
39MAIN_SYNCHRONIZE_BATTERY(current_time=45031,last_time=44725)
40MAIN_FORWARD(concrete_position=(1385↦1800),current_time=47175,last_time=45031,reward=20.766666666666666)
41MAIN_SYNCHRONIZE_BATTERY(current_time=48526,last_time=47175)
42MAIN_UPDATE_POSITION(current_time=49111,last_time=48526)
43MAIN_SYNCHRONIZE_BATTERY(current_time=49820,last_time=49111)
44MAIN_OBSERVE(current_time=50533,field={(1↦1↦2),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦1),(2↦2↦1),(2↦3↦1),(2↦4↦1),(2↦5↦0),(...
45MAIN_SYNCHRONIZE_BATTERY(current_time=51261,last_time=50533)
Generated on 15/1/2026 at 13:23 using ProB version 1.16.0-nightly
Main specification file: ../DroneMainController_replay.mch (modified on 14/1/2026 at 16:09)
Main specification name: DroneMainController_replay
Main VisB JSON file: ../visualization/Drone_VisB_Mockup.def (modified on 15/1/2026 at 13:22)