The start state of the model, *stopped,* **describes the corresponding initial state of the hybrid** 
automaton, i.e., fixes the initial conditions of the rover. Then, the *start* **rule initiates the rover** movement by setting the *running* **variable to true.** 
The other five model rules, namely accelerate, decelerate, *running, braking* and *cooling***, model** 
the main transitions and states of the automaton. In particular, *accelerate* and *decelerate* **update** 
the acceleration variable as described by the corresponding automaton transitions. These rules have a null duration and weight, according to the hybrid automaton semantics, since they represent instantaneous updates. On the other hand, the *running, braking* and *cooling* rules have *duration* **1, since they model the** 
changes in the rover state (i.e., speed, distance and battery charge) during a time step of one second. Such updates are actually performed by the running_*status_update,* braking_*status_update* and cooling_*status_update* **procedures, respectively, which concentrate** the update logic found in the entire automaton, i.e., the updates specified on the *maxDistance*, 
arrest and *restart* transitions and the ones contained in the *running* and *cooling* **states. The** 
status update procedures, in turn, compute some values through external C functions (e.g., update_c_cooling**) that are used to evaluate the complex expressions described in Section 4.1.** 
Moreover, the external functions *cost_moving* and *cost_cooling* **are used to dynamically** calculate the *weight* **of each rule, as defined by the cost function shown in Section 4.2.** The invariants *engineExplode* and *energyEnd* **model the homonymous transitions that lead, in** 
the automaton, to error states (*engineBlown* and *noenergy***, respectively). These states are not** 
modelled here, since the planner automatically detects as errors all the states that violate an invariant. 

Finally, the *goal* **construct is used to declare the success condition of the model, i.e., when the** 
rover completes successfully its journey. 

## 4.4. **Planning**

To build the optimal plan, the model was given in input to UPMurphi. Initially, we set H/1AoC1D  HC1D**, to see if we can devise a safe plan without imposing more restrictive** 
constraints on the rover speed. The exploration of the model dynamics lead to 939,477 reachable states, which is considerably smaller than the theoretical system state space of 2.2 p 10!Z **states. Thanks to such state space pruning, due to the reachability analysis performed** 
by the model checking algorithms of UPMurphi, finding an optimal (w.r.t. the cost function) 
plan required a relatively small amount of resources, with a peak memory allocation of 500 MB, 
and 2,257 seconds of processing. 

The resulting plan is described in Table 2. The table reports, for each second (which is the plan sampling time, as discussed earlier) the model rule (with respect to the code in Figure 2) chosen by UPMurphi. Thus, the rover starts its journey when *Start* is selected, moves when *Running* **is** selected, brakes when *Braking* is selected, increases or decreases its speed when *Accelerate* **or** 
Decelerate are selected, respectively, and performs a *Cooling* **when the homonymous rule is** 
chosen. Note that we may have more than one rule executed in a single time step, since some of them (namely, Start, *Accelerate* and *Decelerate)* have **duration zero.** 
Table 3 summarises the plan statistics. It is worth noting that the plan optimisation allowed us to save 922.7 C with respect to the required minimal battery charge, and 17 seconds with respect to the maximum allowed plan duration. 