MMCsp is a compiler from a simple probabilistic pi-calculus to PRISM models. It is built on XSB, a tabled logic programming system, and generates the symbolic semantic representation of a probabilistic pi-calculus term in text. A separate Java program then translates this semantic representation into a probabilistic model for PRISM.
The tool was developed under the collaboration between teams Comete (Laboratoire d'Informatique de l'Ecole Polytechnique, LIX) and PRISM (Oxford University Computing Laboratory) under an INRIA/ARC Project ProNobis.
The source code is free to download.
- To install MMCsp, please install XSB first. Then, unzip the source code and run "install.sh".
- Dining Cryptographers Problem (under directories "Examples\probdcp2" and "Examples\probdcp3")
- Partial Secret Exchange algorithm (under directory "Examples\pse")
- To run these examples, type "make" under each of the above directories.