(s,a,s1,s2)
0:(1,0,0,0)
1:(1,0,0,1)
2:(1,0,1,0)
3:(1,0,1,1)
4:(1,1,1,0)
5:(1,1,1,1)
6:(2,0,0,0)
7:(2,0,0,1)
8:(2,0,1,0)
9:(2,0,1,1)
10:(2,1,0,1)
11:(2,1,1,1)
This appendix details the (plain text) file formats used by PRISM for exporting and importing 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 PRISM modelling language. Below, we describe:
These contain an explicit list of the reachable states of a model. The first line is of the form (v1,...,vn), 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 n variables in each state of the model. Each line is of the form i:(x1,...,xn), where i is the index of the state (starting from 0) and x1,...,xn 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.
For the example PRISM model poll2.sm, the states file looks like:
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.
DTMCs and CTMCs
For Markov chains the first line take the form "n m", giving the number of states (n) and the number of transitions (m). The remaining lines are of the form "i j x", where i and j are the row (source) and column (destination) indices of the transition, and x is the probability (for a DTMC) or rate (for a CTMC) of the transition. Row/column state indices are zero-indexed (i.e. between 0 and n-1). Probability/rate values are written as (positive) floating point numbers (examples: 0.5, .5, 5.6e-6, 1).
Often, the transition lines in the file are ordered by row index and then column index, but this is optional. For a DTMC, the probabilities for the outgoing transitions of each state should sum to 1.
Here is an example, for the (DTMC) PRISM model lec3.pm (which looks like this):
and here is one for the (CTMC) PRISM model poll2.sm (which looks like this):
MDPs (or PAs)
For MDPs, the format is an extension of the above To clarify terminology: each state of the MDP contains (nondeterministic) choices, each of which is essentially a probability distribution over successor states that we can view as a set of transitions. Optionally, each choice can be labelled with an action.
The first line of the file take the form "n c m", giving the number of states (n), the total number of choices (c) and the total number of transitions (m). The remaining lines are of the form "i k j x" or "i k j x a", where i and j are the row (source) and column (destination) indices of the transition, k is the index of the choice that it belongs to, and x is the probability of the transition. a is optional and gives the action label for the choice of the transition. Action labels can be present for some, all or no states but, in slightly redundant fashion, the action labels, if present, must be the same for all transitions belonging to the same choice.
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.
Here is an example, for the (MDP) PRISM model lec12mdp.nm (which looks like this):
and here is an action-labelled version of the same model, lec12mdpa.nm (which looks like this):
There is alternative format for transition matrices (see the -exportrows switch) where transitions for each state/choice are collated on a single line.
Here is the result for the lec3.pm example from above (a DTMC):
for the lec12mdp.nm example (an MDP):
and for the lec12mdpa.nm example (an MDP with actions):
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.
Reward files contain an (optional) header, giving the name of the reward structure that generated it
and the type of rewards (state or transitions) stored in the file.
For state rewards, the information following this header is an explicit list of the (non-zero) state rewards.
The first line is of the form n m where n is the number of states in the model and m is the number of non-zero state rewards.
The following m lines are of the form i r, denoting that the state reward for state i is r.
For the lec3.pm (6-state) DTMC example from above, we get rewards in 3 states (0, 4 and 5):
Files containing transition rewards, like those for state rewards, start with an (optional) header. The rest of the file is formatted identically to transitions files (see above), except that probabilities/rates are replaced with reward values, and the number of transitions (the last number on the first line) is replaced with the number of non-zero transition rewards.
For the lec3.pm (6-state) DTMC example from above, we get non-zero transition rewards on 4 transitions:
And or the lec12mdpa.nm (4-state) MDP example, we get non-zero transition rewards on 4 transitions:
Site hosted at the Department of Computer Science, University of Oxford