 Consider a module \(S\) with four channels labeled \(a_\textrm{in},a_\textrm{out},r_\textrm{in},r_\textrm{out}\). The module is intended to return on channel \(a_\textrm{out}\) the successor of the number \(n\) incoming through channel \(a_\textrm{in}\), therefore its behavior can be specified as follows: