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.

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:

- 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
(line 6).*Om=OM=0.9* - 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 |