Tools for modeling, simulation, control, and verification of piecewise affine systems