How to create *.JPF file to run JPF from a Java application?

[naouar...@gmail.com]

Hi everybody,

I´m developping a java app in order to run JPF from command. So i call the program as following

final String jpf_exe = propiedades.getProperty("root-jpf"); // this root refers to jpf-core/bin/jpf
Process p = Runtime.getRuntime().exec("cmd /c "+jpf_exe+" DiningPhil 4"); // this executes JPF from command and it works perfectly
 
In this sample i´m using DiningPhil class as main class only to try if it works or not , but in my java app, the user upload the main class, its arguments, a file.properties and maybe some "+<key>=<value>" pairs and then my app has to be able to use all these information to run JPF and check the main class.

I´ve seen i can to call JPF with the main class like this :

<jpf-core-dir>/bin/jpf +classpath=. <application-main-class> 

or with *.jpf file like this :
 <jpf-core-dir>/bin/jpf <application-property-file>.jpf

So, which the best methode to call JPF and how can i specify the configuration to call correctly jpf?
Thank you in advance!

Noa.

[PETER C MEHLITZ]

if you have your own JPF driver application anyways, there is no need to start JPF as an external process. You can directly create and initialize the Config object, and instantiate and run the JPF object from your Java code. Look at JPF.start() to see how.

Actually, you can even start your application through JPF if you implement the JPFShell interface and set it as the 'shell' property. See
- http://babelfish.arc.nasa.gov/trac/jpf/wiki/user/run
- http://babelfish.arc.nasa.gov/trac/jpf/wiki/devel/embedded
- http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-shell
for details, although some of this needs to be updated

-- Peter

> --
>
> ---
> You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.

[naouar...@gmail.com]

Hi Peter,

I know i can run JPF as an object, but i have to do it as i explained before. I have to develop a methode in java able to run JPF from command.
This methode has as arguments the main class name or directory, its arguments, key=value pairs if they exist , and a property file (optional as configuration property file) . So how can i call JPF from command with all this information?

Thanks in advance.

[PETER C MEHLITZ]

just like you would invoke it from a command line: "java -jar .../RunJPF.jar +key=val ... <application>.jpf"

If you have to use a specific site.properties that is not in your current directory hierarchy or your ~/.jpf/, you would have to add this as +site=<pathname> to your command line, or as 'site=<pathname>' to your *.jpf

If your create your own application properties file (*.jpf), you can of course also put all your command line options in there. Note that command line options are loaded last, i.e. they override anything that was previously found in a JPF configuration file.

Your application main class has to be specified as 'target=<classname>' (that should go in your generated *.jpf)

-- Peter

[naouar...@gmail.com]

Hi Peter,

When you say "my own application properties file (*.jpf)," which file do you refer to ? in my case all i have are the main class (to check ) ,its arguments and the options to execute JPF. So how can i generate *.jpf ? This is what i don´t really understand :(

Thank you very much.

[PETER C MEHLITZ]

it's a normal text file, so there is no problem creating it from Java. If you don't have a lot of options you can of course bypass and specify everything as "+key=value" arguments - there is no JPF option that can't be set that way. Your main class has to be the 'target' option, your main class arguments the 'target.args'

-- Peter

[naouar...@gmail.com]

Hi,

Ok, so i created a text file with the following information:
target= DiningPhil
target.args =4

and i saved it as MyApp.jpf in the same directory as RunJPF.jar  (exactly in jpf-core/build) , then when i execute JPF from command like this :
> java -jar jpf-core\build\RunJPF.jar MyApp.jpf  , this error appears

JPF configuration error: error in C:\jpf-core\jpf.properties : property file does not exist: C:\\MiApp.jpf
        at gov.nasa.jpf.Config.exception(Config.java:1098)
        at gov.nasa.jpf.Config.loadProperties(Config.java:425)
        at gov.nasa.jpf.Config.<init>(Config.java:218)
        at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:88)

Have i to modify something in jpf.properties?

Thanks a lot!!

[Peter Mehlitz]

(1) you should not store anything in jpf-core - keep your sources/binaries in a separate JPF project

(2) you have to give JPF a pathname for the application properties file (*.jpf). If there is no directory specification JPF would only find it in the directory from where you start java

(3) your printout is inconsistent - your command line says MyApp.jpf, but the configuration error is about MiApp.jpf. Did you modify jpf-core/jpf.properties (which you shouldn't)?

-- Peter

> --

[jinjian...@gmail.com]

hi, Peter

    I am a college student and right now I am required to build up a website which will use JPF to verify the java program uploaded by users, but after I clone the jpf I have no idea what is the next step I should do because I can't find a step by step tutorial for this kind of using JPF（JPF is complete new to me). I will use Java EE  to build this website. Could you give me some useful resource about it (I really need a STEP BY STEP tutorial because otherwise I will get lost in this tutorial since I don't know much about JPF)?

在 2013年11月8日星期五 UTC+8上午2:04:36，pcmehlitz写道：

[Cyrille Artho]

Hi,
Just keep in mind that having a web site where users can upload a program is a bad idea.
A web site could take arbitrary source code that, for example, deletes all files in a system.
The web-based tool would then compile the code and execute it in JPF, and that would be that last thing on that server, because next, all files would be deleted.