Difference between revisions of "MOP Logic Repository"
| Line 1: | Line 1: | ||
| − | MOP provides an extensible logic framework | + | [[MOP]] provides an extensible logic framework, allowing the user to add her/his favariate or domain-specific specification formalisms via '''''logic plugins'''''. A logic plugin encodes monitor synthesis algorithm for a logic formalism, usually composed of a language-specific shell and a language-independent logic engine. But the logic engine may not be always needed as some specification formalisms can be specific to a programming language, for instance, JML and Jass. Here we provide a repository of the logic plugins via which the user can learn and try the logic plugins online. |
Currently, the following specification formalisms are supported: | Currently, the following specification formalisms are supported: | ||
| Line 6: | Line 6: | ||
* [[Past Time Linear Temporal Logic]] (PTLTL) | * [[Past Time Linear Temporal Logic]] (PTLTL) | ||
| − | == | + | == Send us Your Logic! == |
Currently, we only accept new logic plugins via emails. In order to provide a logic plugin, please pack the whole plugin directory into one file and send it to fsl AT cs.uiuc.edu. In order for us to better test the submitted plugin, please put related information into a readme file. After we verify the plugin, we will publish it in our repository. | Currently, we only accept new logic plugins via emails. In order to provide a logic plugin, please pack the whole plugin directory into one file and send it to fsl AT cs.uiuc.edu. In order for us to better test the submitted plugin, please put related information into a readme file. After we verify the plugin, we will publish it in our repository. | ||
Revision as of 02:26, 24 October 2006
MOP provides an extensible logic framework, allowing the user to add her/his favariate or domain-specific specification formalisms via logic plugins. A logic plugin encodes monitor synthesis algorithm for a logic formalism, usually composed of a language-specific shell and a language-independent logic engine. But the logic engine may not be always needed as some specification formalisms can be specific to a programming language, for instance, JML and Jass. Here we provide a repository of the logic plugins via which the user can learn and try the logic plugins online.
Currently, the following specification formalisms are supported:
- Extended Regular Expression (ERE)
- Future Time Linear Temporal Logic (FTLTL)
- Past Time Linear Temporal Logic (PTLTL)
Send us Your Logic!
Currently, we only accept new logic plugins via emails. In order to provide a logic plugin, please pack the whole plugin directory into one file and send it to fsl AT cs.uiuc.edu. In order for us to better test the submitted plugin, please put related information into a readme file. After we verify the plugin, we will publish it in our repository.
