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 JsonValue /*@symbolic*/ {`_freetype_arg19`|(`_freetype_arg19` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg19`) : FLOAT) & (`_freetype_arg19` : ran(JsonArray) => (JsonArray~)(`_freetype_arg19`) : seq(recursive.`20`)) & (`_freetype_arg19` : ran(JsonObject) => (JsonObject~)(`_freetype_arg19`) : STRING +-> recursive.`20`)}
2 JsonNull JsonNull
3 JsonBoolean /*@symbolic*/ {`_constr_arg21`,`_constr_res22`|`_constr_res22` = JsonBoolean(`_constr_arg21`)}
4 JsonNumber /*@symbolic*/ %`_constr_arg23`.(`_constr_arg23` : FLOAT|JsonNumber(`_constr_arg23`))
5 JsonString /*@symbolic*/ {`_constr_arg25`,`_constr_res26`|`_constr_res26` = JsonString(`_constr_arg25`)}
6 JsonArray /*@symbolic*/ %`_constr_arg27`.(`_constr_arg27` : seq(/*@symbolic*/ {`_freetype_arg19`|(`_freetype_arg19` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg19`) : FLOAT) & (`_freetype_arg19` : ran(JsonArray) => (JsonArray~)(`_freetype_arg19`) : seq(recursive.`20`)) & (`_freetype_arg19` : ran(JsonObject) => (JsonObject~)(`_freetype_arg19`) : STRING +-> recursive.`20`)})|JsonArray(`_constr_arg27`))
7 JsonObject /*@symbolic*/ %`_constr_arg29`.(`_constr_arg29` : STRING +-> /*@symbolic*/ {`_freetype_arg19`|(`_freetype_arg19` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg19`) : FLOAT) & (`_freetype_arg19` : ran(JsonArray) => (JsonArray~)(`_freetype_arg19`) : seq(recursive.`20`)) & (`_freetype_arg19` : ran(JsonObject) => (JsonObject~)(`_freetype_arg19`) : STRING +-> recursive.`20`)}|JsonObject(`_constr_arg29`))
8 RpcResult /*@symbolic*/ {`_freetype_arg31`|`_freetype_arg31` : ran(RpcSuccess) => (RpcSuccess~)(`_freetype_arg31`) : /*@symbolic*/ {`_freetype_arg19`|(`_freetype_arg19` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg19`) : FLOAT) & (`_freetype_arg19` : ran(JsonArray) => (JsonArray~)(`_freetype_arg19`) : seq(recursive.`20`)) & (`_freetype_arg19` : ran(JsonObject) => (JsonObject~)(`_freetype_arg19`) : STRING +-> recursive.`20`)}}
9 RpcSuccess /*@symbolic*/ %`_constr_arg33`.(`_constr_arg33` : /*@symbolic*/ {`_freetype_arg19`|(`_freetype_arg19` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg19`) : FLOAT) & (`_freetype_arg19` : ran(JsonArray) => (JsonArray~)(`_freetype_arg19`) : seq(recursive.`20`)) & (`_freetype_arg19` : ran(JsonObject) => (JsonObject~)(`_freetype_arg19`) : STRING +-> recursive.`20`)}|RpcSuccess(`_constr_arg33`))
10 RpcError /*@symbolic*/ {`_constr_arg35`,`_constr_res36`|`_constr_res36` = RpcError(`_constr_arg35`)}
11 BATTERY_STEP 2
12 WIDTH 5
13 DEPTH 5
14 BASE_POSITION (2|->2)
15 CONCRETE_DEPTH 3000
16 MAP_TO_ABSTRACT_POS /*@symbolic*/ %p.(p : INTEGER|(IF p >= 0 THEN p / 600 + 1 ELSE p / 600 END))
17 SAFETY_DISTANCE 0
18 GRID_SIZE 600
19 CONCRETE_WIDTH 3000
20 DroneCommunicator_Param.drone_url "radio://0/80/2M/5700B500F3"
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↦2))State 1
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(600↦600),current_position=(2↦2),current_time=0,cycle=...
3MAIN_SYNCHRONIZE_BATTERY
4MAIN_TAKEOFF
5MAIN_SYNCHRONIZE_BATTERY
6MAIN_UPDATE_POSITION
7MAIN_SYNCHRONIZE_BATTERY
8MAIN_OBSERVE
9MAIN_SYNCHRONIZE_BATTERY
10MAIN_FORWARD(concrete_position=(669↦2400),reward=4.2)
11MAIN_SYNCHRONIZE_BATTERY
12MAIN_UPDATE_POSITION
13MAIN_SYNCHRONIZE_BATTERY
14MAIN_OBSERVE
15MAIN_SYNCHRONIZE_BATTERY
16MAIN_LEFT(concrete_position=(1200↦2066),reward=6.43469387755102)
17MAIN_SYNCHRONIZE_BATTERY
18MAIN_UPDATE_POSITION
19MAIN_SYNCHRONIZE_BATTERY
20MAIN_OBSERVE
21MAIN_SYNCHRONIZE_BATTERY
22MAIN_LEFT(concrete_position=(1800↦2010),reward=13.774999999999999)
23MAIN_SYNCHRONIZE_BATTERY
24MAIN_UPDATE_POSITION
25MAIN_SYNCHRONIZE_BATTERY
26MAIN_OBSERVE
27MAIN_SYNCHRONIZE_BATTERY
28MAIN_LEFT(concrete_position=(2400↦1945),reward=16.882978723404257)
29MAIN_SYNCHRONIZE_BATTERY
30MAIN_UPDATE_POSITION
31MAIN_SYNCHRONIZE_BATTERY
32MAIN_OBSERVE
33MAIN_SYNCHRONIZE_BATTERY
34MAIN_BACKWARD(concrete_position=(2776↦1200),reward=13.421739130434782)
35MAIN_SYNCHRONIZE_BATTERY
36MAIN_UPDATE_POSITION
37MAIN_SYNCHRONIZE_BATTERY
38MAIN_OBSERVE
39MAIN_SYNCHRONIZE_BATTERY
40MAIN_BACKWARD(concrete_position=(2776↦1200),reward=15.966666666666667)
41MAIN_SYNCHRONIZE_BATTERY
42MAIN_UPDATE_POSITION
43MAIN_SYNCHRONIZE_BATTERY
44MAIN_OBSERVE
45MAIN_SYNCHRONIZE_BATTERY
Generated on 15/1/2026 at 17:06 using ProB version 1.15.1-final
Main specification file: ../DroneMainController.mch (modified on 15/1/2026 at 17:03)
Main specification name: DroneMainController
Main VisB JSON file: Drone_VisB_MAIN.def (modified on 15/1/2026 at 14:26)