| 57 | | MRMC models can be generated from [http://www.prismmodelchecker.org/ Prism] models, using the command line Prism starting from the version 3.0. |
| 58 | | |
| 59 | | The required options of "prism" are listed here and were obtained by running "prism -help": |
| 60 | | |
| 61 | | *''-exportmrmc .................... When exporting matrices/vectors/labels, use MRMC format'' |
| 62 | | |
| 63 | | *''-exportlabels <file> ........... Export the list of labels and satisfying states to a file'' |
| 64 | | |
| 65 | | *''-exporttrans <file> ............ Export the transition matrix to a file'' |
| 66 | | |
| 67 | | *''-exportstaterewards <file> ..... Export the state rewards vector to a file'' |
| 68 | | |
| 69 | | *''-exporttransrewards <file> ...... Export the transition rewards matrix to a file'' |
| 70 | | |
| 71 | | '''NOTE''': The "transition rewards" are what we refer to as "impulse rewards". |
| 72 | | |
| 73 | | A typical example of generating MRMC model from the Prism model would be: |
| 74 | | |
| 75 | | ''$ prism model.sm model.csl -exportmrmc -exportlabels model.lab -exporttrans model.tra -exportstaterewards model.rew -exporttransrewards model.rewi'' |
| 76 | | |
| 77 | | The resulting model.tra model.lab model.rew model.rewi files can be immediately consumed by MRMC. |
| 78 | | |
| 79 | | Some more information on generating MRMC models using Prism can be found [http://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel here]. |
| | 57 | MRMC models can be generated from [http://www.prismmodelchecker.org/ Prism] |
| | 58 | models, using the command line Prism starting from the version 3.0. |
| | 59 | For more information on generating MRMC models see [wiki:Specifications MRMC Manual]. |
