When PRISM crashes, the most likely cause is that it has run out of memory. Similarly, if PRISM (or the machine you are running it on) becomes very slow or seems to have stopped responding, this is probably because it is using too much of your machine's memory. Probabilistic model checking, much like other formal verification techniques, can be a very resource-intensive process. It is very easy to create a seemingly simple PRISM model that requires a large amount of time and/or memory to construct and analyse. See some of the other questions in this section for tips on how to avoid this.

The other possibility is that you have found a bug. If PRISM crashes or freezes whilst not using all/most of the available memory (you can check this with the top command in a Unix/Linux terminal or the Task Manager (via Ctrl-Alt-Delete) on Windows) then please file a bug report.

It depends. First, you need to establish at what point in PRISM's operation, you ran out of memory. If you are running the command-line version of PRISM then the output from the tool so far should give an indication of this. If using the GUI, check the log tab for this information. If PRISM crashed because of its memory usage, the error message can be helpful. If using the GUI, you may need to start the GUI from the command-line to see any error messages.

The two main steps that PRISM typically has to perform are:

1. Model construction (conversion of a PRISM language description to the corresponding probabilistic model)
2. Model checking/analysis (processing/analysis of a constructed probabilistic model in order to determine the result of a property or to compute steady-state/transient probabilities)

Memory usage issues for each of these steps are discussed in separate sections below. In some cases the process performed prior to step 1 (model parsing - reading in a model description in the PRISM language and checking it for correctness) can also be resource intensive. This is also discussed below.

If you are using the simulator to generate approximate model checking results then step 1 (model construction) is not performed and step 2 is carried out very differently. Memory consumption is not usually a problem in this case.

If PRISM has already output this:

but there is no line of the form:

and then you get an error like this:

or like this:

then PRISM ran out of memory whilst trying to construct the model. Model construction in PRISM is performed using BDDs (binary decision diagrams) and MTBDDs (multi-terminal) BDDs which are implemented in the CUDD library. The first thing to try in this case is to increase the amount of memory available to CUDD. See the entry "CUDD memory" in the section "Configuring PRISM - Other Options" for details of this.

If increasing this memory limit does not resolve the problem, then you will need to consider ways to reduce the size of your model. You can find some tips on this in the PRISM Modelling section. Bear in mind also that if you are having to increase the CUDD memory limit too high (e.g. close to the physical memory available on your computer) just for model construction, then it is unlikely that you will have enough memory for subsequent model checking operations.

Finally, it is also worth considering the ordering of the modules and variables in your model since this can have a (in some cases dramatic) effect on the size of MTBDD representation of the model. This topic is covered in the "PRISM Modelling" section of this FAQ.

If model construction was successfully completed (see previous question) but model checking was not, there are several things you can try. First of all, if the error message you see looks like the one in the previous question or you see a message such as

then it may be worth increasing the memory limit for CUDD (as described above). However, if you see an error more like this:

then increasing the memory CUDD probably will not help - PRISM is just trying to allocate more memory than is physically available on your system.

Here are some general tips:

• Try experimenting with using the different engines in PRISM. Read the section "Configuring PRISM - Computation Engines" for details.
• Look at the detailed output of PRISM for information about memory usage. If you are using the hybrid (or sparse) engine and the limiting factor in terms of memory is creation of the vectors, then you have no choice but to try and reduce the size (number of states) of your model. If you are using the MTBDD engine, it is also well worth considering the variable ordering of your model. Both topics are discussed in the "PRISM Modelling" section of this FAQ.
• Finally, if you can find no way to reduce the size of your model and are happy to consider an approximate (rather than exact) analysis, you may wish to try using PRISM's discrete-event simulation engine for analysis.

This is a less common problem and will only occur if the actual PRISM language description of your model is very large. This may be the case, for example, if you are automatically generating PRISM models in some way. Errors due to lack of memory during parsing usually look like:

or:

You can resolve this problem by increasing the memory allocated to Java. See the entry "Java memory" in the section "Configuring PRISM - Other Options" for details of this.

There is no definitive answer to this. Because of PRISM's symbolic implementation, using data structures based on binary decision diagrams (BDDs), its performance can be unpredictable in this respect. There are also several factors that affect performance, including the type of model and property being checked and the engine being used (PRISM has several different engines, which have varying performance).

Having said that, using the default engine in PRISM (the “hybrid” engine), you can normally expect to be able to handle models with up to 10^7-10^8 states on a typical PC. Using the MTBDD engine, you may be able to analyse much larger models (on some of the PRISM case studies, for example, PRISM can do numerical analysis of models with as many as 10^10 or 10^11 states). The manual has more information about PRISM's engines.

The size of a probabilistic model (i.e. the number of states/transitions) is critical to the efficiency of performing probabilistic model checking on it, since both the time and memory required to do so are often proportional to the model size. Unfortunately, it is very easy to create models that are extremely large. Below are a few general tips for reducing model size.

• Look for variables that have unnecessarily large ranges and try to reduce them. Even if your model needs large variables, it is generally a good strategy to first get a smaller version building successfully and then scale it up afterwards.
• Similarly, can you (if only temporarily) reduce the number of modules/components of your model? Start with the smallest number of components possible and then add others one by one.
• Do you have any inter-dependencies between variables? For example, perhaps you have some variables which are simply functions of other variables of the model. Even if these are convenient for model checking, they can be replaced with formulas or labels, which do not contribute to the state space.
• Do any variables include more detail than is necessary for the model? Perhaps this can be exploited in order to reduce the number of variables in your model.
• More generally, are any aspects of the model not relevant to the properties that you are interested in? If so, start with a simpler, more abstract version of the model and then add more details if possible.

Because PRISM is a symbolic model checker, the amount of memory required to store the probabilistic model can vary (sometime unpredictably) according to several factors. One example is the order in which the variables of your model appear in the model file. In general, there is no definitive answer to what the best ordering is but the following heuristics are a good guide.

• Variables which are closely related should appear close together
• Variables which are related to most or all other variables should appear near the start of the ordering

Variables x and y are "related" if, for example, the value of one is has an effect on how the other changes (e.g. (y'=x+1)) or if both appear together in an expression (e.g. a guard).

These heuristics also apply to the ordering of modules within the model file.

For technical details about variable ordering issues, see e.g. section 8 of [HKN+03] or section 4.1.2 of [Par02].

All delays in a CTMC need to be modelled as exponential distributions. This is what makes them efficient to analyse. If you included a transition whose delay was deterministic, i.e. which always occurred after exactly the same delay, the model would no longer be a CTMC.

One solution to this, if your model require such a delay, is to approximate a deterministic delay with an Erlang distribution (a special case of a phase-type distribution). See for example this PRISM model:

In the model, the occurrence of the the go-labelled action occurs with an Erlang distribution with mean mean and shape k. The special case of k=1 is just an exponential distribution. The graph below shows the probability distribution of the delay, i.e. of P=? [ F<=T x=1 ] for different values of k.

There is an obvious trade-off here between the accuracy (how close it is to modelling a deterministic time delay) and the resulting blow-up in the size of the model that you add this to. For k=1000, you can see that the shape is quite "deterministic" but this would increase your model size by a factor of ~1000.