HelloWorld.md

The source code of this example is in file HelloWorld.pml. The following instructions use the command-line interface of the Spin model checker. One of the GUIs of Spin can be of course used.

Running the model

Assuming that Spin has been installed, the model can be run from the command-line with

spin HelloWorld.pml

this will run the model and print something like:

      Hi!
1 process created