The previous example uses two modules, M1 and M2, one representing each process.
A module is specified as:
The definition of a module contains two parts: its variables and its guards.
In this example, each module has one integer variable with range [0..2].
A variable declaration looks like:
Notice that the initial value of the variable is also specified. See the next subsection for more information about this subject. Boolean variables can also be used, e.g.:
The names given to modules and variables are referred to as identifiers.
Identifiers can be made up of letters, digits and the underscore character, but cannot begin with a digit,
i.e. they must satisfy the regular expression [A-Za-z_][A-Za-z0-9_]*, and are case-sensitive.
Furthermore, identifiers cannot be any of the following, which are all reserved keywords in PRISM:
bool, C, ceil, const, ctmc, double, dtmc, endinit, endmodule, endrewards, endsystem, F, false, floor, formula, G, global, I, init, int, label, max, mdp, min, module, nondeterministic, P, Pmin, Pmax, prob, probabilistic, R, rate, rewards, Rmin, Rmax, S, stochastic, system, true, U, X.
