MOP Logic Repository 3

	MOP
		FSM	ERE	CFG	PTLTL	LTL	PTCaRet	SRS	...
	JavaMOP	JavaFSM	JavaERE	JavaCFG	JavaPTLTL	JavaLTL	JavaPTCaRet	JavaSRS	...
	BusMOP	BusFSM	BusERE	...	BusPTLTL	...	...	...	...
	...	...	...	...	...	...	...	...	...
	MOP Matrix: a clickable map of MOP pages.

The Logic Repository is a framework for managing logic plugins. It aims to provide a clear separation between monitor generation and language specific implementation. Instances of MOP use the Logic Repository to retrieve a monitor from an input property. The Logic Repository also provides an easy environment for logic plugin development.

Logic plugins implement and encapsulate monitor synthesis algorithms for particular requirements specification formalisms. While they are a core feature of MOP, logic plugins can be used in various other monitoring applications. Below is a list containing our current logic plugins. Each plugin can be experimented with online before download.

• FSM -- Finite State Machines
• ERE -- Extended Regular Expressions
• CFG -- Context Free Grammars
• PTLTL -- Past Time Linear Temporal Logic
• LTL -- Linear Temporal Logic
• PTCaRet -- Past Time LTL with Calls and Returns

Below you can run Logic Repository online. If you want to download the source code or if you want to interact with developers, please visit JavaMOP Development Page and comments can be sent to mop@cs.uiuc.edu.

Run the Logic Repository Online

Enter your specification or chose (and modify) one example from the menu - provided examples are also reachable from the individual logic plugin pages, via the MOP matrix above. Click Run to run the Logic Repository on the selected example. The generated monitor can be used by any instance of MOP, or possibly other tools;