PV can be used from the command line but is easiest to use from within the graphical user interface XPV01.

Once PV and XPV01 are installed try running the test script "test". This script runs a few small examples with a variety of parameters. If there is no trouble running this script then PV is installed and functioning as it should.

The PV distribution comes with several examples of various lengths. These examples take the form of Promela specifications. Promela was originally written by Gerard Holtzman as an input language for the model checker SPIN. Those who are unfamiliar with the language of promela can find out more about the constructs and semantics of this language, as well as the SPIN model checker at http://netlib.bell-labs.com/netlib/spin/whatispin.html.

PV's input language is a subset of Promela with a few additions and exceptions. Many similarly written protocols and specifications can be run on both SPIN and PV. Information on the language differences, including what is not included in the language of PV, and what extras you can find in PV can be found here.