Changes between Version 8 and Version 9 of WikiStart


Ignore:
Timestamp:
Jun 17, 2008, 12:16:34 PM (11 years ago)
Author:
Christina Jansen
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • WikiStart

    v8 v9  
    3131 * Two algorithms for time- and reward bounded until-formulae. One is based on discretization [wiki:TijmsV_99 TijmsV_99], the other on uniformization and path truncation [wiki:QureshiS_ISFTC96 QureshiS_ISFTC96]. This includes state- and impulse rewards. For details on these algorithms we refer to [wiki:BaierHHK_ICALP00 BaierHHK_ICALP00], [wiki:ClothKKP_DSN05 ClothKKP_DSN05], [wiki:HaverkortCHKB_DSN02 HaverkortCHKB_DSN02].
    3232 * Safe on-the-fly steady-state detection for time-bounded reachability (see time bounded until operator of CSL logic). [wiki:KatoenZ_QEST06_pdf PDF] [wiki:KatoenZ_QEST06 BibTex]
    33  * Bisimulation minimisation for PCTL, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards. [wiki:KatoenKZJ_TACAS_pdf PDF] [wiki:KatoenKZJ_TACAS BibTex] 
     33 * Bisimulation minimisation for PCTL, CSL, PRCTL and CSRL logics, for the latter two in case without impulse rewards. [wiki:KatoenKZJ_TACAS_pdf PDF] [wiki:KatoenKZJ_TACAS BibTex]
    3434
    35 "[wiki:TracAdmin trac-admin] ''yourenvdir'' initenv" created
    36 a new Trac environment, containing a default set of wiki pages and some sample
    37 data. This newly created environment also contains
    38 [wiki:TracGuide documentation] to help you get started with your project.
     35== Getting MRMC models ==
     36MRMC models can be generated from [http://www.prismmodelchecker.org/ Prism] models, using the command line Prism starting from the version 3.0.
    3937
    40 You can use [wiki:TracAdmin trac-admin] to configure
    41 [http://trac.edgewall.org/ Trac] to better fit your project, especially in
    42 regard to ''components'', ''versions'' and ''milestones''.
     38The required options of "prism" are listed here and were obtained by running "prism -help":
    4339
     40 *''-exportmrmc .................... When exporting matrices/vectors/labels, use MRMC format''
    4441
    45 TracGuide is a good place to start.
     42 *''-exportlabels <file> ........... Export the list of labels and satisfying states to a file''
    4643
    47 Enjoy! [[BR]]
    48 ''The Trac Team''
     44 *''-exporttrans <file> ............ Export the transition matrix to a file''
    4945
    50 == Starting Points ==
     46 *''-exportstaterewards <file> ..... Export the state rewards vector to a file''
    5147
    52  * TracGuide --  Built-in Documentation
    53  * [http://trac.edgewall.org/ The Trac project] -- Trac Open Source Project
    54  * [http://trac.edgewall.org/wiki/TracFaq Trac FAQ] -- Frequently Asked Questions
    55  * TracSupport --  Trac Support
     48 *''-exporttransrewards <file> ...... Export the transition rewards matrix to a file''
    5649
    57 For a complete list of local wiki pages, see TitleIndex.
     50'''NOTE''': The "transition rewards" are what we refer to as "impulse rewards".
     51
     52A typical example of generating MRMC model from the Prism model would be:
     53
     54''$ prism model.sm model.csl -exportmrmc -exportlabels model.lab -exporttrans model.tra -exportstaterewards model.rew -exporttransrewards model.rewi''
     55
     56The resulting model.tra model.lab model.rew model.rewi files can be immediately consumed by MRMC.
     57
     58Some more information on generating MRMC models using Prism can be found [http://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel here].
     59