.rvm files are not generated

[reza-ahmadi]

Hi,

I called javamop on few examples (shipped with javamop). The program said .rvm files and .aj files were generated, but .rvm files are missing!

In one case, I saw that some .rvm files were generated in the output path, but once the execution of javamop finished, those files disappeared!

I am using an Ubuntu 14.04.

Any clues are much appreciated,
Reza

[owolabileg]

Could you please share the exact command that you ran and the output that you got?

[reza-ahmadi]

root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile# javamop SafeFile.mop
-Processing SafeFile.mop
SafeFile.rvm is generated
SafeFileMonitorAspect.aj is generated
-Processing SafeFile.rvm
SafeFileRuntimeMonitor.java is generated
root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile# ll
total 56
drwxrwxr-x 4 reza reza 4096 Oct 24 16:17 ./
drwxrwxr-x 5 reza reza 4096 Oct 24 15:00 ../
drwxrwxr-x 2 reza reza 4096 Jul 11 2015 SafeFile_1/
drwxrwxr-x 2 reza reza 4096 Jul 11 2015 SafeFile_2/
-rw-r--r-- 1 root root 34282 Oct 24 16:17 SafeFileMonitorAspect.aj
-rw-rw-r-- 1 reza reza 971 Jul 11 2015 SafeFile.mop
root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile#

As you can see, there are no .rvm file, the only generated output is the .aj file.

[owolabileg]

Try this: mkdir out; javamop -d out SafeFile.mop

Both the .rvm and .aj files should now be stored in the out directory when execution is complete.

[owolabileg]

Also, did you install JavaMOP from sources or from the binary?

[reza-ahmadi]

Nope. I had tried to save the output files in a folder, but still as you see, only the the aspectJ related file is generated there:

root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile# javamop -d out SafeFile.mop
-Processing SafeFile.mop
SafeFile.rvm is generated
SafeFileMonitorAspect.aj is generated
-Processing SafeFile.rvm
SafeFileRuntimeMonitor.java is generated
root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile# ll out/
total 44
drwxr-xr-x 2 root root 4096 Oct 24 16:39 ./
drwxrwxr-x 5 reza reza 4096 Oct 24 16:39 ../
-rw-r--r-- 1 root root 34282 Oct 24 16:39 SafeFileMonitorAspect.aj
root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile#

It's from the binaries.

[owolabileg]

The binaries are out of sync with the sources, hence my previous suggestion. With the binaries, the keepRVFiles option should work for you, like so:

javamop -keepRVFiles SafeFile.mop

You can see an explanation for the keepRVFiles option by running:

javamop -help

May I ask what you usage scenario for JavaMOP is?

@kheradmand, can you please look into making another release of the binaries?

[reza-ahmadi]

OK. Thanks!

Now the output are two files: .js file and a .java file (the monitor: SafeFileRuntimeMonitor.java).

I have now another issue. I am now trying to weave the code using ajc, but it complains (5 errors):

root@reza:/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile# ajc -1.6 -d out/ out/SafeFileMonitorAspect.aj out/SafeFileRuntimeMonitor.java SafeFile_1/SafeFile_1.java
/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile/out/SafeFileRuntimeMonitor.java:20 [error] The type SafeFileMonitor_Set is already defined
final class SafeFileMonitor_Set extends com.runtimeverification.rvmonitor.java.rt.tablebase.AbstractMonitorSet {
^^^^^^^^^^^^^^^^^^
/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile/out/SafeFileRuntimeMonitor.java:108 [error] The type ISafeFileMonitor is already defined
interface ISafeFileMonitor extends IMonitor, IDisableHolder {
^^^^^^^^^^^^^^^
/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile/out/SafeFileRuntimeMonitor.java:111 [error] The type SafeFileDisableHolder is already defined
class SafeFileDisableHolder extends DisableHolder implements ISafeFileMonitor {
^^^^^^^^^^^^^^^^^^^^
/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile/out/SafeFileRuntimeMonitor.java:133 [error] The type SafeFileMonitor is already defined
class SafeFileMonitor extends com.runtimeverification.rvmonitor.java.rt.tablebase.AbstractSynchronizedMonitor implements Cloneable, com.runtimeverification.rvmonitor.java.rt.RVMObject, ISafeFileMonitor {
^^^^^^^^^^^^^^
/home/reza/Desktop/MOP/javamop/examples/CFG/SafeFile/out/SafeFileRuntimeMonitor.java:547 [error] The type SafeFileRuntimeMonitor is already defined
public final class SafeFileRuntimeMonitor implements com.runtimeverification.rvmonitor.java.rt.RVMObject {
^^^^^^^^^^^^^^^^^^^^^

5 errors

Any idea?

By the way, I am also interested in run-time verification, so i'm learning now.

[owolabileg]

What command did you run?

[owolabileg]

Sorry, I see it in your message.

[reza-ahmadi]

No more ideas?

I am wondering if you could release some last version of binaries? I have issues with building, too, and currently the binaries suit me the best.

I'd appreciate it

[devturnip]

I know this is an old issue, sorry for bringing it up but was this issue ever resolved? Im following the instructions in here to build the agent but the rvm files are not generated for me as well.

[devturnip]

So i think there are a few issues at hand here.

1. In the instructions mvn package does not work due to not being able to locate rv-monitor during package time:
   Caused by: org.apache.maven.project.DependencyResolutionException: Could not resolve dependencies for project javamop:javamop:jar:4.0-SNAPSHOT: Failed to collect dependencies at com.runtimeverification.rvmonitor:rv-monitor:jar:[1.4,)

2. Using javamop binary downloaded from the javamop website for some reason fails to generate the rvm files.

What I did (or at least whats worked for me)

1. Build rv-monitor jar ,use mvn local install to install the rv-monitor jar file built from source, use mvn package to build the javamop binaries , use built javamop binaries and follow the tutorial again for building the agent.
   a. Building rv-monitor only worked when using an ubuntu machine for me see here. It results in version 1.4 being built.
   b. pom.xml in javamop expects version 1.3 for rv-monitor. I changed it to 1.4
   c. Following this stackoverflow on how to install local jar files i ran this command: mvn install:install-file -Dfile=/Users/tony/rvmonitor/rv-monitor/lib/rv-monitor -DgroupId=com.runtimeverification.rvmonitor -DartifactId=rv-monitor -Dversion=1.4 -Dpackaging=jar
   
   

Not sure what sort of chaos this would cause down the road but I'm able to build the agent for now.