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|->4)
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↦4))State 1
2INITIALISATION(battery=100,battery_actual=FALSE,concrete_position=(1200↦1800),current_position=(3↦4),current_time=0,cycl...
3MAIN_SYNCHRONIZE_BATTERY
4MAIN_TAKEOFF
5MAIN_SYNCHRONIZE_BATTERY
6MAIN_UPDATE_POSITION
7MAIN_SYNCHRONIZE_BATTERY
8MAIN_OBSERVE
9MAIN_SYNCHRONIZE_BATTERY
10MAIN_LEFT(concrete_position=(1800↦2240),reward=4.2)
11MAIN_SYNCHRONIZE_BATTERY
12MAIN_UPDATE_POSITION
13MAIN_SYNCHRONIZE_BATTERY
14MAIN_OBSERVE
15MAIN_SYNCHRONIZE_BATTERY
16MAIN_LEFT(concrete_position=(2400↦2284),reward=5.822448979591837)
17MAIN_SYNCHRONIZE_BATTERY
18MAIN_UPDATE_POSITION
19MAIN_SYNCHRONIZE_BATTERY
20MAIN_OBSERVE
21MAIN_SYNCHRONIZE_BATTERY
22MAIN_RIGHT(concrete_position=(1800↦2199),reward=-0.3125)
23MAIN_SYNCHRONIZE_BATTERY
24MAIN_UPDATE_POSITION
25MAIN_SYNCHRONIZE_BATTERY
26MAIN_OBSERVE
27MAIN_SYNCHRONIZE_BATTERY
28MAIN_LEFT(concrete_position=(2400↦2239),reward=0.0)
29MAIN_SYNCHRONIZE_BATTERY
30MAIN_UPDATE_POSITION
31MAIN_SYNCHRONIZE_BATTERY
32MAIN_OBSERVE
33MAIN_SYNCHRONIZE_BATTERY
34MAIN_RIGHT(concrete_position=(1800↦2239),reward=-0.32608695652173914)
35MAIN_SYNCHRONIZE_BATTERY
36MAIN_UPDATE_POSITION
37MAIN_SYNCHRONIZE_BATTERY
38MAIN_OBSERVE
39MAIN_SYNCHRONIZE_BATTERY
40MAIN_LEFT(concrete_position=(2400↦2202),reward=0.0)
41MAIN_SYNCHRONIZE_BATTERY
42MAIN_UPDATE_POSITION
43MAIN_SYNCHRONIZE_BATTERY
44MAIN_OBSERVE
45MAIN_SYNCHRONIZE_BATTERY
46MAIN_RIGHT(concrete_position=(1800↦2207),reward=-0.34090909090909094)
47MAIN_SYNCHRONIZE_BATTERY
48MAIN_UPDATE_POSITION
49MAIN_SYNCHRONIZE_BATTERY
50MAIN_OBSERVE
51MAIN_SYNCHRONIZE_BATTERY
52MAIN_LEFT(concrete_position=(2400↦2173),reward=0.0)
53MAIN_SYNCHRONIZE_BATTERY
54MAIN_UPDATE_POSITION
55MAIN_SYNCHRONIZE_BATTERY
56MAIN_OBSERVE
57MAIN_SYNCHRONIZE_BATTERY
58MAIN_RIGHT(concrete_position=(1800↦2210),reward=-0.3571428571428571)
59MAIN_SYNCHRONIZE_BATTERY
60MAIN_UPDATE_POSITION
61MAIN_SYNCHRONIZE_BATTERY
62MAIN_OBSERVE
63MAIN_SYNCHRONIZE_BATTERY
64MAIN_LEFT(concrete_position=(2400↦2157),reward=-0.9146341463414633)
65MAIN_SYNCHRONIZE_BATTERY
66MAIN_UPDATE_POSITION
67MAIN_SYNCHRONIZE_BATTERY
68MAIN_OBSERVE
69MAIN_SYNCHRONIZE_BATTERY
70MAIN_RIGHT(concrete_position=(1800↦2052),reward=-0.375)
71MAIN_SYNCHRONIZE_BATTERY
72MAIN_UPDATE_POSITION
73MAIN_SYNCHRONIZE_BATTERY
74MAIN_OBSERVE
75MAIN_SYNCHRONIZE_BATTERY
76MAIN_LEFT(concrete_position=(2400↦2117),reward=0.0)
77MAIN_SYNCHRONIZE_BATTERY
78MAIN_UPDATE_POSITION
79MAIN_SYNCHRONIZE_BATTERY
80MAIN_OBSERVE
81MAIN_SYNCHRONIZE_BATTERY
82MAIN_RIGHT(concrete_position=(1800↦2120),reward=-0.39473684210526316)
83MAIN_SYNCHRONIZE_BATTERY
84MAIN_UPDATE_POSITION
85MAIN_SYNCHRONIZE_BATTERY
86MAIN_OBSERVE
87MAIN_SYNCHRONIZE_BATTERY
88MAIN_LEFT(concrete_position=(2400↦2127),reward=0.0)
89MAIN_SYNCHRONIZE_BATTERY
90MAIN_UPDATE_POSITION
91MAIN_SYNCHRONIZE_BATTERY
92MAIN_OBSERVE
93MAIN_SYNCHRONIZE_BATTERY
94MAIN_RIGHT(concrete_position=(1800↦2127),reward=-0.41666666666666663)
95MAIN_SYNCHRONIZE_BATTERY
96MAIN_UPDATE_POSITION
97MAIN_SYNCHRONIZE_BATTERY
98MAIN_OBSERVE
99MAIN_SYNCHRONIZE_BATTERY
100MAIN_LEFT(concrete_position=(2400↦2082),reward=-1.0714285714285714)
101MAIN_SYNCHRONIZE_BATTERY
102MAIN_UPDATE_POSITION
103MAIN_SYNCHRONIZE_BATTERY
104MAIN_OBSERVE
105MAIN_SYNCHRONIZE_BATTERY
106MAIN_RIGHT(concrete_position=(1800↦2084),reward=-0.4411764705882353)
107MAIN_SYNCHRONIZE_BATTERY
108MAIN_UPDATE_POSITION
109MAIN_SYNCHRONIZE_BATTERY
110MAIN_OBSERVE
111MAIN_SYNCHRONIZE_BATTERY
112MAIN_RIGHT(concrete_position=(1200↦2087),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 16:49 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)