Experiments

Experiments

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.

Some comments:

• Lines 1-3 shows that we need to refine the partition wrt. numerical constraints in order to prove the property.
• Lines 3-5 illustrates that more nondeterminism in the scheduler requires more partition refinement steps.
• We fail to show the property if Om=OM=0.9 (line 6).
• We then find a necessary condition, k<0.8, on the parameter k=Om=OM (line 7) for the property to hold.
• Lines 8-9 show the analysis without initial guided refinement: the results are comparable (line 8) or worse (line 9).

Experiments