JavaMOP and RVMonitor Usage

Prerequisite

Scala

You can obtain scala(2.9.1 is preferred) from:

 http://www.scala-lang.org/

Don't forget to set SCALA_HOME environment to the path where you install the scala.

AspectJ

You can either download AspectJ from the website:

 http://eclipse.org/aspectj/

or git clone a modified AspectJ which is able to weave DaCapo 9.12 with 179 specifications:

 git clone -b javamop ssh://[your-id]@fslwork.cs.illinois.edu/home/clee83/repository/aspectj

For detailed information, please refer to:

 http://fsl.cs.illinois.edu/index.php/JavaMOPAgent

RV Monitor

Installation

You can clone it from the github:

 https://github.com/runtimeverification/rv-monitor

Use "ant" to build it. After compilation, you will see several .jar files generated under $rv-monitor/lib. Among them:

• rvmonitor.jar: rvmonitor which is used to generate library code with .rvm file.
• rt.jar: runtime library used by generated library code. This jar file contains all the important data structures like AbstactMonitor, AbstractMonitorSet, Indexing Tree and so on.

Usage

You can run the script:

 source $rv-monitor/bin/rvmonitor [options] <path-to-rvm>

Frequently used options are

 -d $MONITOR_DIR -silent -n all -merge

JavaMop

Installation

You can clone it from the github:

 https://github.com/runtimeverification/javamop

Use "ant" to build it.

Usage

You can run the script:

 source $javamop/bin/javamop [options] <path-to-mop>

Frequently used options are

 -d $RVSPEC_DIR -silent -n all -merge

After executing the command, a .aj file will be generated in $RVSPEC_DIR (the library code generated by rvmonitor is appended to the original .aj file). Note that rvmonitor.jar and rt.jar has already been included in the $javamop/lib. JavaMop will invoke rvmonitor automatically during the generation of .aj file. Thus, rvmonitor is "invisible" to the users.

Weave and Run

Compile AspectJ File

Use ajc to weave the code:

 ajc -cp $javamop/lib/rt.jar:$path-to-aspectjrt.jar -d $OUTPUT-DIR <path-to-aj-file> <path-to-java-file>

After compiliation, a .class file will be generated in $OUTPUT-DIR

Run the Weaved Code

Run the following command

 java -cp $javamop/lib/rt.jar:$path-to-aspectjrt.jar Foo

You can also create java agent to weave the code at runtime. For more information, please go to:

 http://fsl.cs.illinois.edu/index.php/JavaMOPAgent