In the process of using SPIN to model the IPC system of a research microkernel here at Utah, we developed several tools to help with SPIN and Promela. (Well, tools is a strong word, perhaps hacks is a better word.)

Note that this code was written in 1996 for an old version of Promela. Things have changed a lot since then, so I wouldn't expect too much from this code.

• promela.el: An emacs promela mode. I developed this under Xemacs, but it should also work in FSF emacs. Its a lame hack and does little more than fontification and really poor auto-indentation. But, you do get a neat little "(Promela)" down on the modeline.
• prMunge: A Perl script that transforms a CPP processed promela file. It reformats its input to optimize line breaks.
• dumpMunge: A Perl script that takes the result of a spin -a dump and reformats it. It looks more like the Xspin trace after processing.

patrick tullmann
Last updated on Wednesday, November 03, 2010