Skip to content

QuickStart

Jump to bottom Edit New page
Alessio edited this page Apr 5, 2019 · 14 revisions

Quick-Start

How to play around with Janus and understand the I/O

QUICK-RUN

  • download this zip. It contains only the essential files to run Janus, i.e., the Jar, launcher scripts and 2 example inputs
  • reach the folder where you unzip the program in the terminal
  • for mining
    • use the command "sh start-Janus-mining.sh"
    • read the result in terminal
  • for model checking
    • use the command "sh start-Janus-model-checking.sh"
    • find the JSON output "output_X.json" in the same folder

CHANGE INPUT or SETTINGS

To use other input files or settings you can launch manually the Janus.jar as described below or modify the .sh scripts

LAUNCH COMMAND DETAILS:

This is the expected command to launch the Janus mining:

`java -cp Janus.jar ${JANUS_MAINCLASS} -iLF ${INPUT_LOG} -s ${SUPPORT} -c ${CONFIDENCE}`

where:

  • JANUS_MAINCLASS can be either "minerful.JanusMinerStarter" or "minerful.JanusOfflineMinerStarter", respectively the classic online-ready algorithm and the offline faster one
  • INPUT_LOG the path to the input log file. If the file is a TXT text file add the following option "-iLE strings"
  • SUPPORT/CONFIDENCE thresholds of the respective measures. It is expected a real number between 0.0 and 1.0

This is the expected command to launch the Janus model checking:

`java -cp Janus.jar $JANUS_MAINCLASS -iLF ${INPUT_LOG} -iME json -iMF ${INPUT_MODEL} -JSON ${OUTPUT_FILE}`

where:

  • JANUS_MAINCLASS is "minerful.JanusModelCheckStarter"
  • INPUT_LOG the path to the input log file. If the file is a TXT text file add the following option "-iLE strings"
  • INPUT_MODEL the path to the JSON file containing the model to check
  • OUTPUT_FILE the path where to save the results as a JSON file

EXPLANATION OF MODEL CHECKING OUTPUT

  • Janus uses constraints defined in a reactive form "Activator []-> Target", where both Activator and Target are arbitrary LTLpf formulas. Only a subset of DECLARE constraints is used for now.
  • For readability, regardless of the input log, the output events are encoded in characters like "A", "B", "C",...
  • The result is a 3D matrix of bytes to be read as follows: for each trace -> for each constraint -> for each event of the trace -> byte result = [activator evaluation of (event;constraint;trace)][target evaluation of (event;constraint;trace)]
  • Each byte stores the results of both Activator and target evaluation of a given constraint in a specific trace for a specific event. The left bit is for the activator, the right bit for the target,i.e.,[activator-bit][target-bit] In details:
    • 0 -> 00 -> Activator: False, Target: False
    • 1 -> 01 -> Activator: False, Target: true
    • 2 -> 10 -> Activator: True, Target: False
    • 3 -> 11 -> Activator: True, Target: True
  • Based on the single events evaluation, it is reported a set of measures for the each trace and constraint (Support, Confidence, Lovinger's measure, ...)

e.g.

{
	"TRACE-1":
		{
            "DECLARE-CONSTRAINT-A(VARIABLE1, VAR2, ...)": [ {"EVENT-1": BYTE},{"EVENT2": BYTE},... ]
            "Support": S.S
            "Confidence": C.C
            "Lovinger": L.L
		},
	
	"TRACE-2":
		{
            "DECLARE-CONSTRAINT-B(...)": [ ... ]
            "Support": ...
            "Confidence": ...
            "Lovinger": ...
		},
	...
}

Notes:

SEPSIS event log

Contents

Contents

Clone this wiki locally