We ran nbacg.opt with the option file .nbacrc:

nbacg.opt -rc .nbacrc -print "+p +r" lecteur.ba

The global model has 10 Boolean state variables (or equivalently for enumerated variables), 1 integer and 2 real state variables.

The initial control structure is the control structure of process X (scheduler). We then ask (with the control statement) to distinguish the mode of the disk motor. This is the "guided refinement" step. Then further refinement is performed by our standard heuristics.

We choosed EPS=0.8, M=N=2, and we tried different options for the constants DIM, DOm, and DOM. We remind that the goal of the controller is to maintain the speed in the interval [8,12], and the physical speed may be outside of this range for at most 7 cycles. A cycle is one time unit.

Meaning of columns
Partition Size of the final partition, in nb of locations/nb of transitions
Refinements Number of heuristic refinement steps/location divisions

Some comments: