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_arg1`|(`_freetype_arg1` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg1`) : FLOAT) & (`_freetype_arg1` : ran(JsonArray) => (JsonArray~)(`_freetype_arg1`) : seq(recursive.`2`)) & (`_freetype_arg1` : ran(JsonObject) => (JsonObject~)(`_freetype_arg1`) : STRING +-> recursive.`2`)}
2 JsonNull JsonNull
3 JsonBoolean /*@symbolic*/ {`_constr_arg3`,`_constr_res4`|`_constr_res4` = JsonBoolean(`_constr_arg3`)}
4 JsonNumber /*@symbolic*/ %`_constr_arg5`.(`_constr_arg5` : FLOAT|JsonNumber(`_constr_arg5`))
5 JsonString /*@symbolic*/ {`_constr_arg7`,`_constr_res8`|`_constr_res8` = JsonString(`_constr_arg7`)}
6 JsonArray /*@symbolic*/ %`_constr_arg9`.(`_constr_arg9` : seq(/*@symbolic*/ {`_freetype_arg1`|(`_freetype_arg1` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg1`) : FLOAT) & (`_freetype_arg1` : ran(JsonArray) => (JsonArray~)(`_freetype_arg1`) : seq(recursive.`2`)) & (`_freetype_arg1` : ran(JsonObject) => (JsonObject~)(`_freetype_arg1`) : STRING +-> recursive.`2`)})|JsonArray(`_constr_arg9`))
7 JsonObject /*@symbolic*/ %`_constr_arg11`.(`_constr_arg11` : STRING +-> /*@symbolic*/ {`_freetype_arg1`|(`_freetype_arg1` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg1`) : FLOAT) & (`_freetype_arg1` : ran(JsonArray) => (JsonArray~)(`_freetype_arg1`) : seq(recursive.`2`)) & (`_freetype_arg1` : ran(JsonObject) => (JsonObject~)(`_freetype_arg1`) : STRING +-> recursive.`2`)}|JsonObject(`_constr_arg11`))
8 RpcResult /*@symbolic*/ {`_freetype_arg13`|`_freetype_arg13` : ran(RpcSuccess) => (RpcSuccess~)(`_freetype_arg13`) : /*@symbolic*/ {`_freetype_arg1`|(`_freetype_arg1` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg1`) : FLOAT) & (`_freetype_arg1` : ran(JsonArray) => (JsonArray~)(`_freetype_arg1`) : seq(recursive.`2`)) & (`_freetype_arg1` : ran(JsonObject) => (JsonObject~)(`_freetype_arg1`) : STRING +-> recursive.`2`)}}
9 RpcSuccess /*@symbolic*/ %`_constr_arg15`.(`_constr_arg15` : /*@symbolic*/ {`_freetype_arg1`|(`_freetype_arg1` : ran(JsonNumber) => (JsonNumber~)(`_freetype_arg1`) : FLOAT) & (`_freetype_arg1` : ran(JsonArray) => (JsonArray~)(`_freetype_arg1`) : seq(recursive.`2`)) & (`_freetype_arg1` : ran(JsonObject) => (JsonObject~)(`_freetype_arg1`) : STRING +-> recursive.`2`)}|RpcSuccess(`_constr_arg15`))
10 RpcError /*@symbolic*/ {`_constr_arg17`,`_constr_res18`|`_constr_res18` = RpcError(`_constr_arg17`)}
11 BATTERY_STEP 2
12 WIDTH 5
13 DEPTH 5
14 BASE_POSITION (3|->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/5700B500FA"
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=(3↦2))State 1
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(1200↦600),current_position=(3↦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_BACKWARD(concrete_position=(1626↦600),reward=4.2)
11MAIN_SYNCHRONIZE_BATTERY
12MAIN_UPDATE_POSITION
13MAIN_SYNCHRONIZE_BATTERY
14MAIN_OBSERVE
15MAIN_SYNCHRONIZE_BATTERY
16MAIN_LEFT(concrete_position=(1800↦715),reward=6.43469387755102)
17MAIN_SYNCHRONIZE_BATTERY
18MAIN_UPDATE_POSITION
19MAIN_SYNCHRONIZE_BATTERY
20MAIN_OBSERVE
21MAIN_SYNCHRONIZE_BATTERY
22MAIN_FORWARD(concrete_position=(2085↦1200),reward=4.4875)
23MAIN_SYNCHRONIZE_BATTERY
24MAIN_UPDATE_POSITION
25MAIN_SYNCHRONIZE_BATTERY
26MAIN_OBSERVE
27MAIN_SYNCHRONIZE_BATTERY
28MAIN_LEFT(concrete_position=(2400↦1329),reward=5.5212765957446805)
29MAIN_SYNCHRONIZE_BATTERY
30MAIN_UPDATE_POSITION
31MAIN_SYNCHRONIZE_BATTERY
32MAIN_OBSERVE
33MAIN_SYNCHRONIZE_BATTERY
34MAIN_RIGHT(concrete_position=(1800↦1210),reward=-0.32608695652173914)
35MAIN_SYNCHRONIZE_BATTERY
36MAIN_UPDATE_POSITION
37MAIN_SYNCHRONIZE_BATTERY
38MAIN_OBSERVE
39MAIN_SYNCHRONIZE_BATTERY
40MAIN_BACKWARD(concrete_position=(2278↦600),reward=-0.5)
41MAIN_SYNCHRONIZE_BATTERY
42MAIN_UPDATE_POSITION
43MAIN_SYNCHRONIZE_BATTERY
44MAIN_OBSERVE
45MAIN_SYNCHRONIZE_BATTERY
46MAIN_BACKWARD(concrete_position=(2138↦0),reward=13.718181818181817)
47MAIN_SYNCHRONIZE_BATTERY
48MAIN_UPDATE_POSITION
49MAIN_SYNCHRONIZE_BATTERY
50MAIN_OBSERVE
51MAIN_SYNCHRONIZE_BATTERY
52MAIN_LEFT(concrete_position=(2400↦398),reward=15.927906976744186)
53MAIN_SYNCHRONIZE_BATTERY
54MAIN_UPDATE_POSITION
55MAIN_SYNCHRONIZE_BATTERY
56MAIN_OBSERVE
57MAIN_SYNCHRONIZE_BATTERY
58MAIN_RIGHT(concrete_position=(1800↦421),reward=-0.7142857142857142)
59MAIN_SYNCHRONIZE_BATTERY
60MAIN_UPDATE_POSITION
61MAIN_SYNCHRONIZE_BATTERY
62MAIN_OBSERVE
63MAIN_SYNCHRONIZE_BATTERY
64MAIN_RIGHT(concrete_position=(1800↦434),reward=9.051219512195122)
65MAIN_SYNCHRONIZE_BATTERY
66MAIN_UPDATE_POSITION
67MAIN_SYNCHRONIZE_BATTERY
68MAIN_OBSERVE
69MAIN_SYNCHRONIZE_BATTERY
70MAIN_FORWARD(concrete_position=(1625↦600),reward=-0.375)
71MAIN_SYNCHRONIZE_BATTERY
72MAIN_UPDATE_POSITION
73MAIN_SYNCHRONIZE_BATTERY
74MAIN_OBSERVE
75MAIN_SYNCHRONIZE_BATTERY
76MAIN_FORWARD(concrete_position=(1462↦1200),reward=-0.1923076923076923)
77MAIN_SYNCHRONIZE_BATTERY
78MAIN_UPDATE_POSITION
79MAIN_SYNCHRONIZE_BATTERY
80MAIN_OBSERVE
81MAIN_SYNCHRONIZE_BATTERY
82MAIN_LAND(reward=37.5)
Generated on 13/1/2026 at 17:13 using ProB version 1.15.1-final
Main specification file: ../DroneMainController.mch (modified on 13/1/2026 at 14:18)
Main specification name: MAIN_MACHINE_FOR_DroneMainController
Main VisB JSON file: ../visualization/Drone_VisB_MAIN.def (modified on 13/1/2026 at 10:33)