diff --git a/manual/Appendices/AllOnOnePage.html b/manual/Appendices/AllOnOnePage.html index 5f933255..f85618a2 100644 --- a/manual/Appendices/AllOnOnePage.html +++ b/manual/Appendices/AllOnOnePage.html @@ -116,6 +116,7 @@ Below, we describe:
@@ -285,6 +286,25 @@ To clarify terminology: each state of the MDP contains (nondeterministi
[$[Get Code]]
+
+

+

Labels (.lab) files

+

These contain an explicit list of which labels are satisfied in each state. +The first line lists the labels, assigning each one an index. +The remaining lines list indices of all states satisfying one or more labels, +followed by a list of the the indices of labels that that are satisfied in it. +This includes the built-in labels "init" (initial states) and deadlock (deadlock states). +An example is shown below, where, for example, both "heads" and "end" are satisfied in state 2. +

+
+
+
0="init" 1="deadlock" 2="heads" 3="tails" 4="end"
+0: 0
+2: 2 4
+3: 3 4
+
[$[Get Code]]
+
+

State rewards (.srew) files

@@ -293,12 +313,12 @@ To clarify terminology: each state of the MDP contains (nondeterministi

For the lec3.pm (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):

-
+
6 3
0 2
4 1
5 1
-
[$[Get Code]]
+
[$[Get Code]]
@@ -310,25 +330,25 @@ except that probabilities/rates are replaced with reward values, and the number

For the lec3.pm (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:

-
+
6 4
1 0 1
1 2 1
1 4 1
2 5 2
-
[$[Get Code]]
+
[$[Get Code]]

And or the lec12mdpa.nm (4-state) MDP example, we get non-zero transition rewards on 4 transitions:

-
+
4 5 4
1 0 2 6
1 0 3 6
1 1 0 5
1 1 1 5
-
[$[Get Code]]
+
[$[Get Code]]
diff --git a/manual/Appendices/ExplicitModelFiles.html b/manual/Appendices/ExplicitModelFiles.html index 173182d3..5653b3d9 100644 --- a/manual/Appendices/ExplicitModelFiles.html +++ b/manual/Appendices/ExplicitModelFiles.html @@ -119,6 +119,7 @@ Below, we describe:
@@ -288,6 +289,25 @@ To clarify terminology: each state of the MDP contains (nondeterministi
[$[Get Code]]
+
+

+

Labels (.lab) files

+

These contain an explicit list of which labels are satisfied in each state. +The first line lists the labels, assigning each one an index. +The remaining lines list indices of all states satisfying one or more labels, +followed by a list of the the indices of labels that that are satisfied in it. +This includes the built-in labels "init" (initial states) and deadlock (deadlock states). +An example is shown below, where, for example, both "heads" and "end" are satisfied in state 2. +

+
+
+
0="init" 1="deadlock" 2="heads" 3="tails" 4="end"
+0: 0
+2: 2 4
+3: 3 4
+
[$[Get Code]]
+
+

State rewards (.srew) files

@@ -296,12 +316,12 @@ To clarify terminology: each state of the MDP contains (nondeterministi

For the lec3.pm (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):

-
+
6 3
0 2
4 1
5 1
-
[$[Get Code]]
+
[$[Get Code]]
@@ -313,25 +333,25 @@ except that probabilities/rates are replaced with reward values, and the number

For the lec3.pm (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:

-
+
6 4
1 0 1
1 2 1
1 4 1
2 5 2
-
[$[Get Code]]
+
[$[Get Code]]

And or the lec12mdpa.nm (4-state) MDP example, we get non-zero transition rewards on 4 transitions:

-
+
4 5 4
1 0 2 6
1 0 3 6
1 1 0 5
1 1 1 5
-
[$[Get Code]]
+
[$[Get Code]]
diff --git a/manual/ConfiguringPRISM/AllOnOnePage.html b/manual/ConfiguringPRISM/AllOnOnePage.html index 457f1f75..955363fc 100644 --- a/manual/ConfiguringPRISM/AllOnOnePage.html +++ b/manual/ConfiguringPRISM/AllOnOnePage.html @@ -230,6 +230,12 @@ Performance (time and space), however, may vary significantly and if you are usi

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.

+

PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically, +based on the size and type of the model, and the property being checked. +Use, for example, -heuristic speed from the command-line to choose options +which target computation speed rather than saving memory. +This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI. +

Approximate/statistical model checking

Although it is not treated as a separate "engine", like those above, PRISM also provides approximate/statistical model checking, diff --git a/manual/ConfiguringPRISM/ComputationEngines.html b/manual/ConfiguringPRISM/ComputationEngines.html index 50a7a5b0..34402978 100644 --- a/manual/ConfiguringPRISM/ComputationEngines.html +++ b/manual/ConfiguringPRISM/ComputationEngines.html @@ -149,6 +149,12 @@ Performance (time and space), however, may vary significantly and if you are usi

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.

+

PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically, +based on the size and type of the model, and the property being checked. +Use, for example, -heuristic speed from the command-line to choose options +which target computation speed rather than saving memory. +This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI. +

Approximate/statistical model checking

Although it is not treated as a separate "engine", like those above, PRISM also provides approximate/statistical model checking, diff --git a/manual/InstallingPRISM/AllOnOnePage.html b/manual/InstallingPRISM/AllOnOnePage.html index 83ee6dc2..e7b41e4d 100644 --- a/manual/InstallingPRISM/AllOnOnePage.html +++ b/manual/InstallingPRISM/AllOnOnePage.html @@ -123,7 +123,7 @@ which install the required dependencies and PRISM itself. They can be found in t

cd "c:\Program Files\prism-4.5-win\bin"
-prism ..\examples\dice\dice.pm
+prism ..\prism-examples\simple\dice\dice.pm
[$[Get Code]]
diff --git a/manual/InstallingPRISM/Main.html b/manual/InstallingPRISM/Main.html index cd0e55a7..35c91320 100644 --- a/manual/InstallingPRISM/Main.html +++ b/manual/InstallingPRISM/Main.html @@ -126,7 +126,7 @@ which install the required dependencies and PRISM itself. They can be found in t
cd "c:\Program Files\prism-4.5-win\bin"
-prism ..\examples\dice\dice.pm
+prism ..\prism-examples\simple\dice\dice.pm
[$[Get Code]]
diff --git a/manual/Main/AllOnOnePage.html b/manual/Main/AllOnOnePage.html index 39377a8c..eef29779 100644 --- a/manual/Main/AllOnOnePage.html +++ b/manual/Main/AllOnOnePage.html @@ -178,7 +178,7 @@ a.varlink { text-decoration:none; }
-

PRISM Manual   version 4.5

+

PRISM Manual   version 4.6

Contents

@@ -306,7 +306,7 @@ which install the required dependencies and PRISM itself. They can be found in t
cd "c:\Program Files\prism-4.5-win\bin"
-prism ..\examples\dice\dice.pm
+prism ..\prism-examples\simple\dice\dice.pm
[$[Get Code]]
@@ -639,7 +639,7 @@ on the PRISM web site.

In this section, we describe the PRISM language and present a number of small illustrative examples. A precise definition of the semantics of the language is available from the "Documentation" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples. -A number of these are included with the tool distribution in the examples directory. +A number of these are included with the tool distribution in the prism-examples directory. Many additional examples can be found on the "Case Studies" section of the PRISM website.

The fundamental components of the PRISM language are modules and variables. @@ -1070,12 +1070,12 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo

Expressions can make use of several built-in functions:

-
  • 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. +
    • 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 (note, in a tie-break, we always round up, e.g. round(-1.5) gives -1 not -2) +
    • 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

    Examples of their usage are:

    @@ -1266,7 +1266,7 @@ secondly, they are written using quotation marks ("..."), as illust

    PTAs

    So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs. PRISM also supports a fourth: probabilistic timed automata (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of timed automata [AD94], by adding real-valued clocks which increase with time and can be reset. For background material on PTAs, see for example [NPS13]. -You can also find several example PTA models included in the PRISM distribution. Look in the examples/pta directory. +You can also find several example PTA models included in the PRISM distribution. Look in the prism-examples/ptas directory.

    Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:

    @@ -2151,8 +2151,8 @@ the rewards associated with the model correspond to power consumption, the prope

    - - + +
     FcosafeC<=tCI=tS
    DTMCsSMHESMHESMHESMHESMHESMH-
    CTMCsSMHESMHESMHESMHESMHESMH-
    DTMCsSMHESMHESMHESMHESMHESMHE
    CTMCsSMHESMHESMHESMHESMHESMHE
    MDPsSM-ESMHES--E----SM-E----

    Non-Probabilistic Properties

    @@ -2539,7 +2539,7 @@ e.g. until (U) properties are allowed, as are cloc
    [$[Get Code]]
-

This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons +

This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons (e.g. x<=5 is allowed, x<5 is not).

The digital clocks also has support for rewards: @@ -2675,7 +2675,9 @@ Some screenshots of the GUI version of PRISM are shown below.


The PRISM GUI (model checking)

Loading And Building a Model

-

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the examples directory of the distribution. +

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the prism-examples directory of the distribution. +A few very small models are contained in the subdirectory simple; +the rest are in subdirectories grouped by model type.

The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error mIessage will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.

@@ -3152,7 +3154,7 @@ You can optionally request that state descriptions are added to each state of gr

Typically, once a model has been constructed, it is analysed through model checking. Properties are specified as described in the "Property Specification" section, and are usually kept in files with extensions .props, .pctl or .csl. -There are properties files accompanying most of the sample PRISM models in the examples directory. +There are properties files accompanying most of the sample PRISM models in the prism-examples directory.

GUI

@@ -3206,15 +3208,25 @@ For example, to check only the fourth property in the file:
[$[Get Code]]
-

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

You can also provide a comma-separated list of multiple properties to check, +using neither numerical indices or property names:

-
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
prism poll2.sm poll.csl -prop 4,5,safe
[$[Get Code]]
+

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

+
+
+
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
+
[$[Get Code]]
+
+

The switches -pctl and -csl are aliases for -pf.

Note the use of single quotes ('...') to avoid characters such as @@ -3302,10 +3314,10 @@ If, for a given property, statistical model checking results in one or more path

Statistical model checking can also be enabled from the command-line version of PRISM, by including the -sim switch. The default methods used are CI (Confidence Interval) for "quantitative" properties and SPRT (Sequential Probability Ratio Test) for "bounded" properties. To select a particular method, use switch -simmethod <method> where <method> is one of ci, aci, apmc and sprt. For example:

-
+
prism model.pm model.pctl -prop 1 -sim -simmethod aci
-
[$[Get Code]]
+
[$[Get Code]]

PRISM has default values for the various simulation method parameters, but these can also be specified using the switches -simsamples, -simconf, -simwidth and -simapprox. The exact meaning of these switches for each simulation method is given in the table below. @@ -3334,19 +3346,19 @@ time value for which you wish to compute probabilities. From the command-line, add the -steadystate (or -ss) switch:

-
+
prism poll2.sm -ss
-
[$[Get Code]]
+
[$[Get Code]]

for steady-state probabilities or the -transient (or -tr) switch:

-
+
prism poll2.sm -tr 2.0
-
[$[Get Code]]
+
[$[Get Code]]

for transient probabilities, again specifying a time value in the latter case. @@ -3356,11 +3368,11 @@ either on the screen (from the command-line) or in the log (from the GUI).

To instead export the vector of computed probabilities to a file, use the "Model | Compute/export" option from the GUI, or the -exportsteadystate (or -exportss) and -exporttransient (or -exporttr) switches from the command-line:

-
+
prism poll2.sm -ss -exportss poll2-ss.txt
prism poll2.sm -tr 2.0 -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

From the command-line, you can request that the probability vectors exported are in Matlab format by adding the -exportmatlab switch. @@ -3372,30 +3384,30 @@ an equiprobable choice over the set of initial states. You can override this and provide a specific initial distribution. This is done using the -importinitdist switch. The format for this imported distribution is identical to the ones exported by PRISM, i.e. simply a list of probabilities for all states separated by new lines. For example, this:

-
+
prism poll2.sm -tr 1.0 -exporttr poll2-tr1.txt
prism poll2.sm -tr 1.0 -importinitdist poll2-tr1.txt -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

is (essentially) equivalent to this:

-
+
prism poll2.sm -tr 2.0 -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

Ranges of time values

Finally, you can compute transient probabilities for a range of time values, e.g.:

-
+
prism poll2.sm -tr 0.1:0.01:0.2
-
[$[Get Code]]
+
[$[Get Code]]

which computes transient probabilities for the time points 0.1, 0.11, 0.12, .., 0.2. In this case, the computation is done incrementally, with probabilities for each time point being computed from the previous point for efficiency. @@ -3405,30 +3417,30 @@ You can override this and provide a specific initial distribution. This is done This is done by leaving one or more constants undefined, e.g.:

-
+
const int N;
const double T;
-
[$[Get Code]]
+
[$[Get Code]]

This can be done for constants in the model file, the properties file, or both. Before any verification can be performed, values must be provided for any such constants. In the GUI, a dialog appears in which the user is required to enter values. From the command line, the -const switch must be used, e.g.:

-
+
prism cluster.sm cluster.csl -const N=4,T=85.9
-
[$[Get Code]]
+
[$[Get Code]]

To run an experiment, provide a range of values for one or more of the constants. Model checking will be performed for all combinations of the constant values provided. For example:

-
+
prism cluster.sm cluster.csl -const N=4:6,T=60:10:100
-
[$[Get Code]]
+
[$[Get Code]]

where N=4:6 means that values of 4,5 and 6 are used for N, @@ -3438,10 +3450,10 @@ and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. s You can also specify double-valued constants as fractions rather than decimals. For example:

-
+
prism cluster.sm cluster.csl -const N=4,T=85.9 -const p=1/3
-
[$[Get Code]]
+
[$[Get Code]]

From the GUI, the same thing can be achieved by selecting a single property, @@ -3475,19 +3487,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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt
-
[$[Get Code]]
+
[$[Get Code]]

to send to output file res.txt, or:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults stdout
-
[$[Get Code]]
+
[$[Get Code]]

to send the results straight to the screen. From the GUI, right click on the experiment and select "Export results". @@ -3495,7 +3507,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:

-
+
N       T       Result
4       0       0.0
4       10      4.707364688019771E-6
@@ -3503,20 +3515,20 @@ or as code which can be used to generate the graph in Matlab. 5       0       0.0
5       10      3.267731327728599E-6
5       20      8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:csv
-
[$[Get Code]]
+
[$[Get Code]]
-
+
N, T, Result
4, 0, 0.0
4, 10, 4.707364688019771E-6
@@ -3524,26 +3536,26 @@ or as code which can be used to generate the graph in Matlab. 5, 0, 0.0
5, 10, 3.267731327728599E-6
5, 20, 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

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.

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:csv,matrix
-
[$[Get Code]]
+
[$[Get Code]]
-
+
"N\T"
, 0.0, 10.0, 20.0
4, 0.0, 4.707364688019771E-6, 1.3126420636755292E-5
5, 0.0, 3.267731327728599E-6, 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

The matrix option is also available in normal (non-CSV) mode. @@ -3551,14 +3563,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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:comment
-
[$[Get Code]]
+
[$[Get Code]]
-
+
// RESULT (N=4,T=0): 0.0
// RESULT (N=4,T=10): 4.707364688019771E-6
// RESULT (N=4,T=20): 1.3126420636755292E-5
@@ -3566,18 +3578,22 @@ This is particularly useful if you want to create a surface plot from results th // RESULT (N=5,T=10): 3.267731327728599E-6
// RESULT (N=5,T=20): 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]
-
+

A related option is the -exportvector <file> switch, useful in general contexts, not for experiments. +This exports the results for all states of the model +(typically, the log just displays the result for the initial state, unless a filter has been used) +to the the file file. +

Adversaries

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:

-
+
Pmax=? [ F "error" ]
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -3587,10 +3603,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.:

-
+
prism mdp.nm -pctl 'Pmax=? [ F "error" ]' -exportadv adv.tra -s
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -3615,7 +3631,7 @@ Secondly, each local state of a sequential component must be named. For exampl definition of these differs from the PEPA definition. Every PEPA synchronisation must have exactly one active component. Some examples of PEPA model descriptions which can be imported into PRISM -can be found in the examples/pepa directory. +can be found in the prism-examples/pepa directory.

From the command-line version of PRISM, add the -importpepa switch and the model will be treated as a PEPA description. From the GUI, select "Model | Open model" and then choose "PEPA models" @@ -3637,7 +3653,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.

-
+
<?xml version="1.0" encoding="UTF-8"?>
<sbml xmlns="http://www.sbml.org/sbml/level2" metaid="_000000" level="2" version="1">
  <model id="nacl" name="Na+Cl">
@@ -3697,13 +3713,13 @@ by selecting menu option "Model | View | Parsed PRISM model".
  </model>
</sbml>
-
[$[Get Code]]
+
[$[Get Code]]

And here is the resulting PRISM code:

-
+
// File generated by automatic SBML-to-PRISM conversion
// Original SBML file: nacl.xml

@@ -3790,7 +3806,7 @@ by selecting menu option "Model | View | Parsed PRISM model". // 4
rewards "cl_minus" true : cl_minus; endrewards
-
[$[Get Code]]
+
[$[Get 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): @@ -3801,11 +3817,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.

-
+
cd prism
java -cp classes prism.SBML2Prism sbml_file.xml > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

If you are using a binary (rather than source code) distribution of PRISM, replace classes with lib/prism.jar in the above. @@ -3813,7 +3829,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:

-
+
#!/bin/sh

# Startup script for SBML-to-PRISM translator
@@ -3822,28 +3838,28 @@ by selecting menu option "Model | View | Parsed PRISM model". PRISM_MAINCLASS="prism.SBML2Prism"
export PRISM_MAINCLASS
prism "$@"
-
[$[Get Code]]
+
[$[Get Code]]

Then use:

-
+
sbml2prism sbml_file.xml > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

The following PRISM properties file will also be useful:

-
+
const double T;
const int c;

R{c}=? [I=T]
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -3860,11 +3876,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:

-
+
cd prism
java -cp classes prism.SBML2Prism sbml_file.xml 1000 > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

Alternatively, upper bounds can be modified manually after the translation process. @@ -3879,16 +3895,15 @@ prism "$@"

The format in which this information is input to the tool is exactly the same as is currently output (see the section "Exporting The Model" and the appendix "Explicit Model Files"). Presently, this functionality is only supported in the command-line version of the tool, using the -importtrans switch (and more convenient -importmodel; see below). -At the moment, PRISM makes no attempt to discern the model type from the input file. -By default it assumes that the model is an MDP. -If this is not the case, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. +PRISM makes some attempt to discern the model type from the format of the input files, +but if this does not work, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. For example:

-
+
prism -importtrans poll2.tra -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

Please note that this method of constructing models in PRISM is typically less efficient than using the PRISM language. @@ -3901,20 +3916,20 @@ The following example shows how PRISM could be used to build, export and then re (not a good strategy in general):

-
+
prism poll2.sm -exporttrans poll2.tra -exportstates poll2.sta
prism -importtrans poll2.tra -importstates poll2.sta -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

You can also import label information using the switch -importlabels, e.g.:

-
+
prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

where the labels file (poll2.lab above) is in the format generated by the -exportlabels export option of PRISM. @@ -3927,19 +3942,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.:

-
+
prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -importstaterewards poll2.srew -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

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:

-
+
prism -importmodel poll2.tra,sta,lab,srew -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

The contents of each file is determined by its extension: @@ -3952,10 +3967,10 @@ Possible file extensions are:

Use the extension .all to import from all of these files:

-
+
prism -importmodel poll2.all -ctmc
-
[$[Get Code]]
+
[$[Get Code]]



@@ -3975,31 +3990,31 @@ Possible file extensions are:

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

-
+
prism -help
-
[$[Get Code]]
+
[$[Get Code]]

For some switches, whose format is not straightforward, there is additional help available on the command-line, using -help switch. For example:

-
+
prism -help const
prism -help simpath
prism -help exportresults
prism -help exportmodel
-
[$[Get Code]]
+
[$[Get Code]]

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

-
+
prism -settings ~/.prism
-
[$[Get Code]]
+
[$[Get Code]]

In the following sections, we give a brief description of the most important configuration options available. @@ -4048,17 +4063,23 @@ 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.:

-
+
prism poll2.sm -tr 1000 -m
prism poll2.sm -tr 1000 -s
prism poll2.sm -tr 1000 -h
prism poll2.sm -tr 1000 -ex
-
[$[Get Code]]
+
[$[Get Code]]

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.

+

PRISM also has some basic support for automatically selecting the engine (and other settings) heuristically, +based on the size and type of the model, and the property being checked. +Use, for example, -heuristic speed from the command-line to choose options +which target computation speed rather than saving memory. +This is also available from the "Heuristic" option under the "PRISM" tab of the "Options" dialog in the GUI. +

Approximate/statistical model checking

Although it is not treated as a separate "engine", like those above, PRISM also provides approximate/statistical model checking, @@ -4191,19 +4212,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:

-
+
prism model.pm -pf "P=? [ G F x=1 ]" -ltl2datool hoa-ltl2dstar-for-prism -ltl2dasyntax lbt
-
[$[Get Code]]
+
[$[Get Code]]

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

-
+
#! /bin/bash
ltl2dstar --output=automaton --output-format=hoa "$1" "$2"
-
[$[Get Code]]
+
[$[Get Code]]

PRISM is known to work with these HOA-enabled tools: @@ -4267,10 +4288,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:

-
+
prism -cuddmaxmem 2g big_model.pm
-
[$[Get Code]]
+
[$[Get Code]]

Above, g denotes GB. You can also use m for MB. @@ -4281,22 +4302,22 @@ 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:

-
+
prism -javamaxmem 4g big_model.pm
xprism -javamaxmem 4g big_model.pm
-
[$[Get Code]]
+
[$[Get Code]]

each set the limit to 4GB. Alternatively, you set the environment variable PRISM_JAVAMAXMEM before running PRISM. For example, under a bash shell:

-
+
PRISM_JAVAMAXMEM=4g
export PRISM_JAVAMAXMEM
prism big_model.pm
-
[$[Get Code]]
+
[$[Get Code]]

If you get an error of the form java.lang.StackOverflowError, then you can try increasing the stack size of the JVM. @@ -4304,22 +4325,22 @@ On Unix, Linux or Mac OS X platforms, this can done by using the -javastac Examples are:

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

or:

-
+
PRISM_JAVASTACKSIZE=1g
export PRISM_JAVASTACKSIZE
prism big_model.pm
-
[$[Get Code]]
+
[$[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. @@ -4403,23 +4424,23 @@ If PRISM crashes or freezes whilst not using all/most of the available memory (y

If PRISM has already output this:

-
+
Building model...
-
[$[Get Code]]
+
[$[Get Code]]

but there is no line of the form:

-
+
Time for model construction: 34.3 seconds.
-
[$[Get Code]]
+
[$[Get Code]]

and then you get an error like this:

-
+
#
# An unexpected error has been detected by Java Runtime Environment:
#
@@ -4436,12 +4457,12 @@ If PRISM crashes or freezes whilst not using all/most of the available memory (y #
/home/dxp/bin/prism: line 50: 19298 Aborted "$PRISM_JAVA" #$PRISM_JAVAMAXMEM -Djava.awt.headless=$PRISM_HEADLESS -Djava.library.path=$PRISM_DIR/lib -classpath "$PRISM_CLASSPATH" $PRISM_MAINCLASS "$@"
-
[$[Get Code]]
+
[$[Get Code]]

or like this:

-
+
#
# An unexpected error has been detected by HotSpot Virtual Machine:
#
@@ -4453,7 +4474,7 @@ If PRISM crashes or freezes whilst not using all/most of the available memory (y #
...
-
[$[Get Code]]
+
[$[Get Code]]

then PRISM ran out of memory whilst trying to construct the model. @@ -4469,18 +4490,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

-
+
DD_MatrixMultiply: res is NULL
-
[$[Get Code]]
+
[$[Get Code]]

then it may be worth increasing the memory limit for CUDD (as described above). However, if you see an error more like this:

-
+
/home/dxp/bin/prism: line 50: 3139 Aborted "$PRISM_JAVA" $PRISM_JAVAMAXMEM -Djava.awt.headless=$PRISM_HEADLESS -Djava.library.path=$PRISM_DIR/lib -classpath "$PRISM_CLASSPATH" $PRISM_MAINCLASS "$@"
-
[$[Get Code]]
+
[$[Get Code]]

then increasing the memory CUDD probably will not help - PRISM is just trying to allocate more memory than is physically available on your system. @@ -4496,18 +4517,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:

-
+
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
-
[$[Get Code]]
+
[$[Get Code]]

or:

-
+
Exception in thread "main" java.lang.StackOverflowError
-
[$[Get Code]]
+
[$[Get Code]]

You can resolve this problem by increasing the memory allocated to Java. @@ -4554,7 +4575,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:

-
+
ctmc

const int k;
@@ -4577,7 +4598,7 @@ See the entry "Java memory" in the section "[$[Get Code]]
+
[$[Get Code]]

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. @@ -4596,6 +4617,7 @@ Below, we describe:

@@ -4606,7 +4628,7 @@ Below, we describe:

For the example PRISM model poll2.sm, the states file looks like:

-
+
(s,a,s1,s2)
0:(1,0,0,0)
1:(1,0,0,1)
@@ -4620,7 +4642,7 @@ Below, we describe: 9:(2,0,1,1)
10:(2,1,0,1)
11:(2,1,1,1)
-
[$[Get Code]]
+
[$[Get Code]]
@@ -4637,7 +4659,7 @@ Below, we describe:

Here is an example, for the (DTMC) PRISM model lec3.pm (which looks like this):

-
+
6 9
0 1 0.5
0 3 0.5
@@ -4648,13 +4670,13 @@ Below, we describe: 3 3 1
4 4 1
5 2 1
-
[$[Get Code]]
+
[$[Get Code]]

and here is one for the (CTMC) PRISM model poll2.sm (which looks like this):

-
+
12 22
0 1 0.5
0 2 0.5
@@ -4678,7 +4700,7 @@ Below, we describe: 10 0 1
10 11 0.5
11 2 1
-
[$[Get Code]]
+
[$[Get Code]]

MDPs (or PAs) @@ -4693,7 +4715,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):

-
+
4 5 7
0 0 1 1
1 0 0 0.7
@@ -4702,13 +4724,13 @@ To clarify terminology: each state of the MDP contains (nondeterministi 1 1 3 0.5
2 0 2 1
3 0 3 1
-
[$[Get Code]]
+
[$[Get Code]]

and here is an action-labelled version of the same model, lec12mdpa.nm (which looks like this):

-
+
4 5 7
0 0 1 1 a
1 0 2 0.5 c
@@ -4717,7 +4739,7 @@ To clarify terminology: each state of the MDP contains (nondeterministi 1 1 1 0.3 b
2 0 2 1 a
3 0 3 1 a
-
[$[Get Code]]
+
[$[Get Code]]
@@ -4728,7 +4750,7 @@ To clarify terminology: each state of the MDP contains (nondeterministi

Here is the result for the lec3.pm example from above (a DTMC):

-
+
6 9
0 0.5:1 0.5:3
1 0.5:0 0.25:2 0.25:4
@@ -4736,33 +4758,52 @@ To clarify terminology: each state of the MDP contains (nondeterministi 3 1:3
4 1:4
5 1:2
-
[$[Get Code]]
+
[$[Get Code]]

for the lec12mdp.nm example (an MDP):

-
+
4 5 7
0 1:1
1 0.7:0 0.3:1
1 0.5:2 0.5:3
2 1:2
3 1:3
-
[$[Get Code]]
+
[$[Get Code]]

and for the lec12mdpa.nm example (an MDP with actions):

-
+
4 5 7
0 1:1 a
1 0.5:2 0.5:3 c
1 0.7:0 0.3:1 b
2 1:2 a
3 1:3 a
-
[$[Get Code]]
+
[$[Get Code]]
+
+ +
+

+

Labels (.lab) files

+

These contain an explicit list of which labels are satisfied in each state. +The first line lists the labels, assigning each one an index. +The remaining lines list indices of all states satisfying one or more labels, +followed by a list of the the indices of labels that that are satisfied in it. +This includes the built-in labels "init" (initial states) and deadlock (deadlock states). +An example is shown below, where, for example, both "heads" and "end" are satisfied in state 2. +

+
+
+
0="init" 1="deadlock" 2="heads" 3="tails" 4="end"
+0: 0
+2: 2 4
+3: 3 4
+
[$[Get Code]]
@@ -4773,12 +4814,12 @@ To clarify terminology: each state of the MDP contains (nondeterministi

For the lec3.pm (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):

-
+
6 3
0 2
4 1
5 1
-
[$[Get Code]]
+
[$[Get Code]]
@@ -4790,25 +4831,25 @@ except that probabilities/rates are replaced with reward values, and the number

For the lec3.pm (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:

-
+
6 4
1 0 1
1 2 1
1 4 1
2 5 2
-
[$[Get Code]]
+
[$[Get Code]]

And or the lec12mdpa.nm (4-state) MDP example, we get non-zero transition rewards on 4 transitions:

-
+
4 5 4
1 0 2 6
1 0 3 6
1 1 0 5
1 1 1 5
-
[$[Get Code]]
+
[$[Get Code]]



diff --git a/manual/Main/Main.html b/manual/Main/Main.html index 8aa484d5..0053aa62 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.

Which version of PRISM does this manual describe?

-

This manual describes version 4.5. +

This manual describes version 4.6. In general, the online copy of the manual corresponds to the most recent publically available version of PRISM (including beta versions). diff --git a/manual/PropertySpecification/AllOnOnePage.html b/manual/PropertySpecification/AllOnOnePage.html index 560d7b67..61480ad2 100644 --- a/manual/PropertySpecification/AllOnOnePage.html +++ b/manual/PropertySpecification/AllOnOnePage.html @@ -770,8 +770,8 @@ the rewards associated with the model correspond to power consumption, the prope

- - + +
 FcosafeC<=tCI=tS
DTMCsSMHESMHESMHESMHESMHESMH-
CTMCsSMHESMHESMHESMHESMHESMH-
DTMCsSMHESMHESMHESMHESMHESMHE
CTMCsSMHESMHESMHESMHESMHESMHE
MDPsSM-ESMHES--E----SM-E----

Non-Probabilistic Properties

@@ -1158,7 +1158,7 @@ e.g. until (U) properties are allowed, as are cloc
[$[Get Code]]
-

This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons +

This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons (e.g. x<=5 is allowed, x<5 is not).

The digital clocks also has support for rewards: diff --git a/manual/PropertySpecification/PTAProperties.html b/manual/PropertySpecification/PTAProperties.html index 0cb861c6..d51c1cc3 100644 --- a/manual/PropertySpecification/PTAProperties.html +++ b/manual/PropertySpecification/PTAProperties.html @@ -124,7 +124,7 @@ e.g. until (U) properties are allowed, as are cloc

[$[Get Code]]
-

This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons +

This engine, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons (e.g. x<=5 is allowed, x<5 is not).

The digital clocks also has support for rewards: diff --git a/manual/PropertySpecification/Reward-basedProperties.html b/manual/PropertySpecification/Reward-basedProperties.html index 0c25e605..0ef544b4 100644 --- a/manual/PropertySpecification/Reward-basedProperties.html +++ b/manual/PropertySpecification/Reward-basedProperties.html @@ -306,8 +306,8 @@ the rewards associated with the model correspond to power consumption, the prope

- - + +
 FcosafeC<=tCI=tS
DTMCsSMHESMHESMHESMHESMHESMH-
CTMCsSMHESMHESMHESMHESMHESMH-
DTMCsSMHESMHESMHESMHESMHESMHE
CTMCsSMHESMHESMHESMHESMHESMHE
MDPsSM-ESMHES--E----SM-E----
diff --git a/manual/RunningPRISM/AllOnOnePage.html b/manual/RunningPRISM/AllOnOnePage.html index d6ed008c..77f01d19 100644 --- a/manual/RunningPRISM/AllOnOnePage.html +++ b/manual/RunningPRISM/AllOnOnePage.html @@ -218,7 +218,9 @@ Some screenshots of the GUI version of PRISM are shown below.

The PRISM GUI (model checking)

Loading And Building a Model

-

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the examples directory of the distribution. +

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the prism-examples directory of the distribution. +A few very small models are contained in the subdirectory simple; +the rest are in subdirectories grouped by model type.

The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error mIessage will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.

@@ -695,7 +697,7 @@ You can optionally request that state descriptions are added to each state of gr

Typically, once a model has been constructed, it is analysed through model checking. Properties are specified as described in the "Property Specification" section, and are usually kept in files with extensions .props, .pctl or .csl. -There are properties files accompanying most of the sample PRISM models in the examples directory. +There are properties files accompanying most of the sample PRISM models in the prism-examples directory.

GUI

@@ -749,15 +751,25 @@ For example, to check only the fourth property in the file:
[$[Get Code]]
-

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

You can also provide a comma-separated list of multiple properties to check, +using neither numerical indices or property names:

-
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
prism poll2.sm poll.csl -prop 4,5,safe
[$[Get Code]]
+

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

+
+
+
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
+
[$[Get Code]]
+
+

The switches -pctl and -csl are aliases for -pf.

Note the use of single quotes ('...') to avoid characters such as @@ -845,10 +857,10 @@ If, for a given property, statistical model checking results in one or more path

Statistical model checking can also be enabled from the command-line version of PRISM, by including the -sim switch. The default methods used are CI (Confidence Interval) for "quantitative" properties and SPRT (Sequential Probability Ratio Test) for "bounded" properties. To select a particular method, use switch -simmethod <method> where <method> is one of ci, aci, apmc and sprt. For example:

-
+
prism model.pm model.pctl -prop 1 -sim -simmethod aci
-
[$[Get Code]]
+
[$[Get Code]]

PRISM has default values for the various simulation method parameters, but these can also be specified using the switches -simsamples, -simconf, -simwidth and -simapprox. The exact meaning of these switches for each simulation method is given in the table below. @@ -877,19 +889,19 @@ time value for which you wish to compute probabilities. From the command-line, add the -steadystate (or -ss) switch:

-
+
prism poll2.sm -ss
-
[$[Get Code]]
+
[$[Get Code]]

for steady-state probabilities or the -transient (or -tr) switch:

-
+
prism poll2.sm -tr 2.0
-
[$[Get Code]]
+
[$[Get Code]]

for transient probabilities, again specifying a time value in the latter case. @@ -899,11 +911,11 @@ either on the screen (from the command-line) or in the log (from the GUI).

To instead export the vector of computed probabilities to a file, use the "Model | Compute/export" option from the GUI, or the -exportsteadystate (or -exportss) and -exporttransient (or -exporttr) switches from the command-line:

-
+
prism poll2.sm -ss -exportss poll2-ss.txt
prism poll2.sm -tr 2.0 -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

From the command-line, you can request that the probability vectors exported are in Matlab format by adding the -exportmatlab switch. @@ -915,30 +927,30 @@ an equiprobable choice over the set of initial states. You can override this and provide a specific initial distribution. This is done using the -importinitdist switch. The format for this imported distribution is identical to the ones exported by PRISM, i.e. simply a list of probabilities for all states separated by new lines. For example, this:

-
+
prism poll2.sm -tr 1.0 -exporttr poll2-tr1.txt
prism poll2.sm -tr 1.0 -importinitdist poll2-tr1.txt -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

is (essentially) equivalent to this:

-
+
prism poll2.sm -tr 2.0 -exporttr poll2-tr2.txt
-
[$[Get Code]]
+
[$[Get Code]]

Ranges of time values

Finally, you can compute transient probabilities for a range of time values, e.g.:

-
+
prism poll2.sm -tr 0.1:0.01:0.2
-
[$[Get Code]]
+
[$[Get Code]]

which computes transient probabilities for the time points 0.1, 0.11, 0.12, .., 0.2. In this case, the computation is done incrementally, with probabilities for each time point being computed from the previous point for efficiency. @@ -948,30 +960,30 @@ You can override this and provide a specific initial distribution. This is done This is done by leaving one or more constants undefined, e.g.:

-
+
const int N;
const double T;
-
[$[Get Code]]
+
[$[Get Code]]

This can be done for constants in the model file, the properties file, or both. Before any verification can be performed, values must be provided for any such constants. In the GUI, a dialog appears in which the user is required to enter values. From the command line, the -const switch must be used, e.g.:

-
+
prism cluster.sm cluster.csl -const N=4,T=85.9
-
[$[Get Code]]
+
[$[Get Code]]

To run an experiment, provide a range of values for one or more of the constants. Model checking will be performed for all combinations of the constant values provided. For example:

-
+
prism cluster.sm cluster.csl -const N=4:6,T=60:10:100
-
[$[Get Code]]
+
[$[Get Code]]

where N=4:6 means that values of 4,5 and 6 are used for N, @@ -981,10 +993,10 @@ and T=60:10:100 means that values of 60, 70, 80, 90 and 100 (i.e. s You can also specify double-valued constants as fractions rather than decimals. For example:

-
+
prism cluster.sm cluster.csl -const N=4,T=85.9 -const p=1/3
-
[$[Get Code]]
+
[$[Get Code]]

From the GUI, the same thing can be achieved by selecting a single property, @@ -1018,19 +1030,19 @@ or as code which can be used to generate the graph in Matlab.

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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt
-
[$[Get Code]]
+
[$[Get Code]]

to send to output file res.txt, or:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults stdout
-
[$[Get Code]]
+
[$[Get Code]]

to send the results straight to the screen. From the GUI, right click on the experiment and select "Export results". @@ -1038,7 +1050,7 @@ or as code which can be used to generate the graph in Matlab.

The default behaviour is to export a list of results in text form, using tabs to separate items. The above examples produce:

-
+
N       T       Result
4       0       0.0
4       10      4.707364688019771E-6
@@ -1046,20 +1058,20 @@ or as code which can be used to generate the graph in Matlab. 5       0       0.0
5       10      3.267731327728599E-6
5       20      8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:csv
-
[$[Get Code]]
+
[$[Get Code]]
-
+
N, T, Result
4, 0, 0.0
4, 10, 4.707364688019771E-6
@@ -1067,26 +1079,26 @@ or as code which can be used to generate the graph in Matlab. 5, 0, 0.0
5, 10, 3.267731327728599E-6
5, 20, 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

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.

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:csv,matrix
-
[$[Get Code]]
+
[$[Get Code]]
-
+
"N\T"
, 0.0, 10.0, 20.0
4, 0.0, 4.707364688019771E-6, 1.3126420636755292E-5
5, 0.0, 3.267731327728599E-6, 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]

The matrix option is also available in normal (non-CSV) mode. @@ -1094,14 +1106,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:

-
+
prism cluster.sm cluster.csl -prop 4 -const N=4:5,T=0:10:20 -exportresults res.txt:comment
-
[$[Get Code]]
+
[$[Get Code]]
-
+
// RESULT (N=4,T=0): 0.0
// RESULT (N=4,T=10): 4.707364688019771E-6
// RESULT (N=4,T=20): 1.3126420636755292E-5
@@ -1109,18 +1121,22 @@ This is particularly useful if you want to create a surface plot from results th // RESULT (N=5,T=10): 3.267731327728599E-6
// RESULT (N=5,T=20): 8.343575060356386E-6
-
[$[Get Code]]
+
[$[Get Code]]
-
+

A related option is the -exportvector <file> switch, useful in general contexts, not for experiments. +This exports the results for all states of the model +(typically, the log just displays the result for the initial state, unless a filter has been used) +to the the file file. +

Adversaries

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:

-
+
Pmax=? [ F "error" ]
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -1130,10 +1146,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.:

-
+
prism mdp.nm -pctl 'Pmax=? [ F "error" ]' -exportadv adv.tra -s
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -1158,7 +1174,7 @@ Secondly, each local state of a sequential component must be named. For exampl definition of these differs from the PEPA definition. Every PEPA synchronisation must have exactly one active component. Some examples of PEPA model descriptions which can be imported into PRISM -can be found in the examples/pepa directory. +can be found in the prism-examples/pepa directory.

From the command-line version of PRISM, add the -importpepa switch and the model will be treated as a PEPA description. From the GUI, select "Model | Open model" and then choose "PEPA models" @@ -1180,7 +1196,7 @@ by selecting menu option "Model | View | Parsed PRISM model".

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.

-
+
<?xml version="1.0" encoding="UTF-8"?>
<sbml xmlns="http://www.sbml.org/sbml/level2" metaid="_000000" level="2" version="1">
  <model id="nacl" name="Na+Cl">
@@ -1240,13 +1256,13 @@ by selecting menu option "Model | View | Parsed PRISM model".
  </model>
</sbml>
-
[$[Get Code]]
+
[$[Get Code]]

And here is the resulting PRISM code:

-
+
// File generated by automatic SBML-to-PRISM conversion
// Original SBML file: nacl.xml

@@ -1333,7 +1349,7 @@ by selecting menu option "Model | View | Parsed PRISM model". // 4
rewards "cl_minus" true : cl_minus; endrewards
-
[$[Get Code]]
+
[$[Get 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): @@ -1344,11 +1360,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.

-
+
cd prism
java -cp classes prism.SBML2Prism sbml_file.xml > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

If you are using a binary (rather than source code) distribution of PRISM, replace classes with lib/prism.jar in the above. @@ -1356,7 +1372,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:

-
+
#!/bin/sh

# Startup script for SBML-to-PRISM translator
@@ -1365,28 +1381,28 @@ by selecting menu option "Model | View | Parsed PRISM model". PRISM_MAINCLASS="prism.SBML2Prism"
export PRISM_MAINCLASS
prism "$@"
-
[$[Get Code]]
+
[$[Get Code]]

Then use:

-
+
sbml2prism sbml_file.xml > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

The following PRISM properties file will also be useful:

-
+
const double T;
const int c;

R{c}=? [I=T]
-
[$[Get Code]]
+
[$[Get Code]]

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. @@ -1403,11 +1419,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:

-
+
cd prism
java -cp classes prism.SBML2Prism sbml_file.xml 1000 > prism_file.sm
-
[$[Get Code]]
+
[$[Get Code]]

Alternatively, upper bounds can be modified manually after the translation process. @@ -1422,16 +1438,15 @@ prism "$@"

The format in which this information is input to the tool is exactly the same as is currently output (see the section "Exporting The Model" and the appendix "Explicit Model Files"). Presently, this functionality is only supported in the command-line version of the tool, using the -importtrans switch (and more convenient -importmodel; see below). -At the moment, PRISM makes no attempt to discern the model type from the input file. -By default it assumes that the model is an MDP. -If this is not the case, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. +PRISM makes some attempt to discern the model type from the format of the input files, +but if this does not work, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. For example:

-
+
prism -importtrans poll2.tra -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

Please note that this method of constructing models in PRISM is typically less efficient than using the PRISM language. @@ -1444,20 +1459,20 @@ The following example shows how PRISM could be used to build, export and then re (not a good strategy in general):

-
+
prism poll2.sm -exporttrans poll2.tra -exportstates poll2.sta
prism -importtrans poll2.tra -importstates poll2.sta -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

You can also import label information using the switch -importlabels, e.g.:

-
+
prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

where the labels file (poll2.lab above) is in the format generated by the -exportlabels export option of PRISM. @@ -1470,19 +1485,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.:

-
+
prism -importtrans poll2.tra -importstates poll2.sta -importlabels poll2.lab -importstaterewards poll2.srew -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

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:

-
+
prism -importmodel poll2.tra,sta,lab,srew -ctmc
-
[$[Get Code]]
+
[$[Get Code]]

The contents of each file is determined by its extension: @@ -1495,10 +1510,10 @@ Possible file extensions are:

Use the extension .all to import from all of these files:

-
+
prism -importmodel poll2.all -ctmc
-
[$[Get Code]]
+
[$[Get Code]]
diff --git a/manual/RunningPRISM/Experiments.html b/manual/RunningPRISM/Experiments.html index ddc3b526..9175d362 100644 --- a/manual/RunningPRISM/Experiments.html +++ b/manual/RunningPRISM/Experiments.html @@ -281,6 +281,11 @@ This is particularly useful if you want to create a surface plot from results th
[$[Get Code]]
+

A related option is the -exportvector <file> switch, useful in general contexts, not for experiments. +This exports the results for all states of the model +(typically, the log just displays the result for the initial state, unless a filter has been used) +to the the file file. +

diff --git a/manual/RunningPRISM/ExplicitModelImport.html b/manual/RunningPRISM/ExplicitModelImport.html index 0a864e3e..3de6b517 100644 --- a/manual/RunningPRISM/ExplicitModelImport.html +++ b/manual/RunningPRISM/ExplicitModelImport.html @@ -100,9 +100,8 @@ a.varlink { text-decoration:none; } The format in which this information is input to the tool is exactly the same as is currently output (see the section "Exporting The Model" and the appendix "Explicit Model Files"). Presently, this functionality is only supported in the command-line version of the tool, using the -importtrans switch (and more convenient -importmodel; see below). -At the moment, PRISM makes no attempt to discern the model type from the input file. -By default it assumes that the model is an MDP. -If this is not the case, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. +PRISM makes some attempt to discern the model type from the format of the input files, +but if this does not work, the model type can be overwritten using the -dtmc, -ctmc and -mdp switches. For example:

diff --git a/manual/RunningPRISM/LoadingAndBuildingAModel.html b/manual/RunningPRISM/LoadingAndBuildingAModel.html index 49314141..f097f131 100644 --- a/manual/RunningPRISM/LoadingAndBuildingAModel.html +++ b/manual/RunningPRISM/LoadingAndBuildingAModel.html @@ -96,7 +96,9 @@ a.varlink { text-decoration:none; }
-

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the examples directory of the distribution. +

Typically, when using PRISM, the first step is to load a model that has been specified in the PRISM modelling language. If using the GUI, select menu option "Model | Open Model" and choose a file. There are a selection of sample PRISM model files in the prism-examples directory of the distribution. +A few very small models are contained in the subdirectory simple; +the rest are in subdirectories grouped by model type.

The model will then be displayed in the editor in the "Model" tab of the GUI window. The file is parsed upon loading. If there are no errors, information about the modules, variables, and other components of the model is displayed in the panel to the left and a green tick will be visible. If there are errors in the file, a red cross will appear instead and the errors will be highlighted in the model editor. To view details of the error, position the mouse pointer over the source of the error (or over the red cross). Alternatively, select menu option "Model | Parse Model" and the error mIessage will be displayed in a message box. Model descriptions can, of course, also be typed from scratch into the GUI's editor.

diff --git a/manual/RunningPRISM/ModelChecking.html b/manual/RunningPRISM/ModelChecking.html index cec44900..72274c5f 100644 --- a/manual/RunningPRISM/ModelChecking.html +++ b/manual/RunningPRISM/ModelChecking.html @@ -99,7 +99,7 @@ a.varlink { text-decoration:none; }

Typically, once a model has been constructed, it is analysed through model checking. Properties are specified as described in the "Property Specification" section, and are usually kept in files with extensions .props, .pctl or .csl. -There are properties files accompanying most of the sample PRISM models in the examples directory. +There are properties files accompanying most of the sample PRISM models in the prism-examples directory.

GUI

@@ -153,15 +153,25 @@ For example, to check only the fourth property in the file:
[$[Get Code]]
-

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

You can also provide a comma-separated list of multiple properties to check, +using neither numerical indices or property names:

-
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
prism poll2.sm poll.csl -prop 4,5,safe
[$[Get Code]]
+

Alternatively, the contents of a properties file can be specified directly from the command-line, using the -pf switch: +

+
+
+
prism poll2.sm -pf 'P>=0.5 [ true U<=5 (s=1 & a=0) ]'
+
+
[$[Get Code]]
+
+

The switches -pctl and -csl are aliases for -pf.

Note the use of single quotes ('...') to avoid characters such as diff --git a/manual/RunningPRISM/SupportForPEPAModels.html b/manual/RunningPRISM/SupportForPEPAModels.html index 0dd88d18..dad9fee0 100644 --- a/manual/RunningPRISM/SupportForPEPAModels.html +++ b/manual/RunningPRISM/SupportForPEPAModels.html @@ -90,7 +90,7 @@ Secondly, each local state of a sequential component must be named. For exampl definition of these differs from the PEPA definition. Every PEPA synchronisation must have exactly one active component. Some examples of PEPA model descriptions which can be imported into PRISM -can be found in the examples/pepa directory. +can be found in the prism-examples/pepa directory.

From the command-line version of PRISM, add the -importpepa switch and the model will be treated as a PEPA description. From the GUI, select "Model | Open model" and then choose "PEPA models" diff --git a/manual/ThePRISMLanguage/AllOnOnePage.html b/manual/ThePRISMLanguage/AllOnOnePage.html index 74c57cea..a4744fb7 100644 --- a/manual/ThePRISMLanguage/AllOnOnePage.html +++ b/manual/ThePRISMLanguage/AllOnOnePage.html @@ -108,7 +108,7 @@ on the PRISM web site.

In this section, we describe the PRISM language and present a number of small illustrative examples. A precise definition of the semantics of the language is available from the "Documentation" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples. -A number of these are included with the tool distribution in the examples directory. +A number of these are included with the tool distribution in the prism-examples directory. Many additional examples can be found on the "Case Studies" section of the PRISM website.

The fundamental components of the PRISM language are modules and variables. @@ -539,12 +539,12 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo

Expressions can make use of several built-in functions:

-
  • 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. +
    • 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 (note, in a tie-break, we always round up, e.g. round(-1.5) gives -1 not -2) +
    • 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

    Examples of their usage are:

    @@ -735,7 +735,7 @@ secondly, they are written using quotation marks ("..."), as illust

    PTAs

    So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs. PRISM also supports a fourth: probabilistic timed automata (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of timed automata [AD94], by adding real-valued clocks which increase with time and can be reset. For background material on PTAs, see for example [NPS13]. -You can also find several example PTA models included in the PRISM distribution. Look in the examples/pta directory. +You can also find several example PTA models included in the PRISM distribution. Look in the prism-examples/ptas directory.

    Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:

    diff --git a/manual/ThePRISMLanguage/Expressions.html b/manual/ThePRISMLanguage/Expressions.html index 4be5b019..f9ebe22c 100644 --- a/manual/ThePRISMLanguage/Expressions.html +++ b/manual/ThePRISMLanguage/Expressions.html @@ -127,12 +127,12 @@ All expressions must evaluate correctly in terms of type (integer, double or Boo

    Expressions can make use of several built-in functions:

    -
    • 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. +
      • 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 (note, in a tie-break, we always round up, e.g. round(-1.5) gives -1 not -2) +
      • 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

      Examples of their usage are:

      diff --git a/manual/ThePRISMLanguage/Main.html b/manual/ThePRISMLanguage/Main.html index 470d7efa..52173950 100644 --- a/manual/ThePRISMLanguage/Main.html +++ b/manual/ThePRISMLanguage/Main.html @@ -111,7 +111,7 @@ on the PRISM web site.

      In this section, we describe the PRISM language and present a number of small illustrative examples. A precise definition of the semantics of the language is available from the "Documentation" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples. -A number of these are included with the tool distribution in the examples directory. +A number of these are included with the tool distribution in the prism-examples directory. Many additional examples can be found on the "Case Studies" section of the PRISM website.

      The fundamental components of the PRISM language are modules and variables. diff --git a/manual/ThePRISMLanguage/PTAs.html b/manual/ThePRISMLanguage/PTAs.html index 538279f3..4f0f6a31 100644 --- a/manual/ThePRISMLanguage/PTAs.html +++ b/manual/ThePRISMLanguage/PTAs.html @@ -98,7 +98,7 @@ a.varlink { text-decoration:none; }

      So far in this section, we have mainly focused on three types of models: DTMCs, MDPs and CTMCs. PRISM also supports a fourth: probabilistic timed automata (PTAs), which extend MDPs with the ability to model real-time behaviour. This is done in the style of timed automata [AD94], by adding real-valued clocks which increase with time and can be reset. For background material on PTAs, see for example [NPS13]. -You can also find several example PTA models included in the PRISM distribution. Look in the examples/pta directory. +You can also find several example PTA models included in the PRISM distribution. Look in the prism-examples/ptas directory.

      Before describing how PTA features are incorporated into the PRISM modelling language, we give a simple example. Here is a small PTA:

      diff --git a/manual/index.html b/manual/index.html index 6830b871..8d31e32b 100644 --- a/manual/index.html +++ b/manual/index.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.

      Which version of PRISM does this manual describe?

      -

      This manual describes version 4.5. +

      This manual describes version 4.6. In general, the online copy of the manual corresponds to the most recent publically available version of PRISM (including beta versions). diff --git a/manual/pub/skins/offline/css/prism.css b/manual/pub/skins/offline/css/prism.css index 29ac239e..2584fea7 100644 --- a/manual/pub/skins/offline/css/prism.css +++ b/manual/pub/skins/offline/css/prism.css @@ -486,3 +486,23 @@ a.prism-cite { color:#006600; } float:left; clear:both; } + +.prism-tag { + color:white; + background-color:grey; + border-radius:2px; + padding:2px; + margin-left:4px; + font-size:75%; +} + +div.prism-shell { + padding:5px 10px 5px 10px; + margin:10px 0 10px 0; + border:1px dotted #808080; + background-color:#F1F0ED; + overflow:auto; + font-family:monospace; + font-weight:bold; + font-size:90%; +}