From 18d4fb7890a1f5d640dc3bb23e875c87d49a8d0a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Apr 2019 15:13:18 +0100 Subject: [PATCH] Update manual (4.5). --- manual/ConfiguringPRISM/AllOnOnePage.html | 41 ++- manual/ConfiguringPRISM/Main.html | 11 +- manual/ConfiguringPRISM/OtherOptions.html | 30 +- manual/InstallingPRISM/AllOnOnePage.html | 52 ++- .../CommonProblemsAndQuestions.html | 2 +- manual/InstallingPRISM/Main.html | 50 ++- manual/Main/AllOnOnePage.html | 321 ++++++++++-------- manual/Main/Main.html | 6 +- manual/RunningPRISM/AllOnOnePage.html | 108 +++--- manual/RunningPRISM/Experiments.html | 48 +-- manual/ThePRISMLanguage/AllOnOnePage.html | 2 + manual/ThePRISMLanguage/Expressions.html | 2 + manual/index.html | 6 +- 13 files changed, 389 insertions(+), 290 deletions(-) diff --git a/manual/ConfiguringPRISM/AllOnOnePage.html b/manual/ConfiguringPRISM/AllOnOnePage.html index 2d492a71..457f1f75 100644 --- a/manual/ConfiguringPRISM/AllOnOnePage.html +++ b/manual/ConfiguringPRISM/AllOnOnePage.html @@ -136,9 +136,14 @@ a.varlink { text-decoration:none; }

Introduction

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: +

From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:

@@ -159,7 +164,7 @@ a.varlink { text-decoration:none; }
[$[Get Code]]
-

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.:

@@ -465,12 +470,32 @@ You can also the CUDD maximum memory setting from the options panel in the GUI,
[$[Get Code]]
-

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. +

+
+
prism -javastack 1g big_model.pm
+xprism -javastack 1g big_model.pm
+
+
[$[Get Code]]
+
+ +

or: +

+
+
+
PRISM_JAVASTACKSIZE=1g
+export PRISM_JAVASTACKSIZE
+prism big_model.pm
+
+
[$[Get Code]]
+
+ +

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.

Precomputation

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: +

From the command-line version of PRISM, options are controlled by switches. A full list can be displayed by typing:

@@ -121,7 +126,7 @@ a.varlink { text-decoration:none; }
[$[Get Code]]
-

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.:

diff --git a/manual/ConfiguringPRISM/OtherOptions.html b/manual/ConfiguringPRISM/OtherOptions.html index 631c9968..22ffe397 100644 --- a/manual/ConfiguringPRISM/OtherOptions.html +++ b/manual/ConfiguringPRISM/OtherOptions.html @@ -144,12 +144,32 @@ You can also the CUDD maximum memory setting from the options panel in the GUI,
[$[Get Code]]
-

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. +

+
+
prism -javastack 1g big_model.pm
+xprism -javastack 1g big_model.pm
+
+
[$[Get Code]]
+
+ +

or: +

+
+
+
PRISM_JAVASTACKSIZE=1g
+export PRISM_JAVASTACKSIZE
+prism big_model.pm
+
+
[$[Get Code]]
+
+ +

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.

Precomputation

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; }

Instructions

Prerequisites

-

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:

-