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 (4|->1)
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=(4↦1))State 1
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(1800↦0),current_position=(4↦1),current_time=0,cycle=1...
3MAIN_SYNCHRONIZE_BATTERY
4MAIN_TAKEOFF
5MAIN_SYNCHRONIZE_BATTERY
6MAIN_UPDATE_POSITION
7MAIN_SYNCHRONIZE_BATTERY
8MAIN_OBSERVE
9MAIN_SYNCHRONIZE_BATTERY
10MAIN_BACKWARD(concrete_position=(2232↦0),reward=4.2)
11MAIN_SYNCHRONIZE_BATTERY
12MAIN_UPDATE_POSITION
13MAIN_SYNCHRONIZE_BATTERY
14MAIN_OBSERVE
15MAIN_SYNCHRONIZE_BATTERY
16MAIN_LEFT(concrete_position=(2400↦387),reward=6.740816326530611)
17MAIN_SYNCHRONIZE_BATTERY
18MAIN_UPDATE_POSITION
19MAIN_SYNCHRONIZE_BATTERY
20MAIN_OBSERVE
21MAIN_SYNCHRONIZE_BATTERY
22MAIN_FORWARD(concrete_position=(2905↦600),reward=4.4875)
23MAIN_SYNCHRONIZE_BATTERY
24MAIN_UPDATE_POSITION
25MAIN_SYNCHRONIZE_BATTERY
26MAIN_OBSERVE
27MAIN_SYNCHRONIZE_BATTERY
28MAIN_BACKWARD(concrete_position=(2879↦0),reward=-0.4787234042553191)
29MAIN_SYNCHRONIZE_BATTERY
30MAIN_UPDATE_POSITION
31MAIN_SYNCHRONIZE_BATTERY
32MAIN_OBSERVE
33MAIN_SYNCHRONIZE_BATTERY
34MAIN_FORWARD(concrete_position=(2911↦600),reward=-0.32608695652173914)
35MAIN_SYNCHRONIZE_BATTERY
36MAIN_UPDATE_POSITION
37MAIN_SYNCHRONIZE_BATTERY
38MAIN_OBSERVE
39MAIN_SYNCHRONIZE_BATTERY
40MAIN_BACKWARD(concrete_position=(2856↦0),reward=-0.5)
41MAIN_SYNCHRONIZE_BATTERY
42MAIN_UPDATE_POSITION
43MAIN_SYNCHRONIZE_BATTERY
44MAIN_OBSERVE
45MAIN_SYNCHRONIZE_BATTERY
46MAIN_RIGHT(concrete_position=(1800↦446),reward=-0.34090909090909094)
47MAIN_SYNCHRONIZE_BATTERY
48MAIN_UPDATE_POSITION
49MAIN_SYNCHRONIZE_BATTERY
50MAIN_OBSERVE
51MAIN_SYNCHRONIZE_BATTERY
52MAIN_LEFT(concrete_position=(2400↦545),reward=-0.5232558139534884)
53MAIN_SYNCHRONIZE_BATTERY
54MAIN_UPDATE_POSITION
55MAIN_SYNCHRONIZE_BATTERY
56MAIN_OBSERVE
57MAIN_SYNCHRONIZE_BATTERY
58MAIN_RIGHT(concrete_position=(1800↦554),reward=-0.3571428571428571)
59MAIN_SYNCHRONIZE_BATTERY
60MAIN_UPDATE_POSITION
61MAIN_SYNCHRONIZE_BATTERY
62MAIN_OBSERVE
63MAIN_SYNCHRONIZE_BATTERY
64MAIN_LEFT(concrete_position=(2400↦579),reward=-0.548780487804878)
65MAIN_SYNCHRONIZE_BATTERY
66MAIN_UPDATE_POSITION
67MAIN_SYNCHRONIZE_BATTERY
68MAIN_OBSERVE
69MAIN_SYNCHRONIZE_BATTERY
70MAIN_RIGHT(concrete_position=(1800↦595),reward=-0.375)
71MAIN_SYNCHRONIZE_BATTERY
72MAIN_UPDATE_POSITION
73MAIN_SYNCHRONIZE_BATTERY
74MAIN_OBSERVE
75MAIN_SYNCHRONIZE_BATTERY
76MAIN_LEFT(concrete_position=(2400↦526),reward=-0.576923076923077)
77MAIN_SYNCHRONIZE_BATTERY
78MAIN_UPDATE_POSITION
79MAIN_SYNCHRONIZE_BATTERY
80MAIN_OBSERVE
81MAIN_SYNCHRONIZE_BATTERY
82MAIN_RIGHT(concrete_position=(1800↦531),reward=-0.39473684210526316)
83MAIN_SYNCHRONIZE_BATTERY
84MAIN_UPDATE_POSITION
85MAIN_SYNCHRONIZE_BATTERY
86MAIN_OBSERVE
87MAIN_SYNCHRONIZE_BATTERY
88MAIN_LEFT(concrete_position=(2400↦546),reward=-0.6081081081081081)
89MAIN_SYNCHRONIZE_BATTERY
90MAIN_UPDATE_POSITION
91MAIN_SYNCHRONIZE_BATTERY
92MAIN_OBSERVE
93MAIN_SYNCHRONIZE_BATTERY
94MAIN_RIGHT(concrete_position=(1800↦549),reward=-0.41666666666666663)
95MAIN_SYNCHRONIZE_BATTERY
96MAIN_UPDATE_POSITION
97MAIN_SYNCHRONIZE_BATTERY
98MAIN_OBSERVE
99MAIN_SYNCHRONIZE_BATTERY
100MAIN_LEFT(concrete_position=(2400↦574),reward=-0.6428571428571429)
101MAIN_SYNCHRONIZE_BATTERY
102MAIN_UPDATE_POSITION
103MAIN_SYNCHRONIZE_BATTERY
104MAIN_OBSERVE
105MAIN_SYNCHRONIZE_BATTERY
106MAIN_RIGHT(concrete_position=(1800↦569),reward=-0.4411764705882353)
107MAIN_SYNCHRONIZE_BATTERY
108MAIN_UPDATE_POSITION
109MAIN_SYNCHRONIZE_BATTERY
110MAIN_OBSERVE
111MAIN_SYNCHRONIZE_BATTERY
112MAIN_FORWARD(concrete_position=(2317↦600),reward=-0.2272727272727273)
113MAIN_SYNCHRONIZE_BATTERY
114MAIN_UPDATE_POSITION
115MAIN_SYNCHRONIZE_BATTERY
116MAIN_OBSERVE
117MAIN_SYNCHRONIZE_BATTERY
118MAIN_LAND(reward=37.5)
Generated on 13/1/2026 at 14:31 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)