Skip to content

Commit

Permalink
Update manual.
Browse files Browse the repository at this point in the history
  • Loading branch information
@davexparker
davexparker committed Mar 19, 2021
1 parent eee992f commit 0c972a8
Show file tree
Hide file tree
Showing 57 changed files with 2,216 additions and 1,022 deletions.
14 changes: 7 additions & 7 deletions manual/Appendices/AllOnOnePage.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ <h1>Explicit Model Files</h1>
</p><h3>States (.sta) files</h3>
<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.
</p>
<p class='vspace'>For the example PRISM model <a class='urllink' href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
<p class='vspace'>For the example PRISM model <a class='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a>, the states file looks like:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
Expand Down Expand Up @@ -172,7 +172,7 @@ <h1>Explicit Model Files</h1>
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/AllOnOnePage?action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and here is one for the (CTMC) PRISM model <a class='urllink' href='../uploads/poll2.sm'>poll2.sm</a> (which looks like <a class='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
<p class='vspace'>and here is one for the (CTMC) PRISM model <a class='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a> (which looks like <a class='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
Expand Down Expand Up @@ -211,7 +211,7 @@ <h1>Explicit Model Files</h1>
</p>
<p class='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.
</p>
<p class='vspace'>Here is an example, for the (MDP) PRISM model <a class='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
<p class='vspace'>Here is an example, for the (MDP) PRISM model <a class='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
Expand All @@ -226,7 +226,7 @@ <h1>Explicit Model Files</h1>
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/AllOnOnePage?action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and here is an action-labelled version of the same model, <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
<p class='vspace'>and here is an action-labelled version of the same model, <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
Expand Down Expand Up @@ -260,7 +260,7 @@ <h1>Explicit Model Files</h1>
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/AllOnOnePage?action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>for the <a class='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> example (an MDP):
<p class='vspace'>for the <a class='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> example (an MDP):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
Expand All @@ -273,7 +273,7 @@ <h1>Explicit Model Files</h1>
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/AllOnOnePage?action=sourceblock&amp;num=7' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and for the <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> example (an MDP with actions):
<p class='vspace'>and for the <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> example (an MDP with actions):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
Expand Down Expand Up @@ -339,7 +339,7 @@ <h1>Explicit Model Files</h1>
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/AllOnOnePage?action=sourceblock&amp;num=11' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>And or the <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
<p class='vspace'>And or the <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock12'>
Expand Down
14 changes: 7 additions & 7 deletions manual/Appendices/ExplicitModelFiles.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@
</p><h3>States (.sta) files</h3>
<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.
</p>
<p class='vspace'>For the example PRISM model <a class='urllink' href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
<p class='vspace'>For the example PRISM model <a class='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a>, the states file looks like:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
Expand Down Expand Up @@ -175,7 +175,7 @@
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles?action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and here is one for the (CTMC) PRISM model <a class='urllink' href='../uploads/poll2.sm'>poll2.sm</a> (which looks like <a class='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
<p class='vspace'>and here is one for the (CTMC) PRISM model <a class='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a> (which looks like <a class='urllink' href='../uploads/poll2.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
Expand Down Expand Up @@ -214,7 +214,7 @@
</p>
<p class='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.
</p>
<p class='vspace'>Here is an example, for the (MDP) PRISM model <a class='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
<p class='vspace'>Here is an example, for the (MDP) PRISM model <a class='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdp.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
Expand All @@ -229,7 +229,7 @@
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles?action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and here is an action-labelled version of the same model, <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
<p class='vspace'>and here is an action-labelled version of the same model, <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (which looks like <a class='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
Expand Down Expand Up @@ -263,7 +263,7 @@
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles?action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>for the <a class='urllink' href='../uploads/lec12mdp.nm'>lec12mdp.nm</a> example (an MDP):
<p class='vspace'>for the <a class='urllink' href='../uploads/lec12mdp.nm.html'>lec12mdp.nm</a> example (an MDP):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
Expand All @@ -276,7 +276,7 @@
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles?action=sourceblock&amp;num=7' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and for the <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> example (an MDP with actions):
<p class='vspace'>and for the <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> example (an MDP with actions):
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
Expand Down Expand Up @@ -342,7 +342,7 @@
<div class='sourceblocklink'><a href='http://www.prismmodelchecker.org/manual/Appendices/ExplicitModelFiles?action=sourceblock&amp;num=11' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>And or the <a class='urllink' href='../uploads/lec12mdpa.nm'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
<p class='vspace'>And or the <a class='urllink' href='../uploads/lec12mdpa.nm.html'>lec12mdpa.nm</a> (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock12'>
Expand Down
4 changes: 2 additions & 2 deletions manual/ConfiguringPRISM/AllOnOnePage.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -259,8 +259,8 @@ <h3>Computation engines</h3>
</li></ul><p class='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 &lt;name&gt;</code> should be used where <code>&lt;name&gt;</code> is either <code>games</code>, <code>digital</code> or <code>backwards</code>.
</p>
<p class='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
the <a class='wikilink' href='../ThePRISMLanguage/PTAs.html'>modelling language</a>
and the types of <a class='wikilink' href='../PropertySpecification/PTAProperties.html'>properties</a> that can be checked.
the <a class='wikilink' href='../ThePRISMLanguage/Real-timeModels.html'>modelling language</a>
and the types of <a class='wikilink' href='../PropertySpecification/Real-timeModels.html'>properties</a> that can be checked.
</p><hr />
<h1>Solution Methods and Options</h1>
<p>Separately from the choice of <a class='wikilink' href='ComputationEngines.html'>engines</a>,
Expand Down
4 changes: 2 additions & 2 deletions manual/ConfiguringPRISM/ComputationEngines.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,8 +178,8 @@ <h3>Computation engines</h3>
</li></ul><p class='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 &lt;name&gt;</code> should be used where <code>&lt;name&gt;</code> is either <code>games</code>, <code>digital</code> or <code>backwards</code>.
</p>
<p class='vspace'>The choice of engine for PTA model checking affects restrictions that imposed on both
the <a class='wikilink' href='../ThePRISMLanguage/PTAs.html'>modelling language</a>
and the types of <a class='wikilink' href='../PropertySpecification/PTAProperties.html'>properties</a> that can be checked.
the <a class='wikilink' href='../ThePRISMLanguage/Real-timeModels.html'>modelling language</a>
and the types of <a class='wikilink' href='../PropertySpecification/Real-timeModels.html'>properties</a> that can be checked.
</p>
</div>

Expand Down
7 changes: 5 additions & 2 deletions manual/InstallingPRISM/AllOnOnePage.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,9 +94,12 @@
<hr />
<h1>Instructions</h1>
<h3>Prerequisites</h3>
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
<p>PRISM is known to run on Linux, Windows and Mac OS X, both 64-bit and 32-bit versions.
</p>
<p class='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <a class='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <a class='urllink' href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
<p class='vspace'>You will need <strong>Java</strong>, version 9 or above
(get it, for example from <a class='urllink' href='https://jdk.java.net/'>Oracle</a>
or <a class='urllink' href='https://adoptopenjdk.net/'>AdoptOpenJDK</a>).
To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
</p>
<p class='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
</p>
Expand Down
7 changes: 5 additions & 2 deletions manual/InstallingPRISM/Main.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,12 @@
<!--PageText-->
<div id='wikitext'>
<h3>Prerequisites</h3>
<p>PRISM is known to run on Linux, Windows and Mac OS X, including 64-bit variants of these operating systems.
<p>PRISM is known to run on Linux, Windows and Mac OS X, both 64-bit and 32-bit versions.
</p>
<p class='vspace'>You will need <strong>Java</strong>, version 8 or above. The tool is known to compile and run with both the <a class='urllink' href='http://www.oracle.com/technetwork/java/javase/downloads/index.html'>Oracle</a> and <a class='urllink' href='http://openjdk.java.net/'>OpenJDK</a> versions of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
<p class='vspace'>You will need <strong>Java</strong>, version 9 or above
(get it, for example from <a class='urllink' href='https://jdk.java.net/'>Oracle</a>
or <a class='urllink' href='https://adoptopenjdk.net/'>AdoptOpenJDK</a>).
To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK).
</p>
<p class='vspace'>To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information:
</p>
Expand Down
Loading

0 comments on commit 0c972a8

Please sign in to comment.