korat.finitization
Interface IFinitization

All Known Implementing Classes:

Finitization

public interface IFinitization

The IFinitization interface is used to set up the bounds for the search. The Finitization class uses these bounds to build the state space for search.

Author:

korat.team

Method Summary

void	addAll(Class cls, String fieldName, IObjSet objSet) Adds all objects from the given objSet to the given field which has to be of type Collection.
void	addAll(String fullFieldName, IObjSet objSet) Adds all objects from the given objSet to the given field which has to be of type Collection.
void	addAll(String className, String fieldName, IObjSet objSet) Adds all objects from the given objSet to the given field which has to be of type Collection.
boolean	areArraysHandledAsObjects()
IArraySet	createArraySet(Class clz, IIntSet array$length, IFieldDomain array$values, int count) Creates an instance of the IArraySet.
IBooleanSet	createBooleanSet() Creates new IBooleanSet
IByteSet	createByteSet(byte singleValue) Creates IByteSet with the single value that is given as the method parameter.
IByteSet	createByteSet(byte min, byte max) Here the step (differecte) between two consecutive values in the set defaults to 1.
IByteSet	createByteSet(byte min, byte diff, byte max)
IClassDomain	createClassDomain(Class cls) Creates new empty class domain Equivalent to createClassDomain(cls, 0);
IClassDomain	createClassDomain(Class cls, int numOfInstances) Creates new ClassDomain if the ClassDomain with the given Class hasn't already been created or returns existing ClassDomain, no matter if it's size is different from the given parameter numOfInstances
IClassDomain	createClassDomain(String className) Equivalent to createClassDomain(className)
IClassDomain	createClassDomain(String className, int numOfInstances) Helper.
IDoubleSet	createDoubleSet(double singleValue) Creates IDoubleSet with the single value that is given as the method parameter.
IDoubleSet	createDoubleSet(double min, double max) Here the step (differecte) between two consecutive values in the set defaults to 1.
IDoubleSet	createDoubleSet(double min, double diff, double max)
IFloatSet	createFloatSet(float singleValue) Creates IFloatSet with the single value that is given as the method parameter.
IFloatSet	createFloatSet(float min, float max) Here the step (differecte) between two consecutive values in the set defaults to 1.
IFloatSet	createFloatSet(float min, float diff, float max) Here the step (differecte) between two consecutive values in the set defaults to 1.
IIntSet	createIntSet(int singleValue) Creates IIntSet with the single value that is given as the method parameter.
IIntSet	createIntSet(int min, int max) Creates IIntSet with the given min and max parameters.
IIntSet	createIntSet(int min, int diff, int max) Creates IIntSet according to the given parameters.
ILongSet	createLongSet(long singleValue) Creates ILongSet with the single value that is given as the method parameter.
ILongSet	createLongSet(long min, long max) Here the step (differecte) between two consecutive values in the set defaults to 1.
ILongSet	createLongSet(long min, long diff, long max)
IObjSet	createObjSet(Class fieldBaseClass) Helper.
IObjSet	createObjSet(Class fieldBaseClass, boolean includeNull) Creates IObjSet according to the given parameters.
IObjSet	createObjSet(Class fieldBaseClass, int numOfInstances) Helper.
IObjSet	createObjSet(Class fieldBaseClass, int numOfInstances, boolean includeNull) Creates IObjSet and automatically creates given number of instances of the same class Equivalent to IClassDomain c = f.createClassDomain(fieldBaseClass, numOfInstances); IObjSet toReturn = f.createObjSet(fieldBaseClass, includeNull); toReturn.addClassDomain(c); return toReturn;
IFieldDomain	createObjSet(IClassDomain classDomain) Helper.
IFieldDomain	createObjSet(IClassDomain classDomain, boolean includeNull) Similar to createObjSet(IClassDomain classDomain) but also can include null value
IObjSet	createObjSet(String fieldBaseClassName) Helper.
IObjSet	createObjSet(String fieldBaseClassName, boolean includeNull) Helper.
IObjSet	createObjSet(String fieldBaseClassName, int numOfInstances) Helper.
IObjSet	createObjSet(String fieldBaseClassName, int numOfInstances, boolean includeNull) Helper.
IShortSet	createShortSet(short singleValue) Creates IShortSet with the single value that is given as the method parameter.
IShortSet	createShortSet(short min, short max) Here the step (differecte) between two consecutive values in the set defaults to 1.
IShortSet	createShortSet(short min, short diff, short max)
IClassDomain	getClassDomain(Class cls) Searches for the ObjSet of the given Class object.
IClassDomain	getClassDomain(String name) Helper.
IFieldDomain	getFieldDomain(Class cls, String fieldName)
IFieldDomain	getFieldDomain(String fullFieldName)
IFieldDomain	getFieldDomain(String className, String fieldName)
Class	getFinClass() Returns Class object of the finitized class
IFinitization	getIncludedFinitization(Class clazz) Returns the included finitization, if there is such, for type given by clazz parameter
void	handleArraysAsObjects(boolean handleAsObjects) If selected, arrays will be handled like other objects during Korat search.
boolean	includeFinitization(IFinitization fin) Includes information from finitization fin into current finitization.
void	set(Class cls, String fieldName, IFieldDomain fieldDomain) Assigns fieldDomain to the given field (fieldName) of the given class (cls).
void	set(String fullFieldName, IFieldDomain fieldDomain) Helper.
void	set(String className, String fieldName, IFieldDomain fieldDomain) Helper.

