You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: manual/Appendices/AllOnOnePage.html
+7-7Lines changed: 7 additions & 7 deletions
Original file line number
Diff line number
Diff line change
@@ -124,7 +124,7 @@ <h1>Explicit Model Files</h1>
124
124
</p><h3>States (.sta) files</h3>
125
125
<p>These contain an explicit list of the reachable states of a model. The first line is of the form <code>(v1,...,vn)</code>, listing the names of all the variables in the model in the order that they appear in the PRISM model. Subsequent lines list the values of the <code>n</code> variables in each state of the model. Each line is of the form <code>i:(x1,...,xn)</code>, where <code>i</code> is the index of the state (starting from 0) and <code>x1,...,xn</code> are the values of each variable in the state. States are ordered by their index, or, equivalently, lexicographically according to the tuple of variable values.
126
126
</p>
127
-
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
127
+
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a>, the states file looks like:
<pclass='vspace'>and here is one for the (CTMC) PRISM model <aclass='urllink' href='../uploads/poll2.sm'>poll2.sm</a> (which looks like <aclass='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
175
+
<pclass='vspace'>and here is one for the (CTMC) PRISM model <aclass='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a> (which looks like <aclass='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
176
176
</p>
177
177
<divclass='vspace'></div>
178
178
<divclass='sourceblock ' id='sourceblock3'>
@@ -211,7 +211,7 @@ <h1>Explicit Model Files</h1>
211
211
</p>
212
212
<pclass='vspace'>Row/column state indices and choice indices are all zero-indexed. Probability values (as above) are written as (positive) floating point numbers and should sum to 1 for each choice. Often, the transition lines in the file are ordered by row index, then choice index and then column index, but this is optional.
213
213
</p>
214
-
<pclass='vspace'>Here is an example, for the (MDP) PRISM model <aclass='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
214
+
<pclass='vspace'>Here is an example, for the (MDP) PRISM model <aclass='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
<pclass='vspace'>and here is an action-labelled version of the same model, <aclass='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
229
+
<pclass='vspace'>and here is an action-labelled version of the same model, <aclass='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
<pclass='vspace'>And or the <aclass='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
342
+
<pclass='vspace'>And or the <aclass='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
Copy file name to clipboardExpand all lines: manual/Appendices/ExplicitModelFiles.html
+7-7Lines changed: 7 additions & 7 deletions
Original file line number
Diff line number
Diff line change
@@ -127,7 +127,7 @@
127
127
</p><h3>States (.sta) files</h3>
128
128
<p>These contain an explicit list of the reachable states of a model. The first line is of the form <code>(v1,...,vn)</code>, listing the names of all the variables in the model in the order that they appear in the PRISM model. Subsequent lines list the values of the <code>n</code> variables in each state of the model. Each line is of the form <code>i:(x1,...,xn)</code>, where <code>i</code> is the index of the state (starting from 0) and <code>x1,...,xn</code> are the values of each variable in the state. States are ordered by their index, or, equivalently, lexicographically according to the tuple of variable values.
129
129
</p>
130
-
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
130
+
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a>, the states file looks like:
<pclass='vspace'>and here is one for the (CTMC) PRISM model <aclass='urllink' href='../uploads/poll2.sm'>poll2.sm</a> (which looks like <aclass='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
178
+
<pclass='vspace'>and here is one for the (CTMC) PRISM model <aclass='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a> (which looks like <aclass='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
179
179
</p>
180
180
<divclass='vspace'></div>
181
181
<divclass='sourceblock ' id='sourceblock3'>
@@ -214,7 +214,7 @@
214
214
</p>
215
215
<pclass='vspace'>Row/column state indices and choice indices are all zero-indexed. Probability values (as above) are written as (positive) floating point numbers and should sum to 1 for each choice. Often, the transition lines in the file are ordered by row index, then choice index and then column index, but this is optional.
216
216
</p>
217
-
<pclass='vspace'>Here is an example, for the (MDP) PRISM model <aclass='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
217
+
<pclass='vspace'>Here is an example, for the (MDP) PRISM model <aclass='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
<pclass='vspace'>and here is an action-labelled version of the same model, <aclass='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
232
+
<pclass='vspace'>and here is an action-labelled version of the same model, <aclass='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
<pclass='vspace'>And or the <aclass='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
345
+
<pclass='vspace'>And or the <aclass='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
Copy file name to clipboardExpand all lines: manual/ConfiguringPRISM/AllOnOnePage.html
+2-2Lines changed: 2 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -259,8 +259,8 @@ <h3>Computation engines</h3>
259
259
</li></ul><pclass='vspace'>The default engine for PTAs is "stochastic games". The engine to be used can be specified using the "PTA model checking method" setting in the "PRISM" options panel in the GUI. From the command-line, switch <code>-ptamethod <name></code> should be used where <code><name></code> is either <code>games</code>, <code>digital</code> or <code>backwards</code>.
260
260
</p>
261
261
<pclass='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
262
-
the <aclass='wikilink' href='../ThePRISMLanguage/PTAs.html'>modelling language</a>
263
-
and the types of <aclass='wikilink' href='../PropertySpecification/PTAProperties.html'>properties</a> that can be checked.
262
+
the <aclass='wikilink' href='../ThePRISMLanguage/Real-timeModels.html'>modelling language</a>
263
+
and the types of <aclass='wikilink' href='../PropertySpecification/Real-timeModels.html'>properties</a> that can be checked.
264
264
</p><hr/>
265
265
<h1>Solution Methods and Options</h1>
266
266
<p>Separately from the choice of <aclass='wikilink' href='ComputationEngines.html'>engines</a>,
Copy file name to clipboardExpand all lines: manual/ConfiguringPRISM/ComputationEngines.html
+2-2Lines changed: 2 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -178,8 +178,8 @@ <h3>Computation engines</h3>
178
178
</li></ul><pclass='vspace'>The default engine for PTAs is "stochastic games". The engine to be used can be specified using the "PTA model checking method" setting in the "PRISM" options panel in the GUI. From the command-line, switch <code>-ptamethod <name></code> should be used where <code><name></code> is either <code>games</code>, <code>digital</code> or <code>backwards</code>.
179
179
</p>
180
180
<pclass='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
181
-
the <aclass='wikilink' href='../ThePRISMLanguage/PTAs.html'>modelling language</a>
182
-
and the types of <aclass='wikilink' href='../PropertySpecification/PTAProperties.html'>properties</a> that can be checked.
181
+
the <aclass='wikilink' href='../ThePRISMLanguage/Real-timeModels.html'>modelling language</a>
182
+
and the types of <aclass='wikilink' href='../PropertySpecification/Real-timeModels.html'>properties</a> that can be checked.
Copy file name to clipboardExpand all lines: manual/InstallingPRISM/AllOnOnePage.html
+5-2Lines changed: 5 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -94,9 +94,12 @@
94
94
<hr/>
95
95
<h1>Instructions</h1>
96
96
<h3>Prerequisites</h3>
97
-
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
97
+
<p>PRISM is known to run on Linux, Windows and Mac OS X, both 64-bit and 32-bit versions.
98
98
</p>
99
-
<pclass='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <aclass='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <aclass='urllink' href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
99
+
<pclass='vspace'>You will need <strong>Java</strong>, version 9 or above
100
+
(get it, for example from <aclass='urllink' href='https://jdk.java.net/'>Oracle</a>
101
+
or <aclass='urllink' href='https://adoptopenjdk.net/'>AdoptOpenJDK</a>).
102
+
To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
100
103
</p>
101
104
<pclass='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
Copy file name to clipboardExpand all lines: manual/InstallingPRISM/Main.html
+5-2Lines changed: 5 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -97,9 +97,12 @@
97
97
<!--PageText-->
98
98
<divid='wikitext'>
99
99
<h3>Prerequisites</h3>
100
-
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
100
+
<p>PRISM is known to run on Linux, Windows and Mac OS X, both 64-bit and 32-bit versions.
101
101
</p>
102
-
<pclass='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <aclass='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <aclass='urllink' href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
102
+
<pclass='vspace'>You will need <strong>Java</strong>, version 9 or above
103
+
(get it, for example from <aclass='urllink' href='https://jdk.java.net/'>Oracle</a>
104
+
or <aclass='urllink' href='https://adoptopenjdk.net/'>AdoptOpenJDK</a>).
105
+
To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
103
106
</p>
104
107
<pclass='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
0 commit comments