The vending machine example in Section 5.1 was presented in a modular way, by separating the underlying signature defining the states of the machine from the rules defining the corresponding transitions.
mod VENDING-MACHINE is
including VENDING-MACHINE-SIGNATURE .
var M : Marking .
rl [add-q] : M => M q .
...
endm
It is important to notice that in this example the importation mode cannot be either protecting or extending, because those modes require preservation of the reachability relation, which clearly is not the case when adding (non-identity) rewrite rules to a functional module (where the reachability relation is the identity).