@ -293,12 +313,12 @@ To clarify terminology: each <em>state</em> of the MDP contains (nondeterministi
<pclass='vspace'>For the <aclass='urllink'href='../uploads/lec3.pm'>lec3.pm</a> (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):
@ -310,25 +330,25 @@ except that probabilities/rates are replaced with reward values, and the number
<pclass='vspace'>For the <aclass='urllink'href='../uploads/lec3.pm'>lec3.pm</a> (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:
<pclass='vspace'>And or the <aclass='urllink'href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
@ -296,12 +316,12 @@ To clarify terminology: each <em>state</em> of the MDP contains (nondeterministi
<pclass='vspace'>For the <aclass='urllink'href='../uploads/lec3.pm'>lec3.pm</a> (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):
@ -313,25 +333,25 @@ except that probabilities/rates are replaced with reward values, and the number
<pclass='vspace'>For the <aclass='urllink'href='../uploads/lec3.pm'>lec3.pm</a> (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:
<pclass='vspace'>And or the <aclass='urllink'href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
@ -230,6 +230,12 @@ Performance (time and space), however, may vary significantly and if you are usi
<pclass='vspace'>Note also that precise details regarding the memory usage of the current engine are displayed during model checking (from the GUI, check the "Log" tab). This can provide valuable feedback when experimenting with different engines.
</p>
<pclass='vspace'>PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically,
based on the size and type of the model, and the property being checked.
Use, for example, <code>-heuristic speed</code> from the command-line to choose options
which target computation speed rather than saving memory.
This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI.
</p>
<divclass='vspace'></div><h3>Approximate/statistical model checking</h3>
<p>Although it is not treated as a separate "engine", like those above,
PRISM also provides approximate/statistical model checking,
@ -149,6 +149,12 @@ Performance (time and space), however, may vary significantly and if you are usi
<pclass='vspace'>Note also that precise details regarding the memory usage of the current engine are displayed during model checking (from the GUI, check the "Log" tab). This can provide valuable feedback when experimenting with different engines.
</p>
<pclass='vspace'>PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically,
based on the size and type of the model, and the property being checked.
Use, for example, <code>-heuristic speed</code> from the command-line to choose options
which target computation speed rather than saving memory.
This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI.
</p>
<divclass='vspace'></div><h3>Approximate/statistical model checking</h3>
<p>Although it is not treated as a separate "engine", like those above,
PRISM also provides approximate/statistical model checking,
This document is the main source of information regarding the installation and operation of the PRISM tool. For access to other resources, such as <aclass='urllink'href='http://www.prismmodelchecker.org/publications.php'>related publications</a> and details of <aclass='urllink'href='http://www.prismmodelchecker.org/casestudies/'>case studies</a>, or to <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>download</a> the tool itself, see the main <aclass='urllink'href='http://www.prismmodelchecker.org/'>PRISM website</a>.
</p>
<divclass='vspace'></div><h3>Which version of PRISM does this manual describe?</h3>
<p>This manual describes version <strong>4.5</strong>.
<p>This manual describes version <strong>4.6</strong>.
In general, the online copy of the manual corresponds to the most recent
<pclass='vspace'>This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
<pclass='vspace'>This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
(e.g. <code>x<=5</code> is allowed, <code>x<5</code> is not).
</p>
<pclass='vspace'>The digital clocks also has support for rewards:
<pclass='vspace'>This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
<pclass='vspace'>This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
(e.g. <code>x<=5</code> is allowed, <code>x<5</code> is not).
</p>
<pclass='vspace'>The digital clocks also has support for rewards:
<p>Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the <code>examples</code> directory of the distribution.
<p>Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the <code>prism-examples</code> directory of the distribution.
A few very small models are contained in the subdirectory <code>simple</code>;
the rest are in subdirectories grouped by model type.
</p>
<pclass='vspace'>The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error mIessage will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.
</p>
@ -695,7 +697,7 @@ You can optionally request that state descriptions are added to each state of gr
<p>Typically, once a model has been constructed, it is analysed through model checking.
Properties are specified as described in the "<aclass='wikilink'href='../PropertySpecification/Main.html'>Property Specification</a>" section,
and are usually kept in files with extensions <code>.props</code>, <code>.pctl</code> or <code>.csl</code>.
There are properties files accompanying most of the sample PRISM models in the <code>examples</code> directory.
There are properties files accompanying most of the sample PRISM models in the <code>prism-examples</code> directory.
</p>
<pclass='vspace'>
</p><h3>GUI</h3>
@ -749,15 +751,25 @@ For example, to check only the fourth property in the file:
<pclass='vspace'>The switches <code>-pctl</code> and <code>-csl</code> are aliases for <code>-pf</code>.
</p>
<pclass='vspace'>Note the use of single quotes (<code>'...'</code>) to avoid characters such as
@ -845,10 +857,10 @@ If, for a given property, statistical model checking results in one or more path
<p>Statistical model checking can also be enabled from the command-line version of PRISM, by including the <code>-sim</code> switch. The default methods used are CI (Confidence Interval) for "quantitative" properties and SPRT (Sequential Probability Ratio Test) for "bounded" properties. To select a particular method, use switch <code>-simmethod <method></code> where <code><method></code> is one of <code>ci</code>, <code>aci</code>, <code>apmc</code> and <code>sprt</code>. For example:
<pclass='vspace'>PRISM has default values for the various simulation method parameters, but these can also be specified using the switches <code>-simsamples</code>, <code>-simconf</code>, <code>-simwidth</code> and <code>-simapprox</code>. The exact meaning of these switches for each simulation method is given in the table below.
@ -877,19 +889,19 @@ time value for which you wish to compute probabilities.
From the command-line, add the <code>-steadystate</code> (or <code>-ss</code>) switch:
<pclass='vspace'>for transient probabilities, again specifying a time value in the latter case.
@ -899,11 +911,11 @@ either on the screen (from the command-line) or in the log (from the GUI).
<pclass='vspace'>To instead export the vector of computed probabilities to a file, use the "Model | Compute/export" option from the GUI, or the <code>-exportsteadystate</code> (or <code>-exportss</code>) and <code>-exporttransient</code> (or <code>-exporttr</code>) switches from the command-line:
<pclass='vspace'>From the command-line, you can request that the probability vectors exported are in Matlab format by adding the <code>-exportmatlab</code> switch.
@ -915,30 +927,30 @@ an equiprobable choice over the set of initial states.
You can override this and provide a specific initial distribution. This is done using the <code>-importinitdist</code> switch. The format for this imported distribution is identical to the ones exported by PRISM, i.e. simply a list of probabilities for all states separated by new lines. For example, this:
<pclass='vspace'>which computes transient probabilities for the time points 0.1, 0.11, 0.12, .., 0.2. In this case, the computation is done incrementally, with probabilities for each time point being computed from the previous point for efficiency.
@ -948,30 +960,30 @@ You can override this and provide a specific initial distribution. This is done
This is done by leaving one or more <aclass='wikilink'href='../ThePRISMLanguage/Constants.html'>constants</a> undefined, e.g.:
<pclass='vspace'>This can be done for constants in the model file, the properties file, or both.
Before any verification can be performed, values must be provided for any such constants. In the GUI, a dialog appears in which the user is required to enter values. From the command line, the <code>-const</code> switch must be used, e.g.:
<pclass='vspace'>To run an experiment, provide a <em>range</em> of values for one or more of the constants. Model checking will be performed for all combinations of the constant values provided. For example:
<pclass='vspace'>From the GUI, the same thing can be achieved by selecting a single property,
@ -1018,19 +1030,19 @@ or as code which can be used to generate the graph in Matlab.
<p>You can export all the results from an experiment to a file or to the screen. From the command-line, use the <code>-exportresults</code> switch, for example:
<pclass='vspace'>to send the results straight to the screen. From the GUI, right click on the experiment and select "Export results".
@ -1038,7 +1050,7 @@ or as code which can be used to generate the graph in Matlab.
<pclass='vspace'>The default behaviour is to export a <em>list</em> of results in <em>text</em> form, using tabs to separate items. The above examples produce:
</p>
<divclass='vspace'></div>
<divclass='sourceblock 'id='sourceblock44'>
<divclass='sourceblock 'id='sourceblock45'>
<divclass='sourceblocktext'><divclass="text">N T Result<br/>
<pclass='vspace'>You can change the format in which the results are exported by appending one or more comma-separated options to the end of the <code>-exportresults</code> switch, for example to export in CSV (comma-separated values) format:
<pclass='vspace'>A related option is the <code>-exportvector <file></code> switch, useful in general contexts, not for experiments.
This exports the results for all states of the model
(typically, the log just displays the result for the initial state, unless a <aclass='wikilink'href='../PropertySpecification/Filters.html'>filter</a> has been used)
to the the file <code>file</code>.
</p><hr/>
<h1>Adversaries</h1>
<p>When model checking some properties of MDPs, PRISM can also generate an <em>optimal adversary</em>, i.e. one which corresponds to either the minimum or maximum values of the probabilities or rewards computed during verification. Recall that, for MDPs, PRISM quantifies over all possible adversaries, i.e. all possible resolutions of nondeterminism in the model. A typical property would be:
<pclass='vspace'>which computes the maximum probability, over all adversaries, of reaching a state satisfying the label <code>"error"</code>, from all states of the model. When under the control of a specific adversary, the behaviour of an MDP is purely probabilistic, yielding a single value (for each state) for the probability of reaching <code>"error"</code>. In addition to giving the maximum probability value(s), PRISM can produce an adversary of the MDP for which the probabilities (for each state) coincide with the maximum values.
@ -1130,10 +1146,10 @@ This is particularly useful if you want to create a surface plot from results th
<pclass='vspace'>Currently, adversary generation is only implemented in the <aclass='wikilink'href='../ConfiguringPRISM/ComputationEngines.html'>sparse engine</a>, so you need to make sure this engine is enabled. From the command-line, you specify that an optimal adversary should be generated using the <code>-exportadv</code> switch, e.g.:
<pclass='vspace'>From the GUI, change the "Adversary export" option (under the "PRISM" settings) from "None" to "DTMC". You can also change the filename for the export adversary which, by default, is <code>adv.tra</code> as in the example above.
@ -1158,7 +1174,7 @@ Secondly, each local state of a sequential component must be named. For exampl
definition of these differs from the PEPA definition. Every PEPA
synchronisation must have exactly one active component.
Some examples of PEPA model descriptions which can be imported into PRISM
can be found in the <code>examples/pepa</code> directory.
can be found in the <code>prism-examples/pepa</code> directory.
</p>
<pclass='vspace'>From the command-line version of PRISM, add the <code>-importpepa</code> switch and the model will be treated as a PEPA description.
From the GUI, select "Model | Open model" and then choose "PEPA models"
@ -1180,7 +1196,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
<p>An SBML file comprises a set of <em>species</em> and a set of <em>reactions</em> which they undergo. Below is the SBML file for the simple reversible reaction: <strong>Na + Cl ↔ Na<sup>+</sup> + Cl<sup>-</sup></strong>, where there are initially 100 Na and Cl atoms and no ions, and the base rates for the forwards and backwards reactions are 100 and 10, respectively.
<pclass='vspace'>From the latter, we can use PRISM to generate a simple plot of the expected amount of Na and Na+ over time (using both model checking and a single random trace from the simulator):
@ -1344,11 +1360,11 @@ by selecting menu option "Model | View | Parsed PRISM model".
<p>At present, the SBML-to-PRISM translator is included in the PRISM code-base, but not integrated into the application itself.
<pclass='vspace'>If you are using a binary (rather than source code) distribution of PRISM, replace <code>classes</code> with <code>lib/prism.jar</code> in the above.
@ -1356,7 +1372,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
<pclass='vspace'>Alternatively (on Linux or Mac OS X), ensure <code>prism</code> is in your path and then save the script below as an executable file called <code>sbml2prism</code>:
<pclass='vspace'>This contains a single property which, based on the reward structures in the PRISM model generated by the translator, means "the expected amount of species <em>c</em> at time <em>T</em>". The constant <em>c</em> is an integer index which can range between 1 and <em>N</em>, where <em>N</em> is the number of species in the model. To view the expected amount of each species over time, create an <aclass='wikilink'href='Experiments.html'>experiment</a> in PRISM which varies <em>c</em> from 1 to <em>N</em> and <em>T</em> over the desired time range.
<pclass='vspace'>Furthermore, since PRISM is primarily a model checking (rather than simulation) tool, it is important that the amount of each species also has an upper bound (to ensure a finite state space). When model checking, the efficiency (or even feasibility) of the process is likely to be very sensitive to the upper bound(s) chosen. When using the discrete-event simulation functionality of PRISM, this is not the case and the bounds can can be set much higher. By default the translator uses an upper bound of 100 (which is increased if the initial amount exceeds this). A different value can specified through a second command-line argument as follows:
The format in which this information is input to the tool is exactly the same as is currently output
(see the section "<aclass='wikilink'href='ExportingTheModel.html'>Exporting The Model</a>" and the appendix "<aclass='wikilink'href='../Appendices/ExplicitModelFiles.html'>Explicit Model Files</a>").
Presently, this functionality is only supported in the command-line version of the tool, using the <code>-importtrans</code> switch (and more convenient <code>-importmodel</code>; see below).
At the moment, PRISM makes no attempt to discern the model type from the input file.
By default it assumes that the model is an MDP.
If this is not the case, the model type can be overwritten using the <code>-dtmc</code>, <code>-ctmc</code> and <code>-mdp</code> switches.
PRISM makes some attempt to discern the model type from the format of the input files,
but if this does not work, the model type can be overwritten using the <code>-dtmc</code>, <code>-ctmc</code> and <code>-mdp</code> switches.
<pclass='vspace'>where the labels file (<code>poll2.lab</code> above) is in the format generated by the <code>-exportlabels</code><aclass='wikilink'href='ExportingTheModel.html'>export option</a> of PRISM.
@ -1470,19 +1485,19 @@ If not, the default is to assume a single initial state, in which all variables
<pclass='vspace'>Lastly, state (but currently not transition) rewards can also be imported, using the <code>-importstaterewards</code> switch, e.g.:
<pclass='vspace'>In a similar style to PRISM's <aclass='wikilink'href='ExportingTheModel.html'><code>-exportmodel</code></a> switch, you can import several several files for a model using a single <code>-importmodel</code> switch. For example, this is equivalent to the command given above:
<pclass='vspace'>A related option is the <code>-exportvector <file></code> switch, useful in general contexts, not for experiments.
This exports the results for all states of the model
(typically, the log just displays the result for the initial state, unless a <aclass='wikilink'href='../PropertySpecification/Filters.html'>filter</a> has been used)
The format in which this information is input to the tool is exactly the same as is currently output
(see the section "<aclass='wikilink'href='ExportingTheModel.html'>Exporting The Model</a>" and the appendix "<aclass='wikilink'href='../Appendices/ExplicitModelFiles.html'>Explicit Model Files</a>").
Presently, this functionality is only supported in the command-line version of the tool, using the <code>-importtrans</code> switch (and more convenient <code>-importmodel</code>; see below).
At the moment, PRISM makes no attempt to discern the model type from the input file.
By default it assumes that the model is an MDP.
If this is not the case, the model type can be overwritten using the <code>-dtmc</code>, <code>-ctmc</code> and <code>-mdp</code> switches.
PRISM makes some attempt to discern the model type from the format of the input files,
but if this does not work, the model type can be overwritten using the <code>-dtmc</code>, <code>-ctmc</code> and <code>-mdp</code> switches.
<p>Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the <code>examples</code> directory of the distribution.
<p>Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the <code>prism-examples</code> directory of the distribution.
A few very small models are contained in the subdirectory <code>simple</code>;
the rest are in subdirectories grouped by model type.
</p>
<pclass='vspace'>The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error mIessage will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.
<pclass='vspace'>In this section, we describe the PRISM language and present a number of small illustrative examples.
A precise definition of the semantics of the language is available from the "<aclass='urllink'href='http://www.prismmodelchecker.org/doc/'>Documentation</a>" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples.
A number of these are included with the tool distribution in the <code>examples</code> directory.
A number of these are included with the tool distribution in the <code>prism-examples</code> directory.
Many additional examples can be found on the "<aclass='urllink'href='http://www.prismmodelchecker.org/casestudies/'>Case Studies</a>" section of the <aclass='urllink'href='http://www.prismmodelchecker.org/'>PRISM website</a>.
</p>
<pclass='vspace'>The fundamental components of the PRISM language are <em>modules</em> and <em>variables</em>.
@ -539,12 +539,12 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
</p>
<pclass='vspace'>Expressions can make use of several built-in functions:
</p>
<divclass='vspace'></div><ul><li><code>min(...)</code> and <code>max(...)</code>, which select the minimum and maximum value, respectively, of two or more numbers;
</li><li><code>floor(x)</code> and <code>ceil(x)</code>, which round <code>x</code> down and up, respectively, to the nearest integer;
</li><li><code>round(x)</code>, which rounds <code>x</code> to the nearest integer;
</li><li><code>pow(x,y)</code> which computes <code>x</code> to the power of <code>y</code>;
</li><li><code>mod(i,n)</code> for integer modulo operations;
</li><li><code>log(x,b)</code>, which computes the logarithm of <code>x</code> to base <code>b</code>.
<divclass='vspace'></div><ul><li><code>min(...)</code> and <code>max(...)</code>, which select the minimum and maximum value, respectively, of two or more numbers
</li><li><code>floor(x)</code> and <code>ceil(x)</code>, which round <code>x</code> down and up, respectively, to the nearest integer
</li><li><code>round(x)</code>, which rounds <code>x</code> to the nearest integer (note, in a tie-break, we always round <em>up</em>, e.g. <code>round(-1.5)</code> gives <code>-1</code> not <code>-2</code>)
</li><li><code>pow(x,y)</code> which computes <code>x</code> to the power of <code>y</code>
</li><li><code>mod(i,n)</code> for integer modulo operations
</li><li><code>log(x,b)</code>, which computes the logarithm of <code>x</code> to base <code>b</code>
</li></ul><pclass='vspace'>Examples of their usage are:
</p>
<divclass='vspace'></div>
@ -735,7 +735,7 @@ secondly, they are written using quotation marks (<code>"..."</code>), as illust
<h1>PTAs</h1>
<pclass='vspace'>So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs.
PRISM also supports a fourth: <em>probabilistic timed automata</em> (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of <em>timed automata</em> [<aclass='wikilink'href='../Main/References.html#AD94'>AD94</a>], by adding real-valued <em>clocks</em> which increase with time and can be reset. For background material on PTAs, see for example [<aclass='wikilink'href='../Main/References.html#NPS13'>NPS13</a>].
You can also find several example PTA models included in the PRISM distribution. Look in the <code>examples/pta</code> directory.
You can also find several example PTA models included in the PRISM distribution. Look in the <code>prism-examples/ptas</code> directory.
</p>
<pclass='vspace'>Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:
@ -127,12 +127,12 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
</p>
<pclass='vspace'>Expressions can make use of several built-in functions:
</p>
<divclass='vspace'></div><ul><li><code>min(...)</code> and <code>max(...)</code>, which select the minimum and maximum value, respectively, of two or more numbers;
</li><li><code>floor(x)</code> and <code>ceil(x)</code>, which round <code>x</code> down and up, respectively, to the nearest integer;
</li><li><code>round(x)</code>, which rounds <code>x</code> to the nearest integer;
</li><li><code>pow(x,y)</code> which computes <code>x</code> to the power of <code>y</code>;
</li><li><code>mod(i,n)</code> for integer modulo operations;
</li><li><code>log(x,b)</code>, which computes the logarithm of <code>x</code> to base <code>b</code>.
<divclass='vspace'></div><ul><li><code>min(...)</code> and <code>max(...)</code>, which select the minimum and maximum value, respectively, of two or more numbers
</li><li><code>floor(x)</code> and <code>ceil(x)</code>, which round <code>x</code> down and up, respectively, to the nearest integer
</li><li><code>round(x)</code>, which rounds <code>x</code> to the nearest integer (note, in a tie-break, we always round <em>up</em>, e.g. <code>round(-1.5)</code> gives <code>-1</code> not <code>-2</code>)
</li><li><code>pow(x,y)</code> which computes <code>x</code> to the power of <code>y</code>
</li><li><code>mod(i,n)</code> for integer modulo operations
</li><li><code>log(x,b)</code>, which computes the logarithm of <code>x</code> to base <code>b</code>
</li></ul><pclass='vspace'>Examples of their usage are:
<pclass='vspace'>In this section, we describe the PRISM language and present a number of small illustrative examples.
A precise definition of the semantics of the language is available from the "<aclass='urllink'href='http://www.prismmodelchecker.org/doc/'>Documentation</a>" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples.
A number of these are included with the tool distribution in the <code>examples</code> directory.
A number of these are included with the tool distribution in the <code>prism-examples</code> directory.
Many additional examples can be found on the "<aclass='urllink'href='http://www.prismmodelchecker.org/casestudies/'>Case Studies</a>" section of the <aclass='urllink'href='http://www.prismmodelchecker.org/'>PRISM website</a>.
</p>
<pclass='vspace'>The fundamental components of the PRISM language are <em>modules</em> and <em>variables</em>.
<pclass='vspace'>So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs.
PRISM also supports a fourth: <em>probabilistic timed automata</em> (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of <em>timed automata</em> [<aclass='wikilink'href='../Main/References.html#AD94'>AD94</a>], by adding real-valued <em>clocks</em> which increase with time and can be reset. For background material on PTAs, see for example [<aclass='wikilink'href='../Main/References.html#NPS13'>NPS13</a>].
You can also find several example PTA models included in the PRISM distribution. Look in the <code>examples/pta</code> directory.
You can also find several example PTA models included in the PRISM distribution. Look in the <code>prism-examples/ptas</code> directory.
</p>
<pclass='vspace'>Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:
This document is the main source of information regarding the installation and operation of the PRISM tool. For access to other resources, such as <aclass='urllink'href='http://www.prismmodelchecker.org/publications.php'>related publications</a> and details of <aclass='urllink'href='http://www.prismmodelchecker.org/casestudies/'>case studies</a>, or to <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>download</a> the tool itself, see the main <aclass='urllink'href='http://www.prismmodelchecker.org/'>PRISM website</a>.
</p>
<divclass='vspace'></div><h3>Which version of PRISM does this manual describe?</h3>
<p>This manual describes version <strong>4.5</strong>.
<p>This manual describes version <strong>4.6</strong>.
In general, the online copy of the manual corresponds to the most recent
Dave Parker
6 years ago