Method Detail

getFinClass

Class getFinClass()

Returns Class object of the finitized class

Returns:

Class object for root class that is being finitized

createClassDomain

IClassDomain createClassDomain(String className,
                               int numOfInstances)

Helper.

First, tries to find a Class object for the given className and then calls createClassDomain(Class, int).
Searches in the package of the finitized class, or in the default package.

Parameters:

className - fully qualified name of the class or relative to the package name of the finitized class.

numOfInstances - number of elements to be created

Returns:

created IClassDomain

See Also:

createClassDomain(Class, int)

createClassDomain

IClassDomain createClassDomain(String className)

Equivalent to createClassDomain(className)

Parameters:

className -

Returns:

newly created IClassDomain

See Also:

createClassDomain(String, int)

createClassDomain

IClassDomain createClassDomain(Class cls,
                               int numOfInstances)

Creates new ClassDomain if the ClassDomain with the given Class hasn't already been created or returns existing ClassDomain, no matter if it's size is different from the given parameter numOfInstances

Parameters:

cls - Class of the objects

numOfInstances - number of instances to be created

Returns:

created IClassDomain

See Also:

createClassDomain(String, int)

createClassDomain

IClassDomain createClassDomain(Class cls)

Creates new empty class domain

Equivalent to createClassDomain(cls, 0);

Parameters:

cls - Class of the object

Returns:

created class domain

See Also:

createClassDomain(Class, int)

createIntSet

IIntSet createIntSet(int min,
                     int diff,
                     int max)

Creates IIntSet according to the given parameters.

Parameters:

min - minimal element of this set of integers (included)

diff - step, the difference between to elements

max - maximal element of this set of integers (included)

Returns:

created IIntSet

See Also:

createIntSet(int), createIntSet(int, int)

createIntSet

IIntSet createIntSet(int min,
                     int max)

Creates IIntSet with the given min and max parameters. The difference between two elements is by default 1. Equivalent of createIntSet(min, 1, max).

Parameters:

min - minimal element of this set of integers (included)

max - maximal element of this set of integers (included)

Returns:

created IIntSet

See Also:

createIntSet(int), createIntSet(int, int, int)

createIntSet

IIntSet createIntSet(int singleValue)

Creates IIntSet with the single value that is given as the method parameter. Equivalent of createIntSet(value, 1, value).

Parameters:

singleValue - single value that will be added to IIntSet

Returns:

created IIntSet

See Also:

createIntSet(int, int), createIntSet(int, int, int)

createBooleanSet

IBooleanSet createBooleanSet()

Creates new IBooleanSet

Returns:

newly created IBooleanSet

createByteSet

IByteSet createByteSet(byte min,
                       byte diff,
                       byte max)

Parameters:

min - - minimum value to be included in the set

diff - - difference (step) between two consecutive values in the set

max - - maximum value to be included in the set

Returns:

newly created IByteSet

createByteSet

