MoMoC - A Modular Model Checker

The MoMoC Plugin is a modular model-checking tool designed to be able to verify all formalism that Renew can simulate, most notably including the Reference net formalism. Currently, MoMoC can verify CTL formulas on Referencenets and thus also on CPNs and P/T-Nets. It also features an interactive result visualisation for label based model checking approaches such as CTL model checking.

MoMoC is implemented in several modules (thus its name) and each can quickly be exchanged to alter the behaviour of the plugin. This makes it easy to test out new algorithms or data-structures, as only the corresponding module needs to be replaced.

The foundation of MoMoC is the RNRG plugin, whose key functionality (creating a reachability graph) can be accessed through the MoMoC Plugin.

User Guide

A detailed user guide will follow shortly.

Developer Guide

A detailed developer guide will follow shortly.