Mole - A Petri Net Unfolder

Overview

This program implements the Esparza/Römer/Vogler unfolding algorithm for low-level Petri nets. It is designed to be compatible with the tools in the PEP project and with the Model-Checking Kit - its input is a low level Petri net in PEP's ll_net format, and its output is the resulting unfolding in the mci format also used in the PEP tools.

This tool represents an overhaul of Stefan Römer's ERVunfold tool (which, in turn, is an enhancement of the EVunfold tool available in PEP). It is much smaller and does not have the vast set of options that ERVunfold has; in exchange, this tool is usually somewhat faster than ERVunfold. More information can be found in the Readme file.

Downloads

Source code (April 28, 2014)

Related Tools

Cunf - unfolding tool for Petri nets with read arcs, by César Rodríguez
Tours - prototype tool, based on Mole, for test-case generation, by Konstantinos Athanasiou and Hernán Ponce-De-Léon

Related Publications

K. Athanasiou, H. Ponce de Léon, S. Schwoon. Test Case Generation for Concurrent Systems Using Event Structures. In TAP'15, to appear.
Th. Chatain, S. Haar, L. Jezequel, L. Paulevé and S. Schwoon. Characterization of Reachable Attractors Using Petri Net Unfoldings. In CMSB'14, LNBI 8859, pages 129-142. Springer-Verlag, 2014. ( PDF | BibTeX + Abstract )
S. Haar, C. Kern and S. Schwoon. Computing the Reveals Relation in Occurrence Nets. Theoretical Computer Science 493, pages 66-79, 2013. ( PDF | BibTeX + Abstract )

Contact

Please direct questions to Stefan Schwoon.