Changes between Version 13 and Version 14 of WikiStart


Ignore:
Timestamp:
Jun 18, 2008, 4:31:50 PM (10 years ago)
Author:
Dr. Ivan S. Zapreev
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v13 v14  
    5555
    5656== Getting MRMC models ==
    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].
     57MRMC models can be generated from [http://www.prismmodelchecker.org/ Prism]
     58models, using the command line Prism starting from the version 3.0.
     59For more information on generating MRMC models see [wiki:Specifications MRMC Manual].
    8060
    8161----