JavaMOP 1.0 Past Time Linear Temporal Logic (JavaPTLTL) Plugin
This version of JavaMOP is old and not supported anymore! Go to the JavaMOP webpage for the latest version.
This is JavaMOP1.0, which is now deprecated. Go to JavaMOP for the current version.
|MOP Matrix: a clickable map of MOP pages.|
JavaPTLTL is an instance of the generic MOP PTLTL plugin for JavaMOP1.0, the MOP instance for Java. JavaMOP extracts from a specification using the header "logic = PTLTL" the actual PTLTL and passes it to the JavaPTLTL plugin. The JavaPTLTL plugin encapsulates the PTLTL plugin as follows:
- It sends the extracted PTLTL to the PTLTL plugin;
- It collects the output of the PTLTL plugin and produces Java monitoring code snippets (declarations, monitor initialization, monitor step, etc.).
JavaMOP takes the monitoring code snippets generated by the JavaPTLTL plugin and weaves them, using AspectJ, within the original application.
The syntax of JavaMOP PTLTL specifications is as expected:
<Logic> ::= "PTLTL"
<Property> ::= <PTLTL>
Run the JavaPTLTL Plugin Online
We provide a web-based interface to try JavaMOP with the JavaPTLTL plugin online. Enter your specification in the form below, or chose (and possibly modify) one of the existing specifications. Run JavaMOP by clicking the Run button. The generated code will be displayed underneath the form. The generated code can be compiled using any AspectJ compiler.
- Note: The name of the generated Aspect will be the name of the first specification in the text box + MonitorAspect. The name of the .aj file you intend to compile needs to be the same. For example, for LeakingSyncCFG, the generated aspect is LeakingSyncCFGMonitorAspect, and should be placed in a file named LeakingSncCFGMonitorAspect.aj.
- Note: One may append within or !within clauses to the event definitions in JavaMOP to control the scope of instrumentation. For example, if it is certain that some class C will not trigger any event of interest, one may use !within(C) in the event definitions to ignore C during the instrumentation, improving the instrumentation efficiency. The syntax of the within clause can be found in the AspectJ documentation.
Please press the Run button once and wait; it may take a few seconds to run JavaMOP1.0_PTLTL; the execution of JavaMOP1.0_PTLTL using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.