Repository navigation
QuickStart
Alessio Cecconi edited this page Nov 26, 2024
·
14 revisions
How to play around with Janus and understand the I/O
- 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
To use other input files or settings you can launch manually the Janus.jar as described below or modify the .sh scripts
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 measurement framework:
`java -cp Janus.jar $JANUS_MAINCLASS -iLF ${INPUT_LOG} -iLE ${LOG_ENCODING} -iMF ${INPUT_MODEL} -iME ${MODEL_ENCODING} -oCSV ${OUTPUT_FILE_CSV} -oJSON ${OUTPUT_FILE_JSON}`
where:
- JANUS_MAINCLASS is "minerful.JanusMeasurementsStarter"
- INPUT_LOG the path to the input log file.
- LOG_ENCODING the format of the log.
- INPUT_MODEL the path to the file containing the model to check.
- MODEL_ENCODING the format of the model.
- OUTPUT_FILE_JSON the path where to save the results as a JSON files.
- OUTPUT_FILE_CSV the path where to save the results as a CSV files.
The measurement command returns in output two files. For example given OUTPUT_FILE_CSV="output":
- output.csv : contains the bit evaluation of each event and the measures for each trace
- output.csvAggregatedMeasures.CSV : the statistics of the trace measures over the entire log
- 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. Json output
{
"TRACE-1":[
{
"DECLARE-CONSTRAINT-A(VARIABLE1, VAR2, ...)": [ {"EVENT1": BYTE},{"EVENT2": BYTE},... ]
"Support": S.S
"Confidence": C.C
"Lovinger": L.L
"...": ...
},
{
"DECLARE-CONSTRAINT-B(...)": [ ... ]
"Support": ...
"Confidence": ...
"Lovinger": ...,
"...": ...
},
{...}
],
"TRACE-2":[
{
"DECLARE-CONSTRAINT-A(...)": [ ... ]
"Support": ...
"Confidence": ...
"Lovinger": ...
"...": ...
},
{...}
],
...
}- The measurement framework main class is named "ModelCheck" for historical reason, but it will be refactored in the future.
SEPSIS event log
- doi:10.4121/uuid:915d2bfb-7e84-49ad-a286-dc35f063a460
- url: https://data.4tu.nl/repository/uuid:915d2bfb-7e84-49ad-a286-dc35f063a460