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:
All of the variables in the module being renamed (in this case, just x) must be renamed to new, unused names. Optionally, it is also possible to rename other aspects of the module definition. In fact, the renaming is done at a textual level, so any identifiers (including action labels, constants and functions) used in the module definition can be changed in this way.
Note: Care should be taken when renaming modules that make use of formulas.
Site hosted at the Department of Computer Science, University of Oxford