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 GUI. For more detailed instructions on how to read MoMoC's reachability graphs, please 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.

Where to get MoMoC

MoMoC is currently not part of the official Renew release. A version of Renew with MoMoC and some examples can be downloaded here:

​Download Renew with MoMoC

User Guide

Getting Started

After downloading, Renew can be started from within the folder with the command

java -jar loader.jar gui

This opens Renews GUI. MoMoC can be found under Tools > Modular Model Checker. This will open MoMoCs GUI, which is further described below. In the Examples folder, some exemplary reference net systems are provided to demonstrate the capabilities of MoMoC. All net templates must be opened and the root net instance (usually the net called System) must be selected /active.

Warning: MoMoC cannot verify unbounded nets and will run into an infinite loop when trying to do so!

User Interface

The following picture shows !MoMoC's GUI. It consists of three panels, arranged from left to right: The procedure panel, the user input panel and the procedure settings panel.

Procedure Panel: Lists all available procedures which can be selected by the user. Includes a short description of what the procedure does.

User Input Panel: The main text field Specification takes the formula that should be verified. For a better readability, macros can be entered in the text field above (q=term will replace all occurrences of q in the formula with term).

The buttons (from top to bottom) start the selected procedure, perform a syntax check on the entered formula and terminate all ongoing procedures.

Procedure Settings Panel: This panel is optional and shows additional parameters that can be set for the selected procedure.

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)
Other	InstancePredicate	m(Arg) Op Number	m(p3) <= 1
	Op	=, >, <, >=, <=
	Arg	[A-Za-z0-9]+
	Number	[0-9]+

Examples

AG (NOT DEADLOCK) : "On all paths, globally, not deadlock yields" (Deadlock-freedom)

(FIREABLE(T1) OR EX FIREABLE(NetA.T2)) : "Root net transition T1 is fireable (activated), or there exists a path on which in the next state a transition T2 of a net instance of net template NetA is fireable (activated)"

AG !(NetB, m(p1) >= 5) : "On all paths, globally, all net instances of net template NetB have at least 5 tokens on their place p1"

Why does the formula EG(m(p)=1) throw a syntax error?

m(p)=1 is not a valid atomic proposition. Because MoMoC is designed for reference nets, all predicates that refer to a place must be nested into a net instance quantifier to avoid ambiguity.

Atomic Propositions: Semantics

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

Fireable(T): True, iff the transition 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

The following images show exemplary result panels of the same query with opened reachability graphs. The left side of the result panel shows a hierarchical view of the normalized formula, the right side displays information that the procedure returned. Below the result panel is the according reachability graph. The nodes are colored with respect to the selected subformula in the result panel. In green nodes, the selected formula yields, while in red nodes it does not. The initial node is indicated by a strong red or green filling.

Developer Guide

A developer guide will follow.

Paper

At ​(internal filename: Willrodt+20.pdf ) you can find a contribution addressing MoMoC.

Further information (also a video of the talk at the workshop) can be found at ​PNSE'20 Workshop website