Automaton-/Location-local registers

[mtf90]

According to the formal definition, the set of registers are specific to a location. However, the current implementation seems to dynamically determine the registers based on the assignments of the incoming transitions of a location. Should the management of registers be more rigorous in the sense that they are not computed on-the-fly but explicitly defined when constructing a RegisterAutomaton (e.g., via a distinct addRegister method)? This would allow for more consistency checks such as checking whether new transitions only reference existing registers in their assignments, etc.