PromelaにはC言語のような関数は存在しません。その代わりとは行きませんが、よく似たものがあります。inline文です。inline文は関数ではありません！よく間違うので注意してください。あくまでマクロ定義です。inlineはコンパイル時に、inlineの中身そのままに書き換えられます。要するに、showHello(2);がprintf("%d\n",2);に置き換えられます。
　繰り返し同じコードを書くのは大変なので、inline文を使うと大変便利ですね。ただ、inline文の乱発はデバッグや可読性を非常に困難にします。気をつけてください。
　Promelaに関数がないのは、モデルを表現するのに不向きだからです。ただ、利便性を考えると関数のようなモノがほしいですが・・・。今後に期待しましょう。