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_RIGHT(concrete_position=(600↦1204),reward=6.6)
11MAIN_SYNCHRONIZE_BATTERY
12MAIN_UPDATE_POSITION
13MAIN_SYNCHRONIZE_BATTERY
14MAIN_OBSERVE
15MAIN_SYNCHRONIZE_BATTERY
16MAIN_BACKWARD(concrete_position=(1001↦600),reward=6.43469387755102)
17MAIN_SYNCHRONIZE_BATTERY
18MAIN_UPDATE_POSITION
19MAIN_SYNCHRONIZE_BATTERY
20MAIN_OBSERVE
21MAIN_SYNCHRONIZE_BATTERY
22MAIN_BACKWARD(concrete_position=(913↦0),reward=13.462499999999999)
23MAIN_SYNCHRONIZE_BATTERY
24MAIN_UPDATE_POSITION
25MAIN_SYNCHRONIZE_BATTERY
26MAIN_OBSERVE
27MAIN_SYNCHRONIZE_BATTERY
28MAIN_FORWARD(concrete_position=(1007↦600),reward=-0.4787234042553191)
29MAIN_SYNCHRONIZE_BATTERY
30MAIN_UPDATE_POSITION
31MAIN_SYNCHRONIZE_BATTERY
32MAIN_OBSERVE
33MAIN_SYNCHRONIZE_BATTERY
34MAIN_FORWARD(concrete_position=(848↦1200),reward=-0.32608695652173914)
35MAIN_SYNCHRONIZE_BATTERY
36MAIN_UPDATE_POSITION
37MAIN_SYNCHRONIZE_BATTERY
38MAIN_OBSERVE
39MAIN_SYNCHRONIZE_BATTERY
40MAIN_FORWARD(concrete_position=(866↦1800),reward=5.5)
41MAIN_SYNCHRONIZE_BATTERY
42MAIN_UPDATE_POSITION
43MAIN_SYNCHRONIZE_BATTERY
44MAIN_OBSERVE
45MAIN_SYNCHRONIZE_BATTERY
46MAIN_RIGHT(concrete_position=(0↦2078),reward=6.518181818181818)
47MAIN_SYNCHRONIZE_BATTERY
48MAIN_UPDATE_POSITION
49MAIN_SYNCHRONIZE_BATTERY
50MAIN_OBSERVE
51MAIN_SYNCHRONIZE_BATTERY
52MAIN_LEFT(concrete_position=(600↦2066),reward=-0.5232558139534884)
53MAIN_SYNCHRONIZE_BATTERY
54MAIN_UPDATE_POSITION
55MAIN_SYNCHRONIZE_BATTERY
56MAIN_OBSERVE
57MAIN_SYNCHRONIZE_BATTERY
58MAIN_BACKWARD(concrete_position=(777↦1200),reward=-0.3571428571428571)
59MAIN_SYNCHRONIZE_BATTERY
60MAIN_UPDATE_POSITION
61MAIN_SYNCHRONIZE_BATTERY
62MAIN_OBSERVE
63MAIN_SYNCHRONIZE_BATTERY
64MAIN_BACKWARD(concrete_position=(823↦600),reward=-0.548780487804878)
65MAIN_SYNCHRONIZE_BATTERY
66MAIN_UPDATE_POSITION
67MAIN_SYNCHRONIZE_BATTERY
68MAIN_OBSERVE
69MAIN_SYNCHRONIZE_BATTERY
70MAIN_FORWARD(concrete_position=(690↦1200),reward=-0.375)
71MAIN_SYNCHRONIZE_BATTERY
72MAIN_UPDATE_POSITION
73MAIN_SYNCHRONIZE_BATTERY
74MAIN_OBSERVE
75MAIN_SYNCHRONIZE_BATTERY
76MAIN_BACKWARD(concrete_position=(766↦600),reward=-0.576923076923077)
77MAIN_SYNCHRONIZE_BATTERY
78MAIN_UPDATE_POSITION
79MAIN_SYNCHRONIZE_BATTERY
80MAIN_OBSERVE
81MAIN_SYNCHRONIZE_BATTERY
82MAIN_FORWARD(concrete_position=(809↦1200),reward=-0.39473684210526316)
83MAIN_SYNCHRONIZE_BATTERY
84MAIN_UPDATE_POSITION
85MAIN_SYNCHRONIZE_BATTERY
86MAIN_OBSERVE
87MAIN_SYNCHRONIZE_BATTERY
88MAIN_BACKWARD(concrete_position=(722↦600),reward=-0.6081081081081081)
89MAIN_SYNCHRONIZE_BATTERY
90MAIN_UPDATE_POSITION
91MAIN_SYNCHRONIZE_BATTERY
92MAIN_OBSERVE
93MAIN_SYNCHRONIZE_BATTERY
94MAIN_LEFT(concrete_position=(1200↦982),reward=-0.41666666666666663)
95MAIN_SYNCHRONIZE_BATTERY
96MAIN_UPDATE_POSITION
97MAIN_SYNCHRONIZE_BATTERY
98MAIN_OBSERVE
99MAIN_SYNCHRONIZE_BATTERY
100MAIN_FORWARD(concrete_position=(1351↦1200),reward=-0.21428571428571427)
101MAIN_SYNCHRONIZE_BATTERY
102MAIN_UPDATE_POSITION
103MAIN_SYNCHRONIZE_BATTERY
104MAIN_OBSERVE
105MAIN_SYNCHRONIZE_BATTERY
106MAIN_LAND(reward=37.5)
Generated on 13/1/2026 at 17:03 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)