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).
-User options and settings for the GUI are saved locally and reused. They are stored in the file .prism, which can be found in your home directory (~) under Unix, Linux or Mac OS X and in e.g. C:\Documents and Settings\username under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the .prism 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 .prism file and then re-launch the GUI.
+
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:
-From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing: +
$XDG_CONFIG_HOME/prism.settings (on Linux, if that environment variable is set)
+$HOME/.config/prism.settings (on Linux, if $XDG_CONFIG_HOME is not set)
+$HOME/Library/Preferences/prism.settings (on Mac OS)
+.prism in the user's home directory, e.g. C:\Documents and Settings\username (on Windows)
+$HOME/.prism (if the settings file was already created by an older version of PRISM)
+From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
The .prism settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
+
The settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
If you are running PRISM on Windows you will have to do this manually by modifying the prism.bat or xprism.bat scripts. To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+
If you get an error of the form java.lang.StackOverflowError, 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 -javastack switch or the PRISM_JAVASTACKSIZE environment variable.
+Examples are:
If you get an error of the form java.lang.StackOverflowError, then you can try increasing the stack size.
-On Unix, Linux or Mac OS X platforms, you can change the value of PRISM_JAVASTACKSIZE in the prism script
-(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in src/bin when you recompile).
-On Windows, you can edit the call to java or javaw directly, adding e.g. -Xss32M.
+
or: +
+ +If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the prism.bat or xprism.bat scripts.
+To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+To change the stack size to 1GB, add -Xss1g.
By default, PRISM's probabilistic model checking algorithms use an initial precomputation 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 -nopre switch. You can also disable the individual algorithms for probability 0/1 using switches -noprob0 and -noprob1.
diff --git a/manual/ConfiguringPRISM/Main.html b/manual/ConfiguringPRISM/Main.html
index fd81e985..4f00fbfa 100644
--- a/manual/ConfiguringPRISM/Main.html
+++ b/manual/ConfiguringPRISM/Main.html
@@ -98,9 +98,14 @@ a.varlink { text-decoration:none; }
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).
-User options and settings for the GUI are saved locally and reused. They are stored in the file .prism, which can be found in your home directory (~) under Unix, Linux or Mac OS X and in e.g. C:\Documents and Settings\username under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the .prism 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 .prism file and then re-launch the GUI.
+
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:
-From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing: +
$XDG_CONFIG_HOME/prism.settings (on Linux, if that environment variable is set)
+$HOME/.config/prism.settings (on Linux, if $XDG_CONFIG_HOME is not set)
+$HOME/Library/Preferences/prism.settings (on Mac OS)
+.prism in the user's home directory, e.g. C:\Documents and Settings\username (on Windows)
+$HOME/.prism (if the settings file was already created by an older version of PRISM)
+From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
The .prism settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
+
The settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
If you are running PRISM on Windows you will have to do this manually by modifying the prism.bat or xprism.bat scripts. To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+
If you get an error of the form java.lang.StackOverflowError, 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 -javastack switch or the PRISM_JAVASTACKSIZE environment variable.
+Examples are:
If you get an error of the form java.lang.StackOverflowError, then you can try increasing the stack size.
-On Unix, Linux or Mac OS X platforms, you can change the value of PRISM_JAVASTACKSIZE in the prism script
-(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in src/bin when you recompile).
-On Windows, you can edit the call to java or javaw directly, adding e.g. -Xss32M.
+
or: +
+ +If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the prism.bat or xprism.bat scripts.
+To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+To change the stack size to 1GB, add -Xss1g.
By default, PRISM's probabilistic model checking algorithms use an initial precomputation 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 -nopre switch. You can also disable the individual algorithms for probability 0/1 using switches -noprob0 and -noprob1.
diff --git a/manual/InstallingPRISM/AllOnOnePage.html b/manual/InstallingPRISM/AllOnOnePage.html
index 9556acdf..83ee6dc2 100644
--- a/manual/InstallingPRISM/AllOnOnePage.html
+++ b/manual/InstallingPRISM/AllOnOnePage.html
@@ -94,21 +94,26 @@ a.varlink { text-decoration:none; }
PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems. +
PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
You will need Java, version 8 or above. The tool is known to compile and run with both the Oracle and OpenJDK versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
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:
-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 prism/etc/scripts directory:
+
To install PRISM on Windows, just run the self-extracting installer which you downloaded. You do not need administrator privileges for this, just write-access to the directory chosen for installation.
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 xprism.bat (which may just appear as xprism) in the bin 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 cd bin, then xprism.bat and examine the resulting error. If you want to create shortcuts to xprism.bat manually, you will find some PRISM icons in the etc folder.
@@ -117,7 +122,7 @@ a.varlink { text-decoration:none; }
Problems? See the section "Common Problems And Questions''.
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 "Can't load IA 32-bit .dll on a AMD 64-bit platform".
-
You will probably also need to update bin\xprism.bat (and bin\prism.bat, if you use it), changing javaw on the last line to include the full path to the 32-bit executable.
-
Other than this, installing and running PRISM is as for the 32-bit case described above. -
-If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below). -
-Problems? See the section "Common Problems And Questions''. -
-To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris. +
To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux and Mac OS X.
To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the install.sh script, e.g.:
One thing to note: make sure you unzip the PRISM distribution from within Cygwin (e.g. using tar xfz prism-XXX-src.tar.gz). Don't use a Windows program (Winzip, etc.) since this can cause problems.
Problems? See the section "Common Problems And Questions''. +
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 +
+git config --global core.autocrlf false
+Problems? See the section "Common Problems And Questions''.
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: +
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:
When I try to run PRISM on Windows, I get an error of the form:Can't load IA 32-bit .dll on a AMD 64-bit platform
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 bin\xprism.bat (or bin\prism.bat) script, giving the full path to javaw at the end of the file.
+
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 bin\xprism.bat (or bin\prism.bat) script, giving the full path to javaw at the end of the file.
When I try to run PRISM on Windows, I get an error of the form:Can't load IA 32-bit .dll on a AMD 64-bit platform
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 bin\xprism.bat (or bin\prism.bat) script, giving the full path to javaw at the end of the file.
+
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 bin\xprism.bat (or bin\prism.bat) script, giving the full path to javaw at the end of the file.
PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of these operating systems. +
PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
You will need Java, version 8 or above. The tool is known to compile and run with both the Oracle and OpenJDK versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
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:
-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 prism/etc/scripts directory:
+
To install PRISM on Windows, just run the self-extracting installer which you downloaded. You do not need administrator privileges for this, just write-access to the directory chosen for installation.
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 xprism.bat (which may just appear as xprism) in the bin 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 cd bin, then xprism.bat and examine the resulting error. If you want to create shortcuts to xprism.bat manually, you will find some PRISM icons in the etc folder.
@@ -120,7 +125,7 @@ a.varlink { text-decoration:none; }
Problems? See the section "Common Problems And Questions''.
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 "Can't load IA 32-bit .dll on a AMD 64-bit platform".
-
You will probably also need to update bin\xprism.bat (and bin\prism.bat, if you use it), changing javaw on the last line to include the full path to the 32-bit executable.
-
Other than this, installing and running PRISM is as for the 32-bit case described above. -
-If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below). -
-Problems? See the section "Common Problems And Questions''. -
-To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris. +
To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux and Mac OS X.
To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the install.sh script, e.g.:
One thing to note: make sure you unzip the PRISM distribution from within Cygwin (e.g. using tar xfz prism-XXX-src.tar.gz). Don't use a Windows program (Winzip, etc.) since this can cause problems.
Problems? See the section "Common Problems And Questions''. +
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 +
+git config --global core.autocrlf false
+Problems? See the section "Common Problems And Questions''.
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: +
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:
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:
-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 prism/etc/scripts directory:
+
To install PRISM on Windows, just run the self-extracting installer which you downloaded. You do not need administrator privileges for this, just write-access to the directory chosen for installation.
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 xprism.bat (which may just appear as xprism) in the bin 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 cd bin, then xprism.bat and examine the resulting error. If you want to create shortcuts to xprism.bat manually, you will find some PRISM icons in the etc folder.
@@ -300,7 +305,7 @@ Models are supplied to the tool by writing descriptions in the
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 "Can't load IA 32-bit .dll on a AMD 64-bit platform".
-
You will probably also need to update bin\xprism.bat (and bin\prism.bat, if you use it), changing javaw on the last line to include the full path to the 32-bit executable.
-
Other than this, installing and running PRISM is as for the 32-bit case described above. -
-If this is not possible for some reason, an alternative is to build PRISM from source using Cygwin (See below). -
-Problems? See the section "Common Problems And Questions''. -
-To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux (32-bit) and, depending on availability, other operating systems such as Mac OS X and Solaris. +
To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux and Mac OS X.
To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the install.sh script, e.g.:
tar xfz prism-XXX-src.tar.gz). Don't use a Windows program (Winzip, etc.) since this can cause problems.
-Problems? See the section "Common Problems And Questions''. +
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 +
+git config --global core.autocrlf false
+Problems? See the section "Common Problems And Questions''.
@@ -438,7 +434,7 @@ Models are supplied to the tool by writing descriptions in the [$[Get Code]]
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: +
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:
where N=4:6 means that values of 4,5 and 6 are used for N,
-and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T. For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T.
For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+You can also specify double-valued constants as fractions rather than decimals. For example:
+
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.
You can export all the results from an experiment to a file or to the screen. From the command-line, use the -exportresults switch, for example:
to send to output file res.txt, or:
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.
The default behaviour is to export a list of results in text form, using tabs to separate items. The above examples produce:
-You can change the format in which the results are exported by appending one or more comma-separated options to the end of the -exportresults switch, for example to export in CSV (comma-separated values) format:
You can also add the matrix option, to export the results as one or more 2D matrices, rather than a list.
This is particularly useful if you want to create a surface plot from results that vary over two constants.
The matrix option is also available in normal (non-CSV) mode.
@@ -3543,14 +3551,14 @@ This is particularly useful if you want to create a surface plot from results th
Finally, you can export results in the form of comments, used by PRISM's functionality:
-When model checking some properties of MDPs, PRISM can also generate an optimal adversary, 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:
-which computes the maximum probability, over all adversaries, of reaching a state satisfying the label "error", 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 "error". 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
Currently, adversary generation is only implemented in the sparse engine, 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 -exportadv switch, e.g.:
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 adv.tra as in the example above.
@@ -3629,7 +3637,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
An SBML file comprises a set of species and a set of reactions which they undergo. Below is the SBML file for the simple reversible reaction: Na + Cl ↔ Na+ + Cl-, 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.
-And here is the resulting PRISM code:
-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".
At present, the SBML-to-PRISM translator is included in the PRISM code-base, but not integrated into the application itself.
-If you are using a binary (rather than source code) distribution of PRISM, replace classes with lib/prism.jar in the above.
@@ -3805,7 +3813,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
Alternatively (on Linux or Mac OS X), ensure prism is in your path and then save the script below as an executable file called sbml2prism:
Then use:
-The following PRISM properties file will also be useful:
-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 c at time T". The constant c is an integer index which can range between 1 and N, where N is the number of species in the model. To view the expected amount of each species over time, create an experiment in PRISM which varies c from 1 to N and T over the desired time range. @@ -3852,11 +3860,11 @@ prism "$@"
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:
-Alternatively, upper bounds can be modified manually after the translation process.
@@ -3877,10 +3885,10 @@ If this is not the case, the model type can be overwritten using the -dtmc
For example:
Please note that this method of constructing models in PRISM is typically less efficient than using the PRISM language. @@ -3893,20 +3901,20 @@ The following example shows how PRISM could be used to build, export and then re (not a good strategy in general):
-You can also import label information using the switch -importlabels, e.g.:
where the labels file (poll2.lab above) is in the format generated by the -exportlabels export option of PRISM.
@@ -3919,19 +3927,19 @@ If not, the default is to assume a single initial state, in which all variables
Lastly, state (but currently not transition) rewards can also be imported, using the -importstaterewards switch, e.g.:
In a similar style to PRISM's -exportmodel switch, you can import several several files for a model using a single -importmodel switch. For example, this is equivalent to the command given above:
The contents of each file is determined by its extension: @@ -3944,10 +3952,10 @@ Possible file extensions are:
Use the extension .all to import from all of these files:
@@ -3957,36 +3965,41 @@ Possible file extensions are:
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).
-User options and settings for the GUI are saved locally and reused. They are stored in the file .prism, which can be found in your home directory (~) under Unix, Linux or Mac OS X and in e.g. C:\Documents and Settings\username under Windows. Currently the "Options" dialog in the GUI represents the easiest way to modify the settings, but the .prism 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 .prism file and then re-launch the GUI.
+
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:
-From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing: +
$XDG_CONFIG_HOME/prism.settings (on Linux, if that environment variable is set)
+$HOME/.config/prism.settings (on Linux, if $XDG_CONFIG_HOME is not set)
+$HOME/Library/Preferences/prism.settings (on Mac OS)
+.prism in the user's home directory, e.g. C:\Documents and Settings\username (on Windows)
+$HOME/.prism (if the settings file was already created by an older version of PRISM)
+From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:
-For some switches, whose format is not straightforward, there is additional help available on the command-line, using -help switch. For example:
The .prism settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
+
The settings file is ignored by the command-line version (unlike earlier versions of PRISM, where it was used). You can, however, request that the settings file is read, using the -settings switch, e.g.:
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
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 -mtbdd, -sparse, -hybrid and -explicit (or -m, -s, -h and -ex, respectively) switches, e.g.:
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
By default PRISM uses a port of the ltl2dstar library to construct these automata. But it also allows the use of external LTL-to-automata converters producing deterministic automata through support for the Hanoi Omega Automaton (HOA) format. From the command line, an example of this is:
-The -ltl2datool switch specifies the location of the program to be executed to perform the LTL-to-automaton conversion. This will be called by PRISM as "exec in-file out-file", where exec is the executable, in-file is the name of a file containing the LTL formula to be converted and out-file 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 hoa-ltl2dstar-for-prism in the above example), which calls an external copy of ltl2dstar in the required fashion (assuming that the ltl2dstar and ltl2ba executables are located in the current directory or on the PATH).
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
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 -cuddmaxmem switch. For example:
Above, g denotes GB. You can also use m for MB.
@@ -4268,30 +4281,50 @@ You can also the CUDD maximum memory setting from the options panel in the GUI,
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 java.lang.OutOfMemory. To resolve this problem, you can increase this memory limit. On Unix, Linux or Mac OS X platforms, this can done by using the -javamaxmem switch, passed either to the command-line script prism or the GUI launcher xprism. For example:
each set the limit to 4GB. Alternatively, you set the environment variable PRISM_JAVAMAXMEM before running PRISM. For example, under a bash shell:
If you are running PRISM on Windows you will have to do this manually by modifying the prism.bat or xprism.bat scripts. To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+
If you get an error of the form java.lang.StackOverflowError, 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 -javastack switch or the PRISM_JAVASTACKSIZE environment variable.
+Examples are:
If you get an error of the form java.lang.StackOverflowError, then you can try increasing the stack size.
-On Unix, Linux or Mac OS X platforms, you can change the value of PRISM_JAVASTACKSIZE in the prism script
-(but note that, if you are compiling PRISM from source, this file gets regenerated from a template in src/bin when you recompile).
-On Windows, you can edit the call to java or javaw directly, adding e.g. -Xss32M.
+
or: +
+ +If you are running PRISM on Windows you will have to do make adjustments to Java memory manually, by modifying the prism.bat or xprism.bat scripts.
+To set the memory to 4GB, for example, add -Xmx4g to the list of arguments in the call to java or javaw at the end of the file.
+To change the stack size to 1GB, add -Xss1g.
By default, PRISM's probabilistic model checking algorithms use an initial precomputation 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 -nopre switch. You can also disable the individual algorithms for probability 0/1 using switches -noprob0 and -noprob1.
@@ -4370,23 +4403,23 @@ If PRISM crashes or freezes whilst not using all/most of the available memory (y
If PRISM has already output this:
-but there is no line of the form:
-and then you get an error like this:
-or like this:
-then PRISM ran out of memory whilst trying to construct the model. @@ -4436,18 +4469,18 @@ The first thing to try in this case is to increase the amount of memory availabl
If model construction was successfully completed (see previous question) but model checking was not, there are several things you can try. First of all, if the error message you see looks like the one in the previous question or you see a message such as
-then it may be worth increasing the memory limit for CUDD (as described above). However, if you see an error more like this:
-then increasing the memory CUDD probably will not help - PRISM is just trying to allocate more memory than is physically available on your system. @@ -4463,18 +4496,18 @@ The first thing to try in this case is to increase the amount of memory availabl
This is a less common problem and will only occur if the actual PRISM language description of your model is very large. This may be the case, for example, if you are automatically generating PRISM models in some way. Errors due to lack of memory during parsing usually look like:
-or:
-You can resolve this problem by increasing the memory allocated to Java. @@ -4521,7 +4554,7 @@ See the entry "Java memory" in the section "One solution to this, if your model require such a delay, is to approximate a deterministic delay with an Erlang distribution (a special case of a phase-type distribution). See for example this PRISM model:
-In the model, the occurrence of the the go-labelled action occurs with an Erlang distribution with mean mean and shape k. The special case of k=1 is just an exponential distribution. The graph below shows the probability distribution of the delay, i.e. of P=? [ F<=T x=1 ] for different values of k.
@@ -4573,7 +4606,7 @@ Below, we describe:
For the example PRISM model poll2.sm, the states file looks like:
-Here is an example, for the (DTMC) PRISM model lec3.pm (which looks like this):
-and here is one for the (CTMC) PRISM model poll2.sm (which looks like this):
-MDPs (or PAs) @@ -4660,7 +4693,7 @@ To clarify terminology: each state of the MDP contains (nondeterministi
Here is an example, for the (MDP) PRISM model lec12mdp.nm (which looks like this):
-and here is an action-labelled version of the same model, lec12mdpa.nm (which looks like this):
-Here is the result for the lec3.pm example from above (a DTMC):
-for the lec12mdp.nm example (an MDP):
-and for the lec12mdpa.nm example (an MDP with actions):
-For the lec3.pm (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):
-For the lec3.pm (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:
-And or the lec12mdpa.nm (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
-
diff --git a/manual/Main/Main.html b/manual/Main/Main.html
index 8ea0150e..8aa484d5 100644
--- a/manual/Main/Main.html
+++ b/manual/Main/Main.html
@@ -78,7 +78,7 @@ a.varlink { text-decoration:none; }
This document is the main source of information regarding the installation and operation of the PRISM tool. For access to other resources, such as related publications and details of case studies, or to download the tool itself, see the main PRISM website.
This manual describes version 4.4. +
This manual describes version 4.5. In general, the online copy of the manual corresponds to the most recent publically available version of PRISM (including beta versions). @@ -88,10 +88,10 @@ use the version included in that distribution.
This documentation is continuously updated and is best viewed online. If you are reading this online, you can use the built-in search 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.
-If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on one page 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 doc directory.
+
If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on one page and use the search functionality of your browser.
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 entire manual in this way. The best way to print the whole manual is to print the PDF version which is distributed with the tool. +
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 entire manual in this way.
If you have a question about PRISM and you cannot find the answer in this manual, please use the discussion group provided. Check the diff --git a/manual/RunningPRISM/AllOnOnePage.html b/manual/RunningPRISM/AllOnOnePage.html index 99031b43..d6ed008c 100644 --- a/manual/RunningPRISM/AllOnOnePage.html +++ b/manual/RunningPRISM/AllOnOnePage.html @@ -975,8 +975,18 @@ Before any verification can be performed, values must be provided for any such c
where N=4:6 means that values of 4,5 and 6 are used for N,
-and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T. For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T.
For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+You can also specify double-valued constants as fractions rather than decimals. For example:
+
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.
You can export all the results from an experiment to a file or to the screen. From the command-line, use the -exportresults switch, for example:
to send to output file res.txt, or:
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.
The default behaviour is to export a list of results in text form, using tabs to separate items. The above examples produce:
-You can change the format in which the results are exported by appending one or more comma-separated options to the end of the -exportresults switch, for example to export in CSV (comma-separated values) format:
You can also add the matrix option, to export the results as one or more 2D matrices, rather than a list.
This is particularly useful if you want to create a surface plot from results that vary over two constants.
The matrix option is also available in normal (non-CSV) mode.
@@ -1084,14 +1094,14 @@ This is particularly useful if you want to create a surface plot from results th
Finally, you can export results in the form of comments, used by PRISM's functionality:
-When model checking some properties of MDPs, PRISM can also generate an optimal adversary, 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:
-which computes the maximum probability, over all adversaries, of reaching a state satisfying the label "error", 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 "error". 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
Currently, adversary generation is only implemented in the sparse engine, 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 -exportadv switch, e.g.:
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 adv.tra as in the example above.
@@ -1170,7 +1180,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
An SBML file comprises a set of species and a set of reactions which they undergo. Below is the SBML file for the simple reversible reaction: Na + Cl ↔ Na+ + Cl-, 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.
-And here is the resulting PRISM code:
-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".
At present, the SBML-to-PRISM translator is included in the PRISM code-base, but not integrated into the application itself.
-If you are using a binary (rather than source code) distribution of PRISM, replace classes with lib/prism.jar in the above.
@@ -1346,7 +1356,7 @@ by selecting menu option "Model | View | Parsed PRISM model".
Alternatively (on Linux or Mac OS X), ensure prism is in your path and then save the script below as an executable file called sbml2prism:
Then use:
-The following PRISM properties file will also be useful:
-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 c at time T". The constant c is an integer index which can range between 1 and N, where N is the number of species in the model. To view the expected amount of each species over time, create an experiment in PRISM which varies c from 1 to N and T over the desired time range. @@ -1393,11 +1403,11 @@ prism "$@"
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:
-Alternatively, upper bounds can be modified manually after the translation process.
@@ -1418,10 +1428,10 @@ If this is not the case, the model type can be overwritten using the -dtmc
For example:
Please note that this method of constructing models in PRISM is typically less efficient than using the PRISM language. @@ -1434,20 +1444,20 @@ The following example shows how PRISM could be used to build, export and then re (not a good strategy in general):
-You can also import label information using the switch -importlabels, e.g.:
where the labels file (poll2.lab above) is in the format generated by the -exportlabels export option of PRISM.
@@ -1460,19 +1470,19 @@ If not, the default is to assume a single initial state, in which all variables
Lastly, state (but currently not transition) rewards can also be imported, using the -importstaterewards switch, e.g.:
In a similar style to PRISM's -exportmodel switch, you can import several several files for a model using a single -importmodel switch. For example, this is equivalent to the command given above:
The contents of each file is determined by its extension: @@ -1485,10 +1495,10 @@ Possible file extensions are:
Use the extension .all to import from all of these files:
where N=4:6 means that values of 4,5 and 6 are used for N,
-and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T. For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. steps of 10) are used for T.
For convenience, constant specifications can be split across separate instances of the -const switch, if desired.
+You can also specify double-valued constants as fractions rather than decimals. For example:
+
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.
You can export all the results from an experiment to a file or to the screen. From the command-line, use the -exportresults switch, for example:
to send to output file res.txt, or:
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.
The default behaviour is to export a list of results in text form, using tabs to separate items. The above examples produce:
-You can change the format in which the results are exported by appending one or more comma-separated options to the end of the -exportresults switch, for example to export in CSV (comma-separated values) format:
You can also add the matrix option, to export the results as one or more 2D matrices, rather than a list.
This is particularly useful if you want to create a surface plot from results that vary over two constants.
The matrix option is also available in normal (non-CSV) mode.
@@ -253,14 +263,14 @@ This is particularly useful if you want to create a surface plot from results th
Finally, you can export results in the form of comments, used by PRISM's functionality:
-min(...) and max(...), which select the minimum and maximum value, respectively, of two or more numbers;
floor(x) and ceil(x), which round x down and up, respectively, to the nearest integer;
+round(x), which rounds x to the nearest integer;
pow(x,y) which computes x to the power of y;
mod(i,n) for integer modulo operations;
log(x,b), which computes the logarithm of x to base b.
@@ -552,6 +553,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
max(a,b,c)min(...) and max(...), which select the minimum and maximum value, respectively, of two or more numbers;
floor(x) and ceil(x), which round x down and up, respectively, to the nearest integer;
+round(x), which rounds x to the nearest integer;
pow(x,y) which computes x to the power of y;
mod(i,n) for integer modulo operations;
log(x,b), which computes the logarithm of x to base b.
@@ -140,6 +141,7 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo
max(a,b,c)This manual describes version 4.4. +
This manual describes version 4.5. In general, the online copy of the manual corresponds to the most recent publically available version of PRISM (including beta versions). @@ -88,10 +88,10 @@ use the version included in that distribution.
This documentation is continuously updated and is best viewed online. If you are reading this online, you can use the built-in search 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.
-If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on one page 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 doc directory.
+
If you are browsing these pages off-line, for example using the copy distributed with the tool, you can view the whole manual on one page and use the search functionality of your browser.
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 entire manual in this way. The best way to print the whole manual is to print the PDF version which is distributed with the tool. +
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 entire manual in this way.
If you have a question about PRISM and you cannot find the answer in this manual, please use the discussion group provided. Check the