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 Reference nets 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 also be accessed through the MoMoC Plugin. For more detailed instructions on how to read MoMoC's reachability graphs, refer to RNRG.

The rest of this page is split into a user guide and a developer guide. As the names suggest, the user guide explains usage and features of the MoMoC plugin, whereas the developer guide is addressed to anyone who wants to extend the plugin.

User Guide

A detailed user guide will follow shortly.

User Interface

Net Instance Quantifier

Syntax

MoMoC follows the general syntax of CTL. The table below lists possible ways to write the boolean and temporal operators, as well as atomic propositions. The latter are further described below the table.

p and q are state formulas, f is a path formula.

Category	Name	Allowed Variations	Syntax
Boolean	True	TRUE, True
	False	FALSE, False
	Not	NOT, Not, ~, ¬	(Not p)
	And	AND, And, ∧	(p And q)
	Or	Or, OR, ∨	(p Or q)
Temporal	A	A, ALLPATH	Af
	E	E, EXPATH	Ef
	G	G, ALWAYS, [], GLOBAL	Gp
	F	F, EVENTUALLY, <>, FUTURE	Fp
	X	X, NEXTSTATE,O, NEXT	Xp
	U	U, UNTIL	(p U q)
Atomic	Deadlock	DEADLOCK
	Fireable	FIREABLE(Arg)	FIREABLE(T1)
	NetInstanceForall	!(Arg, InstancePredicate)	!(NetA, m(p1) > 0)
	NetInstanceExists	?(Arg, InstancePredicate)	?(NetB, m(p2) = 4)
	InstancePredicate	m(Arg) Op Number	m(p3) <= 1
	Op	=, >, <, >=, <=
	Arg	[A-Za-z0-9]+
	Number	[0-9]+

Examples

AG (NOT DEADLOCK)

(FIREABLE(T1) OR EX FIREABLE(T1))

AG !(Net1, m(p1) <= 5)

Atomic Propositions: Semantics

Deadlock: True, iff no transition is activated in a marking.

Fireable(T): True, iff T is activated in a marking. For root net transitions, it is sufficient to use the transition name as the parameter. For any other net instance, the syntax is NetName.TransitionName

NetInstanceForall: True, iff the instance predicate is true in all instances of the given type.

NetInstanceExists: True, iff the instance predicate is true in at least one instance of the given type.

InstancePredicate: True if the total number of tokens in a place fulfills the given expression. Does not distinguish between token types.

Results

Developer Guide

A detailed developer guide will follow shortly.