<p>The operation of PRISM can be configured in a number of ways. From the GUI, select "Options" from the main menu to bring up the "Options" dialog. The settings are grouped under several tabs. Those which affect the basic model checking functionality of the tool are under the heading "PRISM". Separate settings are available for the simulator and various aspects of the GUI (the model editor, the property editor and the log).
</p>
<pclass='vspace'>User options and settings for the GUI are saved locally and reused. They are stored in the file <code>.prism</code>, which can be found in your home directory (<code>~</code>) under Unix, Linux or Mac OS X and in e.g. <code>C:\Documents and Settings\username</code> under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the <code>.prism</code> file is in a simple textual format and can be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the <code>.prism</code> file and then re-launch the GUI.
<pclass='vspace'>User options and settings for the GUI are saved in a file locally and reused. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the settings file is in a simple textual format and can also be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the settings file re-launch the GUI. The location of the settings file depends on the operating system. As of PRISM 4.5, it is stored in:
</p>
<pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<divclass='vspace'></div><ul><li><code>$XDG_CONFIG_HOME/prism.settings</code> (on Linux, if that environment variable is set)
</li><li><code>$HOME/.config/prism.settings</code> (on Linux, if <code>$XDG_CONFIG_HOME</code> is not set)
</li><li><code>$HOME/Library/Preferences/prism.settings</code> (on Mac OS)
</li><li><code>.prism</code> in the user's home directory, e.g. <code>C:\Documents and Settings\username</code> (on Windows)
</li><li><code>$HOME/.prism</code> (if the settings file was already created by an older version of PRISM)
</li></ul><pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<pclass='vspace'>The <code>.prism</code>settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
<pclass='vspace'>The settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
</p>
<divclass='vspace'></div>
<divclass='sourceblock 'id='sourceblock3'>
@ -465,12 +470,32 @@ You can also the CUDD maximum memory setting from the options panel in the GUI,
<pclass='vspace'>If you are running PRISM on Windows you will have to do this manually by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts. To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size of the JVM.
On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javastack</code> switch or the <code>PRISM_JAVASTACKSIZE</code> environment variable.
Examples are:
</p>
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size.
On Unix, Linux or Mac OS X platforms, you can change the value of <code>PRISM_JAVASTACKSIZE</code> in the <code>prism</code> script
(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in <code>src/bin</code> when you recompile).
On Windows, you can edit the call to <code>java</code> or <code>javaw</code> directly, adding e.g. <code>-Xss32M</code>.
<pclass='vspace'>If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts.
To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
To change the stack size to 1GB, add <code>-Xss1g</code>.
</p>
<divclass='vspace'></div><h3>Precomputation</h3>
<p>By default, PRISM's probabilistic model checking algorithms use an initial <em>precomputation</em> step which uses graph-based techniques to efficient detect trivial cases where probabilities are 0 or 1. This can often result in improved performance and also reduce round-off errors. Occasionally, though, you may want to disable this step for efficiency (e.g. if you know that there are no/few such states and the precomputation process is slow). This can be done with the <code>-nopre</code> switch. You can also disable the individual algorithms for probability 0/1 using switches <code>-noprob0</code> and <code>-noprob1</code>.
<p>The operation of PRISM can be configured in a number of ways. From the GUI, select "Options" from the main menu to bring up the "Options" dialog. The settings are grouped under several tabs. Those which affect the basic model checking functionality of the tool are under the heading "PRISM". Separate settings are available for the simulator and various aspects of the GUI (the model editor, the property editor and the log).
</p>
<pclass='vspace'>User options and settings for the GUI are saved locally and reused. They are stored in the file <code>.prism</code>, which can be found in your home directory (<code>~</code>) under Unix, Linux or Mac OS X and in e.g. <code>C:\Documents and Settings\username</code> under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the <code>.prism</code> file is in a simple textual format and can be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the <code>.prism</code> file and then re-launch the GUI.
<pclass='vspace'>User options and settings for the GUI are saved in a file locally and reused. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the settings file is in a simple textual format and can also be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the settings file re-launch the GUI. The location of the settings file depends on the operating system. As of PRISM 4.5, it is stored in:
</p>
<pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<divclass='vspace'></div><ul><li><code>$XDG_CONFIG_HOME/prism.settings</code> (on Linux, if that environment variable is set)
</li><li><code>$HOME/.config/prism.settings</code> (on Linux, if <code>$XDG_CONFIG_HOME</code> is not set)
</li><li><code>$HOME/Library/Preferences/prism.settings</code> (on Mac OS)
</li><li><code>.prism</code> in the user's home directory, e.g. <code>C:\Documents and Settings\username</code> (on Windows)
</li><li><code>$HOME/.prism</code> (if the settings file was already created by an older version of PRISM)
</li></ul><pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<pclass='vspace'>The <code>.prism</code>settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
<pclass='vspace'>The settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
<pclass='vspace'>If you are running PRISM on Windows you will have to do this manually by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts. To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size of the JVM.
On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javastack</code> switch or the <code>PRISM_JAVASTACKSIZE</code> environment variable.
Examples are:
</p>
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size.
On Unix, Linux or Mac OS X platforms, you can change the value of <code>PRISM_JAVASTACKSIZE</code> in the <code>prism</code> script
(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in <code>src/bin</code> when you recompile).
On Windows, you can edit the call to <code>java</code> or <code>javaw</code> directly, adding e.g. <code>-Xss32M</code>.
<pclass='vspace'>If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts.
To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
To change the stack size to 1GB, add <code>-Xss1g</code>.
</p>
<divclass='vspace'></div><h3>Precomputation</h3>
<p>By default, PRISM's probabilistic model checking algorithms use an initial <em>precomputation</em> step which uses graph-based techniques to efficient detect trivial cases where probabilities are 0 or 1. This can often result in improved performance and also reduce round-off errors. Occasionally, though, you may want to disable this step for efficiency (e.g. if you know that there are no/few such states and the precomputation process is slow). This can be done with the <code>-nopre</code> switch. You can also disable the individual algorithms for probability 0/1 using switches <code>-noprob0</code> and <code>-noprob1</code>.
<p>PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems.
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
</p>
<pclass='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <aclass='urllink'href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <aclass='urllink'href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
</p>
<pclass='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
</p>
<divclass='vspace'></div><ul><li><ahref='AllOnOnePage.html#windows'>Installation on Windows (32-bit)</a>
</li><li><ahref='AllOnOnePage.html#windows64'>Installation on Windows (64-bit)</a>
<divclass='vspace'></div><ul><li><ahref='AllOnOnePage.html#windows'>Installation on Windows</a>
</li><li><ahref='AllOnOnePage.html#binaries'>Installation of Linux/Mac binary versions</a>
</li><li><ahref='AllOnOnePage.html#source'>Building PRISM from source (non-Windows)</a>
</li><li><ahref='AllOnOnePage.html#cygwin'>Building PRISM from source on Windows using Cygwin</a>
</li><li><ahref='AllOnOnePage.html#msys'>Building PRISM from source on Windows using MSYS</a>
</li></ul><pclass='vspace'>If you are installing on a completely fresh operating system installation (e.g. in a virtual machine), you may find the following scripts useful,
which install the required dependencies and PRISM itself. They can be found in the <code>prism/etc/scripts</code> directory:
</p>
<divclass='vspace'></div><ul><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-ubuntu'>script to build on a clean install of Ubuntu</a>
</li><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-rhel'>script to build on clean install of RHEL/CentOS/etc Linux</a>
<p>To install PRISM on Windows, just run the self-extracting installer which you <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>downloaded</a>. You do <strong>not</strong> need administrator privileges for this, just write-access to the directory chosen for installation.
</p>
<pclass='vspace'>If requested, the installer will place shortcuts to run PRISM on the desktop and/or start menu. If not, you can run by PRISM double-clicking the file <code>xprism.bat</code> (which may just appear as <code>xprism</code>) in the <code>bin</code> folder of your PRISM folder. If nothing happens, the most likely explanation is that Java is not installed or not in your path. To check, open a command prompt window, navigate to the PRISM directory, type <code>cd bin</code>, then <code>xprism.bat</code> and examine the resulting error. If you want to create shortcuts to <code>xprism.bat</code> manually, you will find some PRISM icons in the <code>etc</code> folder.
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<p>PRISM is known to run on 64-bit versions of Windows. Since we currently only provide 32-bit binary versions, you will need to install and use a 32-bit, rather than 64-bit version of Java. If not, you may see strange error messages like "<code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code>".
</p>
<pclass='vspace'>You will probably also need to update <code>bin\xprism.bat</code> (and <code>bin\prism.bat</code>, if you use it), changing <code>javaw</code> on the last line to include the full path to the 32-bit executable.
</p>
<pclass='vspace'>Other than this, installing and running PRISM is as for the 32-bit case described above.
</p>
<pclass='vspace'>If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below).
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p><h3>Installation of Linux/Mac binary versions</h3>
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris.
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux and Mac OS X.
</p>
<pclass='vspace'>To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the <code>install.sh</code> script, e.g.:
<pclass='vspace'>One thing to note: make sure you unzip the PRISM distribution from within Cygwin (e.g. using <code>tar xfz prism-XXX-src.tar.gz</code>). Don't use a Windows program (Winzip, etc.) since this can cause problems.
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<pclass='vspace'>If you use git to checkout the PRISM repository, we recommend that you use the version of git provided by Cygwin.
If you use a native Windows version of git, you may want to disable the Unix-to-Windows line-ending conversion, e.g., via
</li></ul><pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. We can solve this by means of a few commands:
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. You can solve this as follows:
<pclass='vspace'><strong>When I try to run PRISM on Windows, I get an error of the form:<br/><code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code></strong>
</p>
<divclass='vspace'></div><divclass='answer'>
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. You need to use a 32-bit version. Make sure you have a 32-bit version installed, and then either make sure it is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. The version of PRISM (32- or 64-bit) needs to match Java. Either download the 64-bit binary for PRISM, or use a 32-bit version of Java. For the latter case, either make sure the right version of Java is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
</p></div>
<divclass='vspace'></div><hr/>
<divclass='vspace'></div><h2>Running PRISM on non-Windows platforms</h2>
<pclass='vspace'><strong>When I try to run PRISM on Windows, I get an error of the form:<br/><code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code></strong>
</p>
<divclass='vspace'></div><divclass='answer'>
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. You need to use a 32-bit version. Make sure you have a 32-bit version installed, and then either make sure it is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. The version of PRISM (32- or 64-bit) needs to match Java. Either download the 64-bit binary for PRISM, or use a 32-bit version of Java. For the latter case, either make sure the right version of Java is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
</p></div>
<divclass='vspace'></div><hr/>
<divclass='vspace'></div><h2>Running PRISM on non-Windows platforms</h2>
<p>PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems.
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
</p>
<pclass='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <aclass='urllink'href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <aclass='urllink'href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
</p>
<pclass='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
</p>
<divclass='vspace'></div><ul><li><ahref='Main.html#windows'>Installation on Windows (32-bit)</a>
</li><li><ahref='Main.html#windows64'>Installation on Windows (64-bit)</a>
<divclass='vspace'></div><ul><li><ahref='Main.html#windows'>Installation on Windows</a>
</li><li><ahref='Main.html#binaries'>Installation of Linux/Mac binary versions</a>
</li><li><ahref='Main.html#source'>Building PRISM from source (non-Windows)</a>
</li><li><ahref='Main.html#cygwin'>Building PRISM from source on Windows using Cygwin</a>
</li><li><ahref='Main.html#msys'>Building PRISM from source on Windows using MSYS</a>
</li></ul><pclass='vspace'>If you are installing on a completely fresh operating system installation (e.g. in a virtual machine), you may find the following scripts useful,
which install the required dependencies and PRISM itself. They can be found in the <code>prism/etc/scripts</code> directory:
</p>
<divclass='vspace'></div><ul><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-ubuntu'>script to build on a clean install of Ubuntu</a>
</li><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-rhel'>script to build on clean install of RHEL/CentOS/etc Linux</a>
<p>To install PRISM on Windows, just run the self-extracting installer which you <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>downloaded</a>. You do <strong>not</strong> need administrator privileges for this, just write-access to the directory chosen for installation.
</p>
<pclass='vspace'>If requested, the installer will place shortcuts to run PRISM on the desktop and/or start menu. If not, you can run by PRISM double-clicking the file <code>xprism.bat</code> (which may just appear as <code>xprism</code>) in the <code>bin</code> folder of your PRISM folder. If nothing happens, the most likely explanation is that Java is not installed or not in your path. To check, open a command prompt window, navigate to the PRISM directory, type <code>cd bin</code>, then <code>xprism.bat</code> and examine the resulting error. If you want to create shortcuts to <code>xprism.bat</code> manually, you will find some PRISM icons in the <code>etc</code> folder.
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<p>PRISM is known to run on 64-bit versions of Windows. Since we currently only provide 32-bit binary versions, you will need to install and use a 32-bit, rather than 64-bit version of Java. If not, you may see strange error messages like "<code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code>".
</p>
<pclass='vspace'>You will probably also need to update <code>bin\xprism.bat</code> (and <code>bin\prism.bat</code>, if you use it), changing <code>javaw</code> on the last line to include the full path to the 32-bit executable.
</p>
<pclass='vspace'>Other than this, installing and running PRISM is as for the 32-bit case described above.
</p>
<pclass='vspace'>If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below).
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p><h3>Installation of Linux/Mac binary versions</h3>
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris.
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux and Mac OS X.
</p>
<pclass='vspace'>To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the <code>install.sh</code> script, e.g.:
<pclass='vspace'>One thing to note: make sure you unzip the PRISM distribution from within Cygwin (e.g. using <code>tar xfz prism-XXX-src.tar.gz</code>). Don't use a Windows program (Winzip, etc.) since this can cause problems.
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<pclass='vspace'>If you use git to checkout the PRISM repository, we recommend that you use the version of git provided by Cygwin.
If you use a native Windows version of git, you may want to disable the Unix-to-Windows line-ending conversion, e.g., via
</li></ul><pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. We can solve this by means of a few commands:
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. You can solve this as follows:
<divclass='vspace'></div><h1><spanclass='big'>PRISM Manual</span> version 4.4</h1>
<divclass='vspace'></div><h1><spanclass='big'>PRISM Manual</span> version 4.5</h1>
<hr/>
<h1><spanclass='big'>Contents</span></h1>
<hr/>
@ -277,21 +277,26 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
<hr/>
<h1>Instructions</h1>
<h3>Prerequisites</h3>
<p>PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems.
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
</p>
<pclass='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <aclass='urllink'href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <aclass='urllink'href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
</p>
<pclass='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
</p>
<divclass='vspace'></div><ul><li><ahref='AllOnOnePage.html#windows'>Installation on Windows (32-bit)</a>
</li><li><ahref='AllOnOnePage.html#windows64'>Installation on Windows (64-bit)</a>
<divclass='vspace'></div><ul><li><ahref='AllOnOnePage.html#windows'>Installation on Windows</a>
</li><li><ahref='AllOnOnePage.html#binaries'>Installation of Linux/Mac binary versions</a>
</li><li><ahref='AllOnOnePage.html#source'>Building PRISM from source (non-Windows)</a>
</li><li><ahref='AllOnOnePage.html#cygwin'>Building PRISM from source on Windows using Cygwin</a>
</li><li><ahref='AllOnOnePage.html#msys'>Building PRISM from source on Windows using MSYS</a>
</li></ul><pclass='vspace'>If you are installing on a completely fresh operating system installation (e.g. in a virtual machine), you may find the following scripts useful,
which install the required dependencies and PRISM itself. They can be found in the <code>prism/etc/scripts</code> directory:
</p>
<divclass='vspace'></div><ul><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-ubuntu'>script to build on a clean install of Ubuntu</a>
</li><li><aclass='urllink'href='https://raw.githubusercontent.com/prismmodelchecker/prism/master/prism/etc/scripts/prism-install-rhel'>script to build on clean install of RHEL/CentOS/etc Linux</a>
<p>To install PRISM on Windows, just run the self-extracting installer which you <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>downloaded</a>. You do <strong>not</strong> need administrator privileges for this, just write-access to the directory chosen for installation.
</p>
<pclass='vspace'>If requested, the installer will place shortcuts to run PRISM on the desktop and/or start menu. If not, you can run by PRISM double-clicking the file <code>xprism.bat</code> (which may just appear as <code>xprism</code>) in the <code>bin</code> folder of your PRISM folder. If nothing happens, the most likely explanation is that Java is not installed or not in your path. To check, open a command prompt window, navigate to the PRISM directory, type <code>cd bin</code>, then <code>xprism.bat</code> and examine the resulting error. If you want to create shortcuts to <code>xprism.bat</code> manually, you will find some PRISM icons in the <code>etc</code> folder.
@ -300,7 +305,7 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
@ -311,30 +316,17 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='../InstallingPRISM/CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<p>PRISM is known to run on 64-bit versions of Windows. Since we currently only provide 32-bit binary versions, you will need to install and use a 32-bit, rather than 64-bit version of Java. If not, you may see strange error messages like "<code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code>".
</p>
<pclass='vspace'>You will probably also need to update <code>bin\xprism.bat</code> (and <code>bin\prism.bat</code>, if you use it), changing <code>javaw</code> on the last line to include the full path to the 32-bit executable.
</p>
<pclass='vspace'>Other than this, installing and running PRISM is as for the 32-bit case described above.
</p>
<pclass='vspace'>If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below).
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='../InstallingPRISM/CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p><h3>Installation of Linux/Mac binary versions</h3>
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris.
<p>To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do <aclass='urllink'href='http://www.prismmodelchecker.org/download.php'>provide</a> pre-compiled binary distributions for Linux and Mac OS X.
</p>
<pclass='vspace'>To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the <code>install.sh</code> script, e.g.:
@ -423,7 +415,11 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
</p>
<pclass='vspace'>One thing to note: make sure you unzip the PRISM distribution from within Cygwin (e.g. using <code>tar xfz prism-XXX-src.tar.gz</code>). Don't use a Windows program (Winzip, etc.) since this can cause problems.
</p>
<pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='../InstallingPRISM/CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
<pclass='vspace'>If you use git to checkout the PRISM repository, we recommend that you use the version of git provided by Cygwin.
If you use a native Windows version of git, you may want to disable the Unix-to-Windows line-ending conversion, e.g., via
</li></ul><pclass='vspace'><strong>Problems?</strong> See the section "<aclass='wikilink'href='../InstallingPRISM/CommonProblemsAndQuestions.html'>Common Problems And Questions</a>''.
</p>
<divclass='vspace'></div><hr/>
<pclass='vspace'><aname='msys'id='msys'></a>
@ -438,7 +434,7 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. We can solve this by means of a few commands:
<pclass='vspace'>At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. You can solve this as follows:
</p>
<divclass='vspace'></div>
<divclass='sourceblock 'id='sourceblock8'>
@ -472,7 +468,7 @@ Models are supplied to the tool by writing descriptions in the <a class='wikilin
<pclass='vspace'><strong>When I try to run PRISM on Windows, I get an error of the form:<br/><code>Can't load IA 32-bit .dll on a AMD 64-bit platform</code></strong>
</p>
<divclass='vspace'></div><divclass='answer'>
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. You need to use a 32-bit version. Make sure you have a 32-bit version installed, and then either make sure it is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
<p>You are probably running a 32-bit Windows binary using a 64-bit version of Java. The version of PRISM (32- or 64-bit) needs to match Java. Either download the 64-bit binary for PRISM, or use a 32-bit version of Java. For the latter case, either make sure the right version of Java is first in your path or update the <code>bin\xprism.bat</code> (or <code>bin\prism.bat</code>) script, giving the full path to <code>javaw</code> at the end of the file.
</p></div>
<divclass='vspace'></div><hr/>
<divclass='vspace'></div><h2>Running PRISM on non-Windows platforms</h2>
@ -1076,6 +1072,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
</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>.
@ -1087,6 +1084,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
@ -3434,8 +3432,18 @@ Before any verification can be performed, values must be provided for any such c
</div>
<pclass='vspace'>where <code>N=4:6</code> means that values of 4,5 and 6 are used for <code>N</code>,
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>. For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>.
</p>
<pclass='vspace'>For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
You can also specify double-valued constants as fractions rather than decimals. For example:
<pclass='vspace'>From the GUI, the same thing can be achieved by selecting a single property,
right clicking on it and selecting "New experiment"
(or alternatively using the popup menu in the "Experiments" panel).
@ -3467,19 +3475,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".
@ -3487,7 +3495,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='sourceblock164'>
<divclass='sourceblock 'id='sourceblock165'>
<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:
@ -3566,10 +3574,10 @@ This is particularly useful if you want to create a surface plot from results th
<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.
@ -3579,10 +3587,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.
@ -3629,7 +3637,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):
@ -3793,11 +3801,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.
@ -3805,7 +3813,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='../RunningPRISM/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:
<pclass='vspace'>where the labels file (<code>poll2.lab</code> above) is in the format generated by the <code>-exportlabels</code><aclass='wikilink'href='../RunningPRISM/ExportingTheModel.html'>export option</a> of PRISM.
@ -3919,19 +3927,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='../RunningPRISM/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:
@ -3957,36 +3965,41 @@ Possible file extensions are:
<h1>Introduction</h1>
<p>The operation of PRISM can be configured in a number of ways. From the GUI, select "Options" from the main menu to bring up the "Options" dialog. The settings are grouped under several tabs. Those which affect the basic model checking functionality of the tool are under the heading "PRISM". Separate settings are available for the simulator and various aspects of the GUI (the model editor, the property editor and the log).
</p>
<pclass='vspace'>User options and settings for the GUI are saved locally and reused. They are stored in the file <code>.prism</code>, which can be found in your home directory (<code>~</code>) under Unix, Linux or Mac OS X and in e.g. <code>C:\Documents and Settings\username</code> under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the <code>.prism</code> file is in a simple textual format and can be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the <code>.prism</code> file and then re-launch the GUI.
<pclass='vspace'>User options and settings for the GUI are saved in a file locally and reused. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the settings file is in a simple textual format and can also be edited by hand. To restore the default options for PRISM, click "Load Defaults" and then "Save Options" from the "Options" dialog in the GUI. Alternatively, delete the settings file re-launch the GUI. The location of the settings file depends on the operating system. As of PRISM 4.5, it is stored in:
</p>
<pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<divclass='vspace'></div><ul><li><code>$XDG_CONFIG_HOME/prism.settings</code> (on Linux, if that environment variable is set)
</li><li><code>$HOME/.config/prism.settings</code> (on Linux, if <code>$XDG_CONFIG_HOME</code> is not set)
</li><li><code>$HOME/Library/Preferences/prism.settings</code> (on Mac OS)
</li><li><code>.prism</code> in the user's home directory, e.g. <code>C:\Documents and Settings\username</code> (on Windows)
</li><li><code>$HOME/.prism</code> (if the settings file was already created by an older version of PRISM)
</li></ul><pclass='vspace'>From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
<pclass='vspace'>For some switches, whose format is not straightforward, there is additional help available on the command-line, using <code>-help switch</code>. For example:
<pclass='vspace'>The <code>.prism</code>settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
<pclass='vspace'>The settings file is <em>ignored</em> by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file <em>is</em> read, using the <code>-settings</code> switch, e.g.:
<pclass='vspace'>In the following sections, we give a brief description of the most important configuration options available.
@ -4035,13 +4048,13 @@ Performance (time and space), however, may vary significantly and if you are usi
</li></ul><pclass='vspace'>When using the PRISM GUI, the engine to be used for model checking can be selected from the "Engine" option under the "PRISM" tab of the "Options" dialog. From the command-line, engines are activated using the <code>-mtbdd</code>, <code>-sparse</code>, <code>-hybrid</code> and <code>-explicit</code> (or <code>-m</code>, <code>-s</code>, <code>-h</code> and <code>-ex</code>, respectively) switches, e.g.:
<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.
@ -4178,19 +4191,19 @@ The default limit is 10,000 but can be changed with the "Termination max. iterat
<pclass='vspace'>By default PRISM uses a port of the <aclass='urllink'href='http://www.ltl2dstar.de/'>ltl2dstar</a> library to construct these automata. But it also allows the use of external LTL-to-automata converters producing deterministic automata through support for the <aclass='urllink'href='http://adl.github.io/hoaf/'>Hanoi Omega Automaton</a> (HOA) format. From the command line, an example of this is:
</p>
<divclass='vspace'></div>
<divclass='sourceblock 'id='sourceblock190'>
<divclass='sourceblock 'id='sourceblock191'>
<divclass='sourceblocktext'><divclass="shell"><spanstyle="font-weight:bold;">prism model.pm -pf "P=? [ G F x=1 ]" -ltl2datool hoa-ltl2dstar-for-prism -ltl2dasyntax lbt</span><br/>
<pclass='vspace'>The <code>-ltl2datool</code> switch specifies the location of the program to be executed to perform the LTL-to-automaton conversion. This will be called by PRISM as "<code>exec</code><code>in-file</code><code>out-file</code>", where <code>exec</code> is the executable, <code>in-file</code> is the name of a file containing the LTL formula to be converted and <code>out-file</code> is the name of a file where the resulting automaton should be written, in HOA format. Typically, the executable will be a script. Here is a simple example (called as <code>hoa-ltl2dstar-for-prism</code> in the above example), which calls an external copy of <code>ltl2dstar</code> in the required fashion (assuming that the <code>ltl2dstar</code> and <aclass='urllink'href='http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/'><code>ltl2ba</code></a> executables are located in the current directory or on the PATH).
<pclass='vspace'>PRISM is known to work with these HOA-enabled tools:
@ -4254,10 +4267,10 @@ You can also change the level of precision used to check that probabilities sum
<p>CUDD, the underlying BDD and MTBDD library used in PRISM has an upper memory limit. By default, this limit is 1 GB. If you are working on a machine with significantly more memory this and PRISM runs out of memory when model checking, it may help to change this. To set the limit, from the command-line, use the <code>-cuddmaxmem</code> switch. For example:
<pclass='vspace'>Above, <code>g</code> denotes GB. You can also use <code>m</code> for MB.
@ -4268,30 +4281,50 @@ You can also the CUDD maximum memory setting from the options panel in the GUI,
<p>The Java virtual machine (JVM) used to execute PRISM also has upper memory limits. Sometimes this limit will be exceeded and you will see an error of the form <code>java.lang.OutOfMemory</code>. To resolve this problem, you can increase this memory limit. On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javamaxmem</code> switch, passed either to the command-line script <code>prism</code> or the GUI launcher <code>xprism</code>. For example:
<pclass='vspace'>each set the limit to 4GB. Alternatively, you set the environment variable PRISM_JAVAMAXMEM before running PRISM. For example, under a <code>bash</code> shell:
<pclass='vspace'>If you are running PRISM on Windows you will have to do this manually by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts. To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size of the JVM.
On Unix, Linux or Mac OS X platforms, this can done by using the <code>-javastack</code> switch or the <code>PRISM_JAVASTACKSIZE</code> environment variable.
Examples are:
</p>
<pclass='vspace'>If you get an error of the form <code>java.lang.StackOverflowError</code>, then you can try increasing the stack size.
On Unix, Linux or Mac OS X platforms, you can change the value of <code>PRISM_JAVASTACKSIZE</code> in the <code>prism</code> script
(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in <code>src/bin</code> when you recompile).
On Windows, you can edit the call to <code>java</code> or <code>javaw</code> directly, adding e.g. <code>-Xss32M</code>.
<pclass='vspace'>If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the <code>prism.bat</code> or <code>xprism.bat</code> scripts.
To set the memory to 4GB, for example, add <code> -Xmx4g</code> to the list of arguments in the call to <code>java</code> or <code>javaw</code> at the end of the file.
To change the stack size to 1GB, add <code>-Xss1g</code>.
</p>
<divclass='vspace'></div><h3>Precomputation</h3>
<p>By default, PRISM's probabilistic model checking algorithms use an initial <em>precomputation</em> step which uses graph-based techniques to efficient detect trivial cases where probabilities are 0 or 1. This can often result in improved performance and also reduce round-off errors. Occasionally, though, you may want to disable this step for efficiency (e.g. if you know that there are no/few such states and the precomputation process is slow). This can be done with the <code>-nopre</code> switch. You can also disable the individual algorithms for probability 0/1 using switches <code>-noprob0</code> and <code>-noprob1</code>.
@ -4370,23 +4403,23 @@ If PRISM crashes or freezes whilst not using all/most of the available memory (y
<p>then PRISM ran out of memory whilst trying to construct the model.
@ -4436,18 +4469,18 @@ The first thing to try in this case is to increase the amount of memory availabl
<divclass='answer'>
<p>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
</p>
<divclass='sourceblock 'id='sourceblock199'>
<divclass='sourceblock 'id='sourceblock202'>
<divclass='sourceblocktext'><divclass="shell"><spanstyle="font-style:italic;">DD_MatrixMultiply: res is NULL</span><br/>
<p>then increasing the memory CUDD probably will not help - PRISM is just trying to allocate more memory than is physically available on your system.
@ -4463,18 +4496,18 @@ The first thing to try in this case is to increase the amount of memory availabl
<divclass='answer'>
<p>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:
</p>
<divclass='sourceblock 'id='sourceblock201'>
<divclass='sourceblock 'id='sourceblock204'>
<divclass='sourceblocktext'><divclass="shell"><spanstyle="font-weight:bold;">Exception in thread "main" java.lang.OutOfMemoryError: Java heap space </span><br/>
<p>You can resolve this problem by increasing the memory allocated to Java.
@ -4521,7 +4554,7 @@ See the entry "Java memory" in the section "<a class='wikilink' href='../Configu
<pclass='vspace'>One solution to this, if your model require such a delay, is to approximate a deterministic delay with an <aclass='urllink'href='http://en.wikipedia.org/wiki/Erlang_distribution'>Erlang distribution</a> (a special case of a phase-type distribution). See for example this PRISM model:
<pclass='vspace'>In the model, the occurrence of the the go-labelled action occurs with an Erlang distribution with mean <code>mean</code> and shape <code>k</code>. The special case of <code>k</code>=1 is just an exponential distribution. The graph below shows the probability distribution of the delay, i.e. of <code>P=? [ F<=T x=1 ]</code> for different values of <code>k</code>.
@ -4573,7 +4606,7 @@ Below, we describe:
<pclass='vspace'>For the example PRISM model <aclass='urllink'href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
<pclass='vspace'>Here is an example, for the (DTMC) PRISM model <aclass='urllink'href='../uploads/lec3.pm'>lec3.pm</a> (which looks like <aclass='urllink'href='../uploads/lec3.dot.pdf'>this</a>):
<pclass='vspace'>and here is one for the (CTMC) PRISM model <aclass='urllink'href='../uploads/poll2.sm'>poll2.sm</a> (which looks like <aclass='urllink'href='../uploads/poll2.dot.pdf'>this</a>):
@ -4660,7 +4693,7 @@ To clarify terminology: each <em>state</em> of the MDP contains (nondeterministi
<pclass='vspace'>Here is an example, for the (MDP) PRISM model <aclass='urllink'href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> (which looks like <aclass='urllink'href='../uploads/lec12mdp.dot.pdf'>this</a>):
<pclass='vspace'>and here is an action-labelled version of the same model, <aclass='urllink'href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (which looks like <aclass='urllink'href='../uploads/lec12mdpa.dot.pdf'>this</a>):
@ -4740,12 +4773,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):
@ -4757,25 +4790,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:
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.4</strong>.
<p>This manual describes version <strong>4.5</strong>.
In general, the online copy of the manual corresponds to the most recent
@ -88,10 +88,10 @@ use the version included in that distribution.
<divclass='vspace'></div><h3>How do I search the manual?</h3>
<p>This documentation is continuously updated and is best viewed online. If you are reading this online, you can use the built-in <aclass='wikilink'href='Search.html'>search</a> facility (there is a link in the grey box at the top of each page). For a nicer search interface (but possibly not 100% up-to-date index), you can also search with Google, using the search box in the banner at the top of the site.
</p>
<pclass='vspace'>If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on <aclass='wikilink'href='AllOnOnePage.html'>one page</a> and use the search functionality of your browser. Alternatively, search the PDF version of the manual, which is also distributed with the tool, in the <code>doc</code> directory.
<pclass='vspace'>If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on <aclass='wikilink'href='AllOnOnePage.html'>one page</a> and use the search functionality of your browser.
</p>
<divclass='vspace'></div><h3>How do I print the manual?</h3>
<p>To print an individual page of the manual click on the "Print" link at the top-right hand corner of the page (in the online version) and print the page from your web browser. You can also print an entire section (see the "View all" link under the contents on the left) or the <aclass='wikilink'href='AllOnOnePage.html'>entire manual</a> in this way. The best way to print the whole manual is to print the PDF version which is distributed with the tool.
<p>To print an individual page of the manual click on the "Print" link at the top-right hand corner of the page (in the online version) and print the page from your web browser. You can also print an entire section (see the "View all" link under the contents on the left) or the <aclass='wikilink'href='AllOnOnePage.html'>entire manual</a> in this way.
</p>
<divclass='vspace'></div><h3>More questions?</h3>
<p>If you have a question about PRISM and you cannot find the answer in this manual, please use the discussion group provided. Check the
@ -975,8 +975,18 @@ Before any verification can be performed, values must be provided for any such c
</div>
<pclass='vspace'>where <code>N=4:6</code> means that values of 4,5 and 6 are used for <code>N</code>,
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>. For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>.
</p>
<pclass='vspace'>For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
You can also specify double-valued constants as fractions rather than decimals. For example:
<pclass='vspace'>From the GUI, the same thing can be achieved by selecting a single property,
right clicking on it and selecting "New experiment"
(or alternatively using the popup menu in the "Experiments" panel).
@ -1008,19 +1018,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".
@ -1028,7 +1038,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='sourceblock43'>
<divclass='sourceblock 'id='sourceblock44'>
<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:
@ -1107,10 +1117,10 @@ This is particularly useful if you want to create a surface plot from results th
<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.
@ -1120,10 +1130,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.
@ -1170,7 +1180,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):
@ -1334,11 +1344,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.
@ -1346,7 +1356,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:
<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.
@ -1460,19 +1470,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:
@ -144,8 +144,18 @@ Before any verification can be performed, values must be provided for any such c
</div>
<pclass='vspace'>where <code>N=4:6</code> means that values of 4,5 and 6 are used for <code>N</code>,
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>. For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
and <code>T=60:10:100</code> means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for <code>T</code>.
</p>
<pclass='vspace'>For convenience, constant specifications can be split across separate instances of the <code>-const</code> switch, if desired.
You can also specify double-valued constants as fractions rather than decimals. For example:
<pclass='vspace'>From the GUI, the same thing can be achieved by selecting a single property,
right clicking on it and selecting "New experiment"
(or alternatively using the popup menu in the "Experiments" panel).
@ -177,19 +187,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".
@ -197,7 +207,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='sourceblock6'>
<divclass='sourceblock 'id='sourceblock7'>
<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:
@ -541,6 +541,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
</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>.
@ -552,6 +553,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
@ -129,6 +129,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
</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>.
@ -140,6 +141,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
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.4</strong>.
<p>This manual describes version <strong>4.5</strong>.
In general, the online copy of the manual corresponds to the most recent
@ -88,10 +88,10 @@ use the version included in that distribution.
<divclass='vspace'></div><h3>How do I search the manual?</h3>
<p>This documentation is continuously updated and is best viewed online. If you are reading this online, you can use the built-in <aclass='wikilink'href='Main/Search.html'>search</a> facility (there is a link in the grey box at the top of each page). For a nicer search interface (but possibly not 100% up-to-date index), you can also search with Google, using the search box in the banner at the top of the site.
</p>
<pclass='vspace'>If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on <aclass='wikilink'href='Main/AllOnOnePage.html'>one page</a> and use the search functionality of your browser. Alternatively, search the PDF version of the manual, which is also distributed with the tool, in the <code>doc</code> directory.
<pclass='vspace'>If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on <aclass='wikilink'href='Main/AllOnOnePage.html'>one page</a> and use the search functionality of your browser.
</p>
<divclass='vspace'></div><h3>How do I print the manual?</h3>
<p>To print an individual page of the manual click on the "Print" link at the top-right hand corner of the page (in the online version) and print the page from your web browser. You can also print an entire section (see the "View all" link under the contents on the left) or the <aclass='wikilink'href='Main/AllOnOnePage.html'>entire manual</a> in this way. The best way to print the whole manual is to print the PDF version which is distributed with the tool.
<p>To print an individual page of the manual click on the "Print" link at the top-right hand corner of the page (in the online version) and print the page from your web browser. You can also print an entire section (see the "View all" link under the contents on the left) or the <aclass='wikilink'href='Main/AllOnOnePage.html'>entire manual</a> in this way.
</p>
<divclass='vspace'></div><h3>More questions?</h3>
<p>If you have a question about PRISM and you cannot find the answer in this manual, please use the discussion group provided. Check the
Dave Parker
7 years ago