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
<p>This appendix details the (plain text) file formats used by PRISM for <aclass='wikilink' href='../RunningPRISM/ExportingTheModel.html'>exporting</a> and <aclass='wikilink' href='../RunningPRISM/ExplicitModelImport.html'>importing</a> models that have already been constructed, i.e., they comprise an explicit list of states, transitions, etc. making up the model, rather than a high-level model description in the <aclass='wikilink' href='../ThePRISMLanguage/Main.html'>PRISM modelling language</a>.
247
+
<p>This appendix details the plain text file formats used by PRISM for <aclass='wikilink' href='../RunningPRISM/ExportingTheModel.html'>exporting</a> and <aclass='wikilink' href='../RunningPRISM/ExplicitModelImport.html'>importing</a> models that have already been constructed, i.e., they comprise an explicit list of states, transitions, etc. making up the model, rather than a high-level model description in the <aclass='wikilink' href='../ThePRISMLanguage/Main.html'>PRISM modelling language</a>.
<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 (and, therefore, given PRISM's default behaviour, lexicographically according to the tuple of variable values).
260
-
</p>
261
-
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm.html'>poll2.sm</a>, the states file looks like:
<p>These contain an explicit list of the transitions making up a probabilistic model, i.e. they are essentially a sparse matrix representation of the transition probability/rate matrix. The first line of the file contains information about the size of the model, the remaining lines contain information about transitions, one per line.
@@ -294,7 +269,7 @@ <h1>Explicit Model Files</h1>
294
269
<pclass='vspace'>Here is an example, for the (DTMC) PRISM model <aclass='urllink' href='../uploads/lec3.pm'>lec3.pm</a> (which looks like <aclass='urllink' href='../uploads/lec3.dot.pdf'>this</a>):
<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>):
286
+
<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>):
<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.html'>lec12mdpa.nm</a> (which looks like <aclass='urllink' href='../uploads/lec12mdpa.dot.pdf'>this</a>):
<pclass='vspace'>The format of a <code>.tra</code> file for a POMDP is similar to an MDP,
359
+
but also contains information about observations.
360
+
</p>
361
+
<pclass='vspace'>The first line of the file take the form "<code>n c m o</code>", where <code>n</code>, <code>c</code> and <code>m</code> are, as for MDPs, the numbers of states, choices and transitions,
362
+
and <code>o</code> is the number of observations.
363
+
The lines that list transitions contain an additional integer after the transition probability
364
+
(and before the action, if present), giving the (deterministic) observation that is made
365
+
when entering the target state of that transition.
366
+
Currently, it is assumed that these are consistent for all states.
367
+
</p>
368
+
<pclass='vspace'>In order to also specify the observation for the initial state,
369
+
a dummy transition line of the form <code>- - s - o</code> is used,
370
+
giving both the initial state <code>s</code> and its observation <code>o</code>.
<p>There is alternative format for transition matrices (see the <aclass='wikilink' href='../RunningPRISM/ExportingTheModel.html#formats'>-exportrows</a>switch) where transitions for each state/choice are collated on a single line.
402
+
<p>There is alternative format for transition matrices (see the <aclass='wikilink' href='../RunningPRISM/ExportingTheModel.html#other'>rows</a>option for <code>-exportmodel</code>) where transitions for each state/choice are collated on a single line.
385
403
</p>
386
404
<pclass='vspace'>Here is the result for the <aclass='urllink' href='../uploads/lec3.pm'>lec3.pm</a> example from above (a DTMC):
387
405
</p>
@@ -500,6 +518,32 @@ <h1>Explicit Model Files</h1>
<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 (and, therefore, given PRISM's default behaviour, lexicographically according to the tuple of variable values).
525
+
</p>
526
+
<pclass='vspace'>For the example PRISM model <aclass='urllink' href='../uploads/poll2.sm'>poll2.sm</a>, the states file looks like:
0 commit comments