The previous example uses two modules, `M1`

and `M2`

, one representing each process.
A module is specified as:

module name ... endmodule

The definition of a module contains two parts: its *variables* and its *commands*.
The variables describe the possible states that the module can be in;
the commands describe its behaviour, i.e. the way in which the state changes over time.
Currently, PRISM supports just a few simple types of variables:
they can either be (finite ranges of) integers or Booleans
(we ignore clocks for now).

In the example above, each module has one integer variable with range `[0..2]`

.
A variable declaration looks like:

x : [0..2] init 0;

Notice that the initial value of the variable is also specified. A Boolean variable is declared as follows:

b : bool init false;

It is also possible to omit the initial value of a variable,
in which case it is assumed to be the lowest value in the range (or `false`

for a Boolean).
Thus, the variable declarations shown below are equivalent to the ones above.
As will be described later, it is also possible to specify
multiple initial states for a model.

x : [0..2];

b : bool;

b : bool;

We also mention that, for a few kinds of model analysis (typically those based on simulation, such as approximate model checking or fast adaptive simulation, it is also permissable to use integer variables with unbounded ranges, denoted as:

x : int;

y : int init 3;

y : int init 3;

Where the state space of the model remains finite, despite the presence of such unbounded variables, you can use the explicit engine to build and analyse the model.

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:

,
**A**

,
**bool**

,
**clock**

,
**const**

,
**ctmc**

,
**C**

,
**double**

,
**dtmc**

,
**E**

,
**endinit**

,
**endinvariant**

,
**endmodule**

,
**endobservables**

,
**endrewards**

,
**endsystem**

,
**false**

,
**formula**

,
**filter**

,
**func**

,
**F**

,
**global**

,
**G**

,
**init**

,
**invariant**

,
**I**

,
**int**

,
**label**

,
**max**

,
**mdp**

,
**min**

,
**module**

,
**X**

,
**nondeterministic**

,
**observable**

,
**observables**

,
**of**

,
**Pmax**

,
**Pmin**

,
**P**

,
**pomdp**

,
**popta**

,
**probabilistic**

,
**prob**

,
**pta**

,
**rate**

,
**rewards**

,
**Rmax**

,
**Rmin**

,
**R**

,
**S**

,
**stochastic**

,
**system**

,
**true**

,
**U**

.
**W**