Closed monperrus closed 7 years ago
Hi Martin,
Thanks for the report. I've fixed the links to the wiki from the README file, they should work now. The correct link for InvariMint usage screen is this one: https://github.com/ModelInference/synoptic/wiki/DocsInvariMintCmdLineHelpScreen
For installing, the instructions for InvariMint are nearly identical as for synoptic, here: https://github.com/ModelInference/synoptic/wiki/DocsInstallation
To build/use from the command line:
This will first build daikonizer and synoptic, which are invarimint dependencies, and then it will build invarimint.
Let us know if you run into any other issues.
ivan.
Thanks. I'll try and let you know.
build with ant
done
you should be able to run "./invarimint.sh -h"
Works fine, thanks
Usage: invarimint [options]
How to produce those log files?
Log files are text files that capture temporal program behavior, e.g., listing one program event or program state per log line. A log file may include several executions of the program. Informally, a log is a file that contains arbitrary text. Arguments to invarimint tell it how to parse that text.
You can find a bunch of example log files under the traces/ directory at top level. For example, one complete example is in traces/abstract/simple-email/
The README.txt in that dir explains the example as:
An example email client input to kTails InvariMint that is used to
introduce the SimpleAlg example in the InvariMint ICSE paper.
In that dir you'll find a trace.txt file that contains the following:
login
check
check
logout
--
login
check
compose
send
logout
You'll also find two argument files, one for invarimint and one for synoptic (another project in same repo). The args_invarimint.txt file contains:
--invMintKTails=true
--kTailLength=1
-r ^(?<TYPE>)$
-s ^--$
-o output/simple-email-invarimint.png
--minimizeIntersections=true
Notice the -r ^(?<TYPE>)$
and -s ^--$
lines which mean that (1) each line in the log file should be interpreted as an event type, and (2) that the "--" is considered an execution separator. These are regular expressions; TYPE
is a built-in capture group.
Informally this means that the alphabet of the state machine that InvariMint will try to infer will contain symbols like "send", "logout", etc. And it will derive this state machine using the two finite traces above.
The args file is handy because you can pass it to invarimint directly, like this:
./invarimint.sh -c traces/abstract/simple-email/args_invarimint.txt traces/abstract/simple-email/trace.txt
If you run this then you'll be able to find the a png of the invarimint-generated model (assuming you have the graphviz dot command installed). The -o output/simple-email-invarimint.png
flag tells invarimint where to place the generated png file. Here is the model that it generate for me:
OK, that's clear thanks.
Does it mean that synoptic does not provide any tracing / instrumentation mechanism?
What do you recommend for tracing the execution of Java programs (eg calls) before using InvariMint?
Yes, these projects don't include any tracing/instrumenting mechanism.
One simple option is a dtrace-based script in the dir synoptic/jvm-dtracing/
The dtrace.sh
script worked for me on OSX without installing anything, but I haven't used it in a while. This will trace Java method names and their calls/returns. There is a bit of documentation at top of the script and in the synflow.d
file that is in the same dir and implements the tracing logic.
Doing a bit of googling you'll find other tracing mechanisms. I'm not as familiar with what's recommended, since we are typically using custom tracing tools or assume a blackbox system and just analyze console logs. Here is a link that discusses some options for Java: http://stackoverflow.com/questions/29382231/how-do-i-trace-methods-calls-in-java
Thanks! --Martin
Hi,
I'm looking for a getting started like doc on InvariMint (how to compile and run)? Is there something like this somewhere?
(the link to https://github.com/ModelInference/synoptic/blob/master/DocsInvariMintCmdLineHelpScreen on the main README seems to be broken)
Thanks, --Martin