PRISM - Symmetry Reduction
Here you can find details about the prototype implementation of symmetry reduction in PRISM,
as described in our CAV'06 paper [KNP06a].
Examples
Below are links to the files and web pages for the 4 examples used in the paper.
Each directory contains PRISM files for both the models and the properties used
plus a script showing the options/switches used for PRISM.
- IEEE 802.3 CSMA/CD communication protocol (files, web page)
- Aspnes and Helihy's randomised consensus protocol (files, web page)
- Cachin/Kursawe/Shoup's randomised Byzantine agreement protocol (files, web page)
- simple peer-to-peer (P2P) protocol based on BitTorrent (files, web page)
Alternatively, download all examples files here: all.tar.gz.
Code
You can experiment with the prototype implementation by following the instructions below.
- Download an up-to-date source code distrbution of the development version of PRISM (the patch included here is against version 3.2)
- Download the 3 files below and copy them into the src/prism directory of the PRISM distribution, overwriting the originals:
(Or, if you prefer, use this patch.)
- Build PRISM as normal (see instructions).
- Run PRISM as normal but with the additional switch -symm <before> <after> where
<before> and <after> are the number of modules in the PRISM model file before and after the block of symmetric modules. For example:
- cd csma
- prism -h csma4.nm csma4.pctl -prop 1 -symm 1 0
Important notes
Please remember:
- PRISM-symm requires models to be fully symmetric (i.e. all of the symmetric processes are indistinguishable).
- PRISM-symm assumes, but does not check, that your model is symmetric. If it is not, you may get unpredictable results.
Contact
If you have any problems, questions or comments about any of these, please
contact us.
