Loading src/prism-converter/README.md 0 → 100644 +37 −0 Original line number Diff line number Diff line # Prism converter This directory containers a helper program called `prism-converter` that converts transition matrices of PRISM[1] models into coalgebra specifications. ## Building ```sh stack build --flag copar:benchmark-generators ``` ## Generating transition matrices You can generate those transition matrices with PRISM itself by using: ```sh prism -exporttrans TRA_FILE -exportstates STA_FILE -const CONST_ASSIGNMENTS ``` Given the constant assignments `CONST_ASSIGNMENTS` (see the PRISM documentation on syntax and semantics of those), thsi output a transition matrix in `TRA_FILE` and a states file in `STA_FILE`. Please see [2] for additional details. ## Converting them into coalgebra specs The resulting files can then be converted into a coalgebra specification using ```sh stack exec prism-converter -- --model-type TYPE --states-file STA_FILE TRA_FILE ``` where type is one of dtmc, ctmc or mdp. See `stack exec prism-converter -- --help` for details. [1]: https://www.prismmodelchecker.org [2]: https://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel Loading
src/prism-converter/README.md 0 → 100644 +37 −0 Original line number Diff line number Diff line # Prism converter This directory containers a helper program called `prism-converter` that converts transition matrices of PRISM[1] models into coalgebra specifications. ## Building ```sh stack build --flag copar:benchmark-generators ``` ## Generating transition matrices You can generate those transition matrices with PRISM itself by using: ```sh prism -exporttrans TRA_FILE -exportstates STA_FILE -const CONST_ASSIGNMENTS ``` Given the constant assignments `CONST_ASSIGNMENTS` (see the PRISM documentation on syntax and semantics of those), thsi output a transition matrix in `TRA_FILE` and a states file in `STA_FILE`. Please see [2] for additional details. ## Converting them into coalgebra specs The resulting files can then be converted into a coalgebra specification using ```sh stack exec prism-converter -- --model-type TYPE --states-file STA_FILE TRA_FILE ``` where type is one of dtmc, ctmc or mdp. See `stack exec prism-converter -- --help` for details. [1]: https://www.prismmodelchecker.org [2]: https://www.prismmodelchecker.org/manual/RunningPRISM/ExportingTheModel