The model of the Belt example in the paper “Modeling of Timing Constraints in Hybrid Systems Using Event-B” can be downloaded in this website.
In the Theory plugin of the Rodin platform, the operators are rewritten, such as summarize are rewritten as sum (x:”Real”, y:”Real”):”Real”. Therefore, complex functions of the systems are not easy to read. To simplify for readers, in this showing example, we write the basic operators of real numbers the same as the operators of Nature numbers in the Rodin platform.