IByteSet createByteSet(byte min,
                       byte max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created IByteSet

createByteSet

IByteSet createByteSet(byte singleValue)

Creates IByteSet with the single value that is given as the method parameter. Equivalent of createByteSet(value, 1, value).

Parameters:

singleValue - single value that will be added to IByteSet

Returns:

created IByteSet

See Also:

createByteSet(byte, byte), createByteSet(byte, byte, byte)

createShortSet

IShortSet createShortSet(short min,
                         short diff,
                         short max)

Parameters:

min - - minimum value to be included in the set

diff - - difference (step) between two consecutive values in the set

max - - maximum value to be included in the set

Returns:

newly created IShortSet

createShortSet

IShortSet createShortSet(short min,
                         short max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created IShortSet

createShortSet

IShortSet createShortSet(short singleValue)

Creates IShortSet with the single value that is given as the method parameter. Equivalent of createShortSet(value, 1, value).

Parameters:

singleValue - single value that will be added to IShortSet

Returns:

created IShortSet

See Also:

createShortSet(short, short), createShortSet(short, short, short)

createLongSet

ILongSet createLongSet(long min,
                       long diff,
                       long max)

Parameters:

min - - minimum value to be included in the set

diff - - difference (step) between two consecutive values in the set

max - - maximum value to be included in the set

Returns:

newly created ILongSet

createLongSet

ILongSet createLongSet(long min,
                       long max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created ILongSet

createLongSet

ILongSet createLongSet(long singleValue)

Creates ILongSet with the single value that is given as the method parameter. Equivalent of createLongSet(value, 1, value).

Parameters:

singleValue - single value that will be added to ILongSet

Returns:

created ILongSet

See Also:

createLongSet(long, long), createLongSet(long, long, long)

createDoubleSet

IDoubleSet createDoubleSet(double min,
                           double diff,
                           double max)

Parameters:

min - - minimum value to be included in the set

diff - - difference (step) between two consecutive values in the set

max - - maximum value to be included in the set

Returns:

newly created IDoubleSet

createDoubleSet

IDoubleSet createDoubleSet(double min,
                           double max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created IDoubleSet

createDoubleSet

IDoubleSet createDoubleSet(double singleValue)

Creates IDoubleSet with the single value that is given as the method parameter. Equivalent of createDoubleSet(value, 1, value).

Parameters:

singleValue - single value that will be added to IDoubleSet

Returns:

created IDoubletSet

See Also:

createDoubleSet(double, double), createDoubleSet(double, double, double)

createFloatSet

IFloatSet createFloatSet(float min,
                         float diff,
                         float max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created IFloatSet

createFloatSet

IFloatSet createFloatSet(float min,
                         float max)

Here the step (differecte) between two consecutive values in the set defaults to 1.

Parameters:

min - - minimum value to be included in the set

max - - maximum value to be included in the set

Returns:

newly created IFloatSet

createFloatSet

IFloatSet createFloatSet(float singleValue)

Creates IFloatSet with the single value that is given as the method parameter. Equivalent of createFloatSet(value, 1, value).

Parameters:

singleValue - single value that will be added to IFloatSet

Returns:

created IFloatSet

See Also:

createFloatSet(float, float), createFloatSet(float, float, float)

createObjSet

IObjSet createObjSet(Class fieldBaseClass,
                     boolean includeNull)

Creates IObjSet according to the given parameters.

Parameters:

fieldBaseClass - Base type of the field that is used in type checking. If fieldBaseClass is a Class object of a reference type, new IObjSet will be returned, else an exception will be thrown.

includeNull - whether to include null in the IObjSet.

Returns:

- created IObjSet

See Also:

createObjSet(Class), createObjSet(String), createObjSet(String, boolean)

createObjSet

IObjSet createObjSet(Class fieldBaseClass,
                     int numOfInstances,
                     boolean includeNull)

Creates IObjSet and automatically creates given number of instances of the same class

Equivalent to

 IClassDomain c = f.createClassDomain(fieldBaseClass, numOfInstances);
 IObjSet toReturn = f.createObjSet(fieldBaseClass, includeNull);
 toReturn.addClassDomain(c);
 return toReturn;
 

Parameters:

fieldBaseClass - - class of the field

numOfInstances - - instances of the fieldBaseClass that are to be created in the class domain of fieldBaseClass

includeNull - - whether to include null in the IObjSet

Returns:

newly created IObjSet

createObjSet

IObjSet createObjSet(Class fieldBaseClass)

Helper.
Calls createObjSet(fieldBaseClass, false);

Parameters:

fieldBaseClass - Base type of the field

Returns:

newly created IObjSet

See Also:

createObjSet(Class, boolean), createObjSet(String), createObjSet(String, boolean)

createObjSet

IObjSet createObjSet(Class fieldBaseClass,
                     int numOfInstances)

Helper.
First, tries to find a Class object for the given fieldBaseClassName and then calls createObjSet(Class, int, boolean).
Searches in the package of the finitized class, or in the default package.

Parameters:

fieldBaseClass -

numOfInstances -

Returns:

newly created IObjSet

createObjSet

IObjSet createObjSet(String fieldBaseClassName,
                     boolean includeNull)

Helper.
First, tries to find a Class object for the given fieldBaseClassName and then calls createObjSet(Class, boolean).
Searches in the package of the finitized class, or in the default package.

Parameters:

fieldBaseClassName - name of the base type of the field

includeNull - weather to include null in the IObjSet.

Returns:

created IObjSet

See Also:

createObjSet(Class, boolean), createObjSet(Class), createObjSet(String)

createObjSet

IObjSet createObjSet(String fieldBaseClassName,
                     int numOfInstances,
                     boolean includeNull)

Helper.
First, tries to find a Class object for the given fieldBaseClassName and then calls createObjSet(Class, int, boolean).
Searches in the package of the finitized class, or in the default package.

Parameters:

fieldBaseClassName -

numOfInstances -

includeNull -

Returns:

newly created IObjSet

createObjSet

IObjSet createObjSet(String fieldBaseClassName)

Helper.
Calls createFieldDomain(fieldBaseClassName, false);

Parameters:

fieldBaseClassName - name of the base type of the field

Returns:

created IObjSet

See Also:

createObjSet(Class, boolean), createObjSet(Class), createObjSet(String, boolean)

createObjSet

IObjSet createObjSet(String fieldBaseClassName,
                     int numOfInstances)

Helper.
Calls createObjSet(fieldBaseClassName, numOfInstances, false);

Parameters:

fieldBaseClassName -

numOfInstances -

Returns:

newly created IObjSet

createObjSet

IFieldDomain createObjSet(IClassDomain classDomain)

Helper.
Creates new ObjectSet for class of the classDomain and adds classDomain. Null value is not allowed

Parameters:

classDomain -

Returns:

newly created IFieldDomain

createObjSet

IFieldDomain createObjSet(IClassDomain classDomain,
                          boolean includeNull)

Similar to createObjSet(IClassDomain classDomain) but also can include null value

Returns:

created IFieldDomain

See Also:

createObjSet(IClassDomain)

createArraySet

IArraySet createArraySet(Class clz,
                         IIntSet array$length,
                         IFieldDomain array$values,
                         int count)

Creates an instance of the IArraySet.

Use this method to create a field domain for the field of an array type. If the given parameter doesn't stand clz.isArray() an IllegalArgumentException will be thrown. The other two parameters are used to set bounds on array length and array components. An array will take any int value from the given IIntSet array$length parameter and any of the array components will take any value from the given IFieldDomain array$values

Parameters:

clz - class of the array field

array$length - possible values for the array length

array$values - possible values for the array components

count - number of arrays to create

Returns:

created IArraySet

set

void set(String fullFieldName,
         IFieldDomain fieldDomain)

Helper.
Parses fullFieldName into className and fieldName according to following format:

• if fullFieldName does not contains "." it is considered as a fieldName of the class which this finitization is for;
• if fullFieldName contains "." then the substring after the last "." in the fullFieldName is considered as a fieldName and the substring before the last "." is taken as className. className should be a fully qualified name of the class or a relative name in the package of the finitized field;

Then calls set(className, fieldName, fieldDomain)

Parameters:

fullFieldName - - name of the field ( format: ClassName.FieldName )

fieldDomain - - field domain

See Also:

set(Class, String, IFieldDomain), set(String, String, IFieldDomain)

set

void set(String className,
         String fieldName,
         IFieldDomain fieldDomain)

Helper.
Searches for the class with the given name (in the default package and in package of the finitized class), and then calls set(Class, String, IFieldDomain)

Parameters:

className - - fully qualified name of the class or name relative to package name of the finitized class

fieldName - - name of the field

fieldDomain - - domain of the field

See Also:

set(String, IFieldDomain), set(Class, String, IFieldDomain)

set

void set(Class cls,
         String fieldName,
         IFieldDomain fieldDomain)

Assigns fieldDomain to the given field (fieldName) of the given class (cls).
Note that you cannot assign field domain to the field of some class if the class domain (ObjSet) for that class has not been created before (e.g. with the call createObjSet(cls, numOfInstances))

Parameters:

cls - - Class object of the class

fieldName - - field name of the given class

fieldDomain - - domain of the field

See Also:

set(String, IFieldDomain), set(String, String, IFieldDomain)

getClassDomain

IClassDomain getClassDomain(String name)

Helper.
Searches for the Class object of the class with the given name and then calls getObjSet(Class)

Parameters:

name - - name of the class of which the ObjSet is requested.

Returns:

existing ObjSet for the given class name or null if is not been created yet.

See Also:

getClassDomain(Class)

getClassDomain

IClassDomain getClassDomain(Class cls)

Searches for the ObjSet of the given Class object.

Parameters:

cls - - Class object of the class

Returns:

existing ObjSet for the given class name or null if is not been created yet.

See Also:

getClassDomain(String)

getFieldDomain

IFieldDomain getFieldDomain(Class cls,
                            String fieldName)

Parameters:

cls -

fieldName -

Returns:

newly created IFieldDomain

See Also:

getFieldDomain(String), getFieldDomain(String, String)

getFieldDomain

IFieldDomain getFieldDomain(String className,
                            String fieldName)

Parameters:

className -

fieldName -

Returns:

newly created IFieldDomain

See Also:

getFieldDomain(Class, String), getFieldDomain(String)

getFieldDomain

IFieldDomain getFieldDomain(String fullFieldName)

Parameters:

fullFieldName -

Returns:

newly created IFieldDomain

See Also:

getFieldDomain(Class, String), getFieldDomain(String, String)

addAll

void addAll(String fullFieldName,
            IObjSet objSet)

Adds all objects from the given objSet to the given field which has to be of type Collection.

Parameters:

fullFieldName - - full name of the field: <className>.<fieldName>

objSet - - set of objects to be added to the given field (collection)

See Also:

addAll(Class, String, IObjSet), addAll(String, String, IObjSet)

addAll

void addAll(String className,
            String fieldName,
            IObjSet objSet)

Adds all objects from the given objSet to the given field which has to be of type Collection.

Parameters:

className - - name of the field's declaring class (class which contains the field)

fieldName - - name of the field

objSet - - set of objects to be added to the given field (collection)

See Also:

addAll(String, IObjSet), addAll(Class, String, IObjSet)

addAll

void addAll(Class cls,
            String fieldName,
            IObjSet objSet)

Adds all objects from the given objSet to the given field which has to be of type Collection.

Parameters:

cls - - field's declaring class (class which contains the field)

fieldName - - name of the field

objSet - - set of objects to be added to the given field (collection)

See Also:

addAll(String, IObjSet), addAll(String, String, IObjSet)

includeFinitization

boolean includeFinitization(IFinitization fin)

Includes information from finitization fin into current finitization. Only one finitization of the same type can be included.

Parameters:

fin - - finitization which will be included in current finitization

Returns:

- is finitization including successful

See Also:

getIncludedFinitization(Class)

getIncludedFinitization

IFinitization getIncludedFinitization(Class clazz)

Returns the included finitization, if there is such, for type given by clazz parameter

Parameters:

clazz - - class for which the finitization has been done

Returns:

- included finitization the root of which is clazz, if exists. Otherwise returns null

See Also:

includeFinitization(IFinitization)

handleArraysAsObjects

void handleArraysAsObjects(boolean handleAsObjects)

If selected, arrays will be handled like other objects during Korat search. This implies that one array object might be shared among many objects.

Another option is to treat array objects as special "field containers", that may belong to only one object.

Parameters:

handleAsObjects - - should arrays be treated like objects during search.

See Also:

areArraysHandledAsObjects()

areArraysHandledAsObjects

boolean areArraysHandledAsObjects()

Returns:

- are arrays treated as objects during Korat search