Formal specification of Acumen's enclosure interpreter

Over the past weeks Jan, Walid and Michal have been writing down a formal specification of the algorithm underlying the Acumen enclosure interpreter. The specification includes a number of theorems formalizing the most important properties of the algorithm, such as definedness, safety and convergence. The main difficulty with formulating these theorems has been the lack of universally accepted definition for the trajectory for a hybrid system after its first Zeno point. The pragmatic approach taken was to use a commonly accepted definition for trajectories up the the first Zeno point and to restrict the theorems to such trajectories. For evolutions beyond the first Zeno point the output of the algorithm is taken to define the behavior of the system. The specification work has exposed a number of opportunities for vast performance improvements which will be the focus of Jan's coming work.