Add specification and implementation of Hesselink's registers.

These models are checked in the equivalence checking case for a varying number of data elements.