korat
Class Korat

java.lang.Object
  korat.Korat

public class Korat
extends Object

Korat Main Class

Author:

Sasa Misailovic

Constructor Summary

Korat()

Method Summary

static void

main(String[] args) Loader of Korat Application

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Korat

public Korat()

Method Detail

main

public static void main(String[] args)

Loader of Korat Application

Parameters:

args - - program arguments are listed below.

Arguments:

--args <arg-list>	mandatory	comma separated list of finitization parameters, ordered as in corresponding finitization method.
--class <fullClassName>	mandatory	name of test case class
--config <fileName>	optional	name of the config file to be used
--cvDelta	optional	use delta file format when storing candidate vectors to disk
--cvEnd <num>	optional	set the end candidate vector to <num>-th vector from cvFile
--cvExpected <num>	optional	expected number of total explored vectors
--cvFile <filename>	optional	name of the candidate-vectors file
--cvFullFormatRatio <num>	optional	the ratio of full format vectors (if delta file format is used)
--cvStart <num>	optional	set the start candidate vector to <num>-th vector from cvFile
--cvWrite	optional	write all explored candidate vectors to file
--cvWriteNum <num>	optional	write only <num> equi-distant vectors to disk
--excludePackages <packages>	optional	comma separated list of packages to be excluded from instrumentation
--finitization <finMethodName>	optional	set the name of finitization method. If ommited, default name fin<ClassName> is used.
--help	optional	print help message.
--listeners <listenerClasses>	optional	comma separated list of full class names that implement ITestCaseListener interface.
--maxStructs <num>	optional	stop execution after finding <num> invariant-passing structures
--predicate <predMethodName>	optional	set the name of predicate method. If ommited, default name "repOK" will be used
--print	optional	print the generated structure to the console
--printCandVects	optional	print candidate vector and accessed field list during the search.
--progress <threshold>	optional	print status of the search after exploration of <threshold> candidates
--serialize <filename>	optional	seralize the invariant-passing test cases to the specified file. If filename contains absolute path, use quotes.
--visualize	optional	visualize the generated data structures

Example command line ::
java korat.Korat --class korat.examples.binarytree.BinaryTree --args 3,3,3