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.
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
, endrewards
, endsystem
, false
, formula
, filter
, func
, F
, global
, G
, init
, invariant
, I
, int
, label
, max
, mdp
, min
, module
, X
, nondeterministic
, Pmax
, Pmin
, P
, probabilistic
, prob
, pta
, rate
, rewards
, Rmax
, Rmin
, R
, S
, stochastic
, system
, true
, U
, W
.