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 (5|->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=(5↦1),MAP_TO_ABSTRACT_POS=/*@symbolic*/ λp.(p ∈ ℤ∣(IF p ≥ 0 THEN p ÷ 600 + 1 ELSE p ÷ 600 ...State 4
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(2400↦0),current_position=(5↦1),current_time=0,cycle=1...
3MAIN_SYNCHRONIZE_BATTERY(current_time=7860)
4MAIN_TAKEOFF(current_time=11851,last_time=7860)
5MAIN_SYNCHRONIZE_BATTERY(current_time=12595,last_time=11851)
6MAIN_UPDATE_POSITION(current_time=12987,last_time=12595)
7MAIN_SYNCHRONIZE_BATTERY(current_time=13373,last_time=12987)
8MAIN_OBSERVE(current_time=13812,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
9MAIN_SYNCHRONIZE_BATTERY(current_time=14187,last_time=13812)
10MAIN_RIGHT(concrete_position=(1800↦344),current_time=16472,last_time=14187,reward=3.0)
11MAIN_SYNCHRONIZE_BATTERY(current_time=17095,last_time=16472)
12MAIN_UPDATE_POSITION(current_time=18018,last_time=17095)
13MAIN_SYNCHRONIZE_BATTERY(current_time=18401,last_time=18018)
14MAIN_OBSERVE(current_time=19204,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
15MAIN_SYNCHRONIZE_BATTERY(current_time=19937,last_time=19204)
16MAIN_LEFT(concrete_position=(2400↦539),current_time=22657,last_time=19937,reward=-0.45918367346938777)
17MAIN_SYNCHRONIZE_BATTERY(current_time=23803,last_time=22657)
18MAIN_UPDATE_POSITION(current_time=24964,last_time=23803)
19MAIN_SYNCHRONIZE_BATTERY(current_time=25562,last_time=24964)
20MAIN_OBSERVE(current_time=26088,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
21MAIN_SYNCHRONIZE_BATTERY(current_time=26513,last_time=26088)
22MAIN_FORWARD(concrete_position=(2876↦1200),current_time=28924,last_time=26513,reward=16.90625)
23MAIN_SYNCHRONIZE_BATTERY(current_time=29903,last_time=28924)
24MAIN_UPDATE_POSITION(current_time=30324,last_time=29903)
25MAIN_SYNCHRONIZE_BATTERY(current_time=30703,last_time=30324)
26MAIN_OBSERVE(current_time=31071,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
27MAIN_SYNCHRONIZE_BATTERY(current_time=31491,last_time=31071)
28MAIN_FORWARD(concrete_position=(2674↦1200),current_time=34098,last_time=31491,reward=-0.7978723404255319)
29MAIN_SYNCHRONIZE_BATTERY(current_time=35223,last_time=34098)
30MAIN_UPDATE_POSITION(current_time=36290,last_time=35223)
31MAIN_SYNCHRONIZE_BATTERY(current_time=36924,last_time=36290)
32MAIN_OBSERVE(current_time=37472,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
33MAIN_SYNCHRONIZE_BATTERY(current_time=37951,last_time=37472)
34MAIN_FORWARD(concrete_position=(2719↦1800),current_time=40396,last_time=37951,reward=13.421739130434782)
35MAIN_SYNCHRONIZE_BATTERY(current_time=41390,last_time=40396)
36MAIN_UPDATE_POSITION(current_time=42288,last_time=41390)
37MAIN_SYNCHRONIZE_BATTERY(current_time=42589,last_time=42288)
38MAIN_OBSERVE(current_time=42857,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
39MAIN_SYNCHRONIZE_BATTERY(current_time=43115,last_time=42857)
40MAIN_RIGHT(concrete_position=(1800↦1889),current_time=44703,last_time=43115,reward=15.966666666666667)
41MAIN_SYNCHRONIZE_BATTERY(current_time=45416,last_time=44703)
42MAIN_UPDATE_POSITION(current_time=46343,last_time=45416)
43MAIN_SYNCHRONIZE_BATTERY(current_time=46873,last_time=46343)
44MAIN_OBSERVE(current_time=47463,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦0),(2↦5↦0),(...
45MAIN_SYNCHRONIZE_BATTERY(current_time=48063,last_time=47463)
46MAIN_RIGHT(concrete_position=(1200↦1903),current_time=50459,last_time=48063,reward=27.777272727272724)
47MAIN_SYNCHRONIZE_BATTERY(current_time=51384,last_time=50459)
48MAIN_UPDATE_POSITION(current_time=52162,last_time=51384)
49MAIN_SYNCHRONIZE_BATTERY(current_time=52560,last_time=52162)
50MAIN_OBSERVE(current_time=52937,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦0),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦0),(2↦4↦1),(2↦5↦0),(...
51MAIN_SYNCHRONIZE_BATTERY(current_time=53269,last_time=52937)
52MAIN_RIGHT(concrete_position=(600↦2037),current_time=55553,last_time=53269,reward=31.17906976744186)
53MAIN_SYNCHRONIZE_BATTERY(current_time=56267,last_time=55553)
54MAIN_UPDATE_POSITION(current_time=56478,last_time=56267)
55MAIN_SYNCHRONIZE_BATTERY(current_time=56751,last_time=56478)
56MAIN_OBSERVE(current_time=57071,field={(1↦1↦0),(1↦2↦0),(1↦3↦0),(1↦4↦1),(1↦5↦0),(2↦1↦0),(2↦2↦0),(2↦3↦1),(2↦4↦1),(2↦5↦1),(...
57MAIN_SYNCHRONIZE_BATTERY(current_time=57631,last_time=57071)
58MAIN_RIGHT(concrete_position=(0↦2078),current_time=60393,last_time=57631,reward=22.57142857142857)
59MAIN_SYNCHRONIZE_BATTERY(current_time=61423,last_time=60393)
60MAIN_UPDATE_POSITION(current_time=62296,last_time=61423)
61MAIN_SYNCHRONIZE_BATTERY(current_time=62661,last_time=62296)
62MAIN_OBSERVE(current_time=63022,field={(1↦1↦0),(1↦2↦0),(1↦3↦1),(1↦4↦1),(1↦5↦2),(2↦1↦0),(2↦2↦0),(2↦3↦1),(2↦4↦1),(2↦5↦1),(...
63MAIN_SYNCHRONIZE_BATTERY(current_time=63348,last_time=63022)
64MAIN_BACKWARD(concrete_position=(246↦1200),current_time=65035,last_time=63348,reward=11.919512195121952)
65MAIN_SYNCHRONIZE_BATTERY(current_time=65986,last_time=65035)
66MAIN_UPDATE_POSITION(current_time=66271,last_time=65986)
67MAIN_SYNCHRONIZE_BATTERY(current_time=66463,last_time=66271)
68MAIN_OBSERVE(current_time=66660,field={(1↦1↦0),(1↦2↦0),(1↦3↦2),(1↦4↦1),(1↦5↦2),(2↦1↦0),(2↦2↦1),(2↦3↦1),(2↦4↦1),(2↦5↦1),(...
69MAIN_SYNCHRONIZE_BATTERY(current_time=66842,last_time=66660)
70MAIN_BACKWARD(concrete_position=(651↦600),current_time=69367,last_time=66842,reward=15.225000000000001)
71MAIN_SYNCHRONIZE_BATTERY(current_time=70012,last_time=69367)
72MAIN_UPDATE_POSITION(current_time=70227,last_time=70012)
73MAIN_SYNCHRONIZE_BATTERY(current_time=70662,last_time=70227)
74MAIN_OBSERVE(current_time=71109,field={(1↦1↦0),(1↦2↦2),(1↦3↦2),(1↦4↦1),(1↦5↦2),(2↦1↦1),(2↦2↦1),(2↦3↦1),(2↦4↦1),(2↦5↦1),(...
75MAIN_SYNCHRONIZE_BATTERY(current_time=71530,last_time=71109)
76MAIN_BACKWARD(concrete_position=(672↦0),current_time=74149,last_time=71530,reward=14.876923076923077)
77MAIN_SYNCHRONIZE_BATTERY(current_time=74892,last_time=74149)
78MAIN_UPDATE_POSITION(current_time=75169,last_time=74892)
79MAIN_SYNCHRONIZE_BATTERY(current_time=75407,last_time=75169)
80MAIN_OBSERVE(current_time=75628,field={(1↦1↦2),(1↦2↦2),(1↦3↦2),(1↦4↦1),(1↦5↦2),(2↦1↦1),(2↦2↦1),(2↦3↦1),(2↦4↦1),(2↦5↦1),(...
81MAIN_SYNCHRONIZE_BATTERY(current_time=75821,last_time=75628)
82MAIN_LEFT(concrete_position=(1200↦418),current_time=78003,last_time=75821,reward=-2.1710526315789473)
83MAIN_SYNCHRONIZE_BATTERY(current_time=78557,last_time=78003)
84MAIN_UPDATE_POSITION(current_time=78835,last_time=78557)
85MAIN_SYNCHRONIZE_BATTERY(current_time=79021,last_time=78835)
86MAIN_OBSERVE(current_time=79201,last_time=79021)
87MAIN_SYNCHRONIZE_BATTERY(current_time=79409,last_time=79201)
88MAIN_LAND(current_time=80938,last_time=79409,reward=37.5)
Generated on 16/1/2026 at 9:47 using ProB version 1.16.0-nightly
Main specification file: ../DroneMainController_replay.mch (modified on 16/1/2026 at 9:39)
Main specification name: DroneMainController_replay
Main VisB JSON file: ../visualization/Drone_VisB_Mockup.def (modified on 16/1/2026 at 9:38)