SPIN and Promela Hacks

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.

For more information on SPIN, see the NetLib SPIN archive.

patrick tullmann
Last updated on Wednesday, November 03, 2010