View - Edit - Print - Search

The PRISM Language /

Modules And Variables

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 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:

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

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.

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:

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.

Identifiers

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.