www.prismmodelchecker.org

The PRISM Language /

PRISM Model Files

Files containing model descriptions written in the PRISM language can contain any amount of white space (spaces, tabs, new lines, etc.), all of which is ignored when the file is parsed by the tool. Comments can also be used included in files in the style of the C programming language, by preceding them with the characters //. This is illustrated by the PRISM language examples from earlier in this section.

By convention, the file extensions used for PRISM model files vary according to the model type:

  • .nm (for MDPs or PTAs)
  • .pm (for DTMCs)
  • .sm (for CTMCs)

but, since new models are added over time, we now recommend that you use:

  • .prism (for any model type)

PRISM Manual

The PRISM Language

[ View all ]