PRISM also supports module renaming, which allows duplication of modules.
In Example 1, module M2 is identical to module M1 so we can in fact replace its entire definition with:
Note that this renaming is done at a textual level, so any identifiers (including action labels)
used in the module definition can be changed in this way.
All of the variables in the module being renamed (in this case, just x) must be renamed to new, unused names.
