jpf-trace-server produces no output besides running src/examples

53 views
Skip to first unread message

Darky SiDai

unread,
Nov 13, 2010, 12:33:21 PM11/13/10
to Java™ Pathfinder
I have a really weird problem when running jpf-trace-server.
Jpf-trace-server works fine when I run the typical examples from jpf-
trace-server/src/examples, but
it produces no output when I try to run anything else.

Files .jpf and jpf-core is fine, I run a bunch of other tests without
using the jpf-trace-server extension.
I should point out that jpf doesnt crash or produce any kind of error,
it just runs my
target application regularly (test application output is shown
normally) and then finishes without
any console output.

I tried all the possible combinations for the .jpf application file
and still no use. The .jpf
files that come with the extension all run as supposed to.

I cannot make any sense out of it, I suppose it has something to do
with the paths.
I paste a typical application .jpf I use and runs smoothly but with no
results below,
any help will be much appreciated! :


*********************
@using = jpf-trace-server

target = Main

classpath = ${jpf-core}/src/examples/LogicSUT/
sourcepath = ${jpf-core}/src/examples/LogicSUT/


listener=gov.nasa.jpf.traceEmitter.DefaultTraceEmitter
traceServer.db_location = dbTrace
traceServer.local_storer = true
traceServer.trace_storer = inMemory
traceServer.skip_init = true

report.publisher=genericConsoleTracePrinter
report.genericConsoleTracePrinter.class=gov.nasa.jpf.traceServer.printer.GenericConsoleTracePrinter
report.genericConsoleTracePrinter.property_violation=output,trace


traceServer.tracePrinter.instruction.show=true
traceServer.tracePrinter.instruction.printExtraData=false

traceServer.tracePrinter.object.show=true
traceServer.tracePrinter.thread.show=true

report.console.property_violation = error,trace
*********************

Darky SiDai

unread,
Nov 14, 2010, 6:45:09 AM11/14/10
to Java™ Pathfinder
I should also add that I updated jpf-trace-server ~15 days ago and,
before that,
it used to run smoothly on default configuration..

Igor Andjelkovic

unread,
Nov 15, 2010, 1:38:37 PM11/15/10
to java-pa...@googlegroups.com
Hi Darky,

thank you for your interest in jpf-trace-server.

Does your app violates a property?
The trace will be printed only if that is the case.
If your app finishes normally, you will have to "analyze" the stored trace,
by writing a special trace-analyzer for your domain, or you can use
gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer to print each event stored in the last path.

I hope that this information will help you.

Regards,
Igor

Darky SiDai

unread,
Nov 17, 2010, 1:30:24 PM11/17/10
to Java™ Pathfinder
Thanks,

Can you provide an example of using
gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer
as a parameter in the .jpf configuration file, because I obviously
miss something..

--George

Darky SiDai

unread,
Nov 17, 2010, 1:52:30 PM11/17/10
to Java™ Pathfinder
To be more specific, I am trying to filter the output and get the
trace
in a form like this :

************
oldclassic.java:126 : System.out.println(" 2");
getstatic
ldc
invokevirtual java.io.PrintStream.println(Ljava/lang/String;)
************

and, if possible, to avoid API calls, javax, java etc and get only the
AUTs execution paths.
At the moment I get a ton of info without reference to the AUT's
source code line.
Tried configuring using consoleTracePrinter as report.publisher but it
doesn't seem to change my results.
By the way, im using the
"traceServer.trace_analyzer=gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer"
configuration as you suggested.

--George

Igor Andjelkovic

unread,
Nov 21, 2010, 4:43:09 PM11/21/10
to java-pa...@googlegroups.com
I apologize for the delay in response.

The ExecTracker has been updated, so now it can print data as well as
the ConsoleTracePrinter.
Current solution is hard-wired, because I am working on a new method of
printing for analyzers.

To be able to use a new way of printing with ExecTracker, you'll have to
provide:

traceServer.trace_analyzer=gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer
# "likeConsole" for a new way of printing, "all" for the old one
traceServer.trace_analyzer.params=all

This will remove details about java* API calls, only method name will be
printed.

The same thing can now be used with consoleTracePrinter, for printing on
propertyViolation by providing:
report.consoleTracePrinter.show_api_calls=false

This is a temporary solution, I will continue to work on it.

Regards,
Igor

Darky SiDai

unread,
Nov 22, 2010, 3:33:52 PM11/22/10
to Java™ Pathfinder
I updated jpf-trace-server and used the configuration you
suggested in order avoid printing the API, but no use. It still
creates a ~27MB file
with all the api instructions inside.

I am posting my .jpf application file in order to have a look,
I might have forgotten to use something small and silly.

***************************

# trace emitter
listener+=,gov.nasa.jpf.traceEmitter.DefaultTraceEmitter

# DB location (folder), it will be created if it doesn't already
exist,
# not used when trace_storer is not persistent, like "inMemory"
traceServer.db_location = dbTrace
# local(true) or remote(false) server
traceServer.local_storer = true
# trace_storer type, "inMemory" or "neo4j"
traceServer.trace_storer = inMemory
# skip initial instructions
traceServer.skip_init = true

# add trace analyzers (full name required)
traceServer.trace_analyzer=gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer
traceServer.trace_analyzer.params=all

*****************************

Thanks for your time,

--George

Igor Andjelkovic

unread,
Nov 22, 2010, 6:03:40 PM11/22/10
to java-pa...@googlegroups.com
I made a typo, use:

traceServer.trace_analyzer=gov.nasa.jpf.traceAnalyzer.ExecTrackerAnalyzer
traceServer.trace_analyzer.params=consoleLike


The parameter should be "consoleLike", not "all".

Regards,
Igor

Reply all
Reply to author
Forward
0 new messages