Skip to content

Using the Consistency Checking Command Line Interface

Jump to bottom
Luca Beurer-Kellner edited this page Dec 2, 2017 · 3 revisions

If need instructions on how to obtain the cchecker.jar file, please have a look at the Creating cchecker.jar article.

We recommend to use the command line tool jar file.

To get the help text of the command line tool execute:

java -jar cchecker.jar help

The output of this is the following:

USAGE: cchecker <MODE> <ARGUMENTS>
The command line tool support the following modes:

learn alergia - Learns a PDFA model from a given input trace data set
	-dataset
		The trace data set to learn a model from
	-alpha <double>
		[OPTIONAL] The alpha parameter for the alergia algorithm.
	-h
		[OPTIONAL] Use a human-readable PDFA output format. (not usable for further processing)
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


learn bla - Learns a SRE from a given input trace data set using the Blockwise Left-Aligned algorithm
	-dataset
		The trace data set to learn a model from
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


check - Checks consistency of a given dataset with an automaton model
	-dataset
		The trace data set to check against
	-automaton
		The automaton model to check
	--traversalThreshold <double>
		[OPTIONAL] The traversal threshold for automaton matrix generation. Branches with less probability are dismissed automatically. Default 0.
	-h
		[OPTIONAL] Use a human-readable Consistency Report output format.
	-csv
		[OPTIONAL] Use a csv output format that only prints the consistency results.
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


sre-to-pdfa - Transforms a SRE-file to a PDFA model.
	-sreFile
		The location of the SRE file (.sre)
	-h
		[OPTIONAL] Use a human-readable PDFA output format.  (not usable for further processing)
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


inspect - Prints general information on the supplied automaton or dataset.
	-dataset
		[OPTIONAL] The trace data set to inspect.
	-automaton
		[OPTIONAL] The automaton model to inspect.
	-csv
		[OPTIONAL] Use a csv output format for the information.
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


random-pdfa - Generate a random PDFA
	-number-of-states <range>
		Range of the possible number of states. (e.g. 4...6)
	-number-of-transitions <range>
		Range of the possible number of outgoing transitions per state. (e.g. 4...6)
	-size-of-alphabet <range>
		Range of the possible size of the alphabet (distinct labels). (e.g. 4...6)
	-self-cycle-probability <double>
		[OPTIONAL] The probability that a state has a transition to itself
	-seed <integer>
		[OPTIONAL] An integer seed to use for initialization of the random number generator.
	-h
		[OPTIONAL] Use a human-readable PDFA output format.  (not usable for further processing)
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


generate-sample-set - Generate a possible sample set for a given automaton
	-automaton
		The automaton model to generate a sample set for.
	-number-of-traces <integer>
		[OPTIONAL] The number of traces to generate
	-v
		[OPTIONAL] Enables verbose output (e.g. additional progress information)
	-perf
		[OPTIONAL] Performs all operations as specified but only outputs performance information


help - Shows this help text

General Information

Human readable output format

Many commands (e.g. learn, check) provide the option to display the results in a human-readable format. This can be done by adding the additional parameter -h. Note that human-readable output is not meant for further processing. In fact, none of the human-readable (-h) outputs can be put back into the software.

Saving output models/traces/SREs into a new file

The CLI puts all it outputs on the stdout. That means to save an output simply use the redirect operator in the terminal: For instance to save the learning outcome of alergia just use:

java -jar cchecker.jar learn alergia -dataset tracedataset_task1.trc > output.pdfa

Where output.pdfa specifies the output path.

Monitoring performance

To get performance measure of the algorithms and transformation, the parameter -perf can be used. This parameter will suppress all regular output. Instead, it will only output timing results.

For instance, to get performance measures for the generation of random PDFA models, one can execute the following command

java -jar cchecker.jar random-pdfa -number-of-states 1000...1000 -perf

Generate random probabilistic automaton;Parsed input parameters;Generated automaton;Remove unreachable states;Total
0.0;0.275925037;0.372283821;0.538018339;0.538021153

The format is meant to be used in a CSV table. Multiple calls of the CLI can be aggregated into a table which can be used to create performance graphs. (The header row has to be skipped)

Examples

For a better understanding this documents lists a few examples that cover most of the use-cases for the CLI:

Running a consistency check on a dataset and an automaton

java -jar cchecker.jar check -dataset tracedataset_task1.trc -automaton output.pdfa

Given that the two input files are to be found in the current directory under these names.

Note that there is no support for direct checking with .sre files. However, the user can simply use the sre-to-pdfa command to transform their .sre to an equivalent .pdfa model.

For a more readable report output the additional argument -h can be used to change the output format of the report from its XML representation to a more readable

Learning a PDFA model from a trace dataset (using the Alergia algorithm)

java -jar cchecker.jar learn alergia -dataset tracedataset_task1.trc

Use the option -h to get a human-readable output.

Learning a SRE from a trace data set (using the BLA algorithm)

java -jar cchecker.jar learn bla -dataset tracedataset_task1.trc

Generating a synthesized sample set for an automaton

java -jar cchecker.jar generate-sample-set -automaton output.pdfa -number-of-traces 40

Transforming a SRE to a equivalent PDFA

java -jar cchecker.jar sre-to-pdfa -sreFile output.sre

Generating a random PDFA model

java -jar cchecker.jar random-pdfa -number-of-states 1000...1005 -number-of-transitions 20...30 -size-of-alphabet 20...30 -self-cycle-probability 0.8

Inspecting an existing PDFA or dataset file

For automata:

➜ java -jar cchecker.jar inspect -automaton random.pdfa
Number of States: 96
Number of Transitions: 287
Average Number of Transitions: 2.9895833333333335
Alphabet Size: 6

For datasets:

➜ java -jar cchecker.jar inspect -dataset random.strc
Number of Traces: 160
Average Trace Length: 9.43125
Alphabet Size: 6

This also has support for CSV output:

➜ java -jar cchecker.jar inspect -dataset random.strc -csv
Number of Traces;Average Trace Length;Alphabet Size
160;9.43125;6

The parameters specify numeric intervals. For instance 1000...1005 represents the interval [1000, 1005[.

Changelog

Version 0.1

Initial version

Version 0.2

  • New mode inspect that can be used with -automaton or -dataset to print basic information on the models/datasets. See Inspect examples
  • Remove debug output from check (counting lengths)
  • Report files of the CLI tool can now be viewed in the Plugin Report Viewer
  • check now support an additional parameter -traversalThreshold <double> that allows to set a value for the traversal threshold while creating the automaton footprint matrices. Very small values like 0.00000001 are already super effective. (Reduces time for borg1000-sre checking to 6s). However, the threshold will also decrease the accuracy of the checking result so be carefule!
Clone this wiki locally