uk.ac.sheffield.vtts.ground

Class ModelFactory

java.lang.Object

uk.ac.sheffield.vtts.ground.AbstractFactory

uk.ac.sheffield.vtts.ground.ModelFactory

All Implemented Interfaces:

Factory

public class ModelFactory
extends AbstractFactory

ModelFactory is a factory for creating Java models for model-simulation purposes. ModelFactory is used during model-checking and simulation, to create simple Java models that can be evaluated and compared by the model-checking tools. It expects values and types to be supplied in the syntax of the model expression language. As well as being able to create instances of simple and generic types, ModelFactory is able to synthesise the successor and predecessor objects for existing objects of these types. This capability is useful when exploring around the edges of a model specification. A single static ModelFactory is created in Expression and shared by all of its subclasses.

ModelFactory also offers an API for extracting parts of model types, expressed as possibly nested types in the expression language. As well as extracting the value-type of lists and the key- and value-types of maps, it is possible to extract the cognate pair-type for map entries.

Version:

Broker@Cloud 1.0

Author:

Anthony J H Simons

Constructor Summary

Constructors

Constructor and Description
ModelFactory()

Method Summary

Methods

Modifier and Type	Method and Description
protected java.lang.Object	createExternalObject(java.lang.String value, java.lang.String type) Creates an instance of an uninterpreted external type, with the given value.
java.lang.Object	createObject(java.lang.String type) Creates a default instance of any kind of model Object with the given model type.
java.lang.Object	createObject(java.lang.String value, java.lang.String type) Creates an instance of any kind of model Object with the given printed representation and model type.
java.lang.String	getBaseType(java.lang.String paramType) Extracts the base-type name from any parametric type.
java.lang.String	getKeyType(java.lang.String paramType) Extracts the search key-type name from any parametric type.
protected java.lang.Object	getNextList(java.util.List<?> list, java.lang.String type, boolean more) Creates the successor, or predecessor of a list, depending on a flag.
protected java.lang.Object	getNextMap(java.util.Map<?,?> map, java.lang.String type, boolean more) Creates the successor, or predecessor of a map, depending on a flag.
protected java.lang.Object	getNextPair(java.util.Map.Entry<?,?> pair, java.lang.String type, boolean more) Creates the successor, or predecessor of a pair, depending on a flag.
protected java.lang.Object	getNextSet(java.util.Set<?> set, java.lang.String type, boolean more) Creates the successor, or predecessor of a set, depending on a flag.
java.lang.String	getPairType(java.lang.String paramType) Extracts the tuple pair-type name from any parametric type.
java.lang.Object	getPredecessor(java.lang.Object value, java.lang.String type) Returns the predecessor of a value of the given type.
java.lang.Object	getSuccessor(java.lang.Object value, java.lang.String type) Returns the successor of a value of the given type.
java.lang.String	getValueType(java.lang.String paramType) Extracts the value-type name from any parametric type.

Methods inherited from class uk.ac.sheffield.vtts.ground.AbstractFactory

create, createDefaultObject, createListObject, createMapObject, createPairObject, createSetObject, createSimpleObject, error, makeEntityId, safeIndexOf, safeSplit

Methods inherited from class java.lang.Object

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

Constructor Detail

ModelFactory

public ModelFactory()

Method Detail

createObject

public java.lang.Object createObject(java.lang.String type)

Creates a default instance of any kind of model Object with the given model type. This is a convenience for creating model instances when their precise value is not known. It expects the type to be supplied in the modelling language format (using square brackets for generic parameters).

Parameters:

type - the model type, as a String.

Returns:

the default instance of the model type.

createObject

public java.lang.Object createObject(java.lang.String value,
                            java.lang.String type)

Creates an instance of any kind of model Object with the given printed representation and model type. This is the principal factory method for creating model instances. It expects the type to be supplied in the modelling language format (using square brackets for generic parameters).

Parameters:

value - the value, as a String.

type - the model type, as a String.

Returns:

a new instance of the model type.

createExternalObject

protected java.lang.Object createExternalObject(java.lang.String value,
                                    java.lang.String type)

Creates an instance of an uninterpreted external type, with the given value. External types are user-defined types that are uninterpreted in the modelling language. This ModelFactory creates an instance of the model type Entity, which is used to model all uninterpreted types. Entities may be compared for Equality and are hashed on their String identifier, but support no other operations.

Specified by:

createExternalObject in class AbstractFactory

Parameters:

value - an identifier String.

type - an external type, as a String.

Returns:

an instance of the Entity model.

getBaseType

public java.lang.String getBaseType(java.lang.String paramType)

Extracts the base-type name from any parametric type. The supplied paramType is the parametric type of a List, Set, Map or Pair. Searches for the base-type name, which is the first symbol found before the first opening square bracket '['.

Parameters:

paramType - the parametric type name.

Returns:

the base-type, one of List, Set, Map or Pair.

getValueType

public java.lang.String getValueType(java.lang.String paramType)

Extracts the value-type name from any parametric type. The supplied paramType is the parametric type of a List, Set, Map or Pair. Searches for the value-type name, which is the last symbol found before the last closing square bracket ']'. If paramType is either a map-type or pair-type with two actual type parameters, these must be separated by ", ".

Parameters:

paramType - the parametric type name.

Returns:

the value-type, the main element type, or second projection.

getKeyType

public java.lang.String getKeyType(java.lang.String paramType)

Extracts the search key-type name from any parametric type. The supplied paramType is the parametric type of a List, Set, Map or Pair. If paramType is a map-type or pair-type with two actual type parameters separated by ", ", searches for the key-type name, which is the first symbol found after the first opening square bracket '['. If the paramType is a list-type or set-type, returns "Integer" as the index type.

Parameters:

paramType - the parametric type name.

Returns:

the search key-type, the index type or first projection.

getPairType

public java.lang.String getPairType(java.lang.String paramType)

Extracts the tuple pair-type name from any parametric type. The supplied paramType is the parametric type of a List, Set, Map or Pair. If paramType is a map-type "Map[K, V]" or pair-type "Pair[K, V]", returns the related pair-type: "Pair[K, V]". If paramType is a list-type "List[T]" or set-type "Set[T]", returns the synthetic pair-type: "Pair[Integer, T]".

Parameters:

paramType - the parametric type name.

Returns:

the pair-type for keyed (or indexed) elements.

getSuccessor

public java.lang.Object getSuccessor(java.lang.Object value,
                            java.lang.String type)

Returns the successor of a value of the given type. Creates the next monotonically greater object. Integral values grow by unit increment, floating point values grow by a decimal fraction and strings acquire an alphabetically-posterior suffix. Collections increase in size by one element and Pairs increment their wrapped projections. Other external uninterpreted types are returned unchanged.

Parameters:

value - a non-null value.

type - the model type.

Returns:

the next greater value.

getPredecessor

public java.lang.Object getPredecessor(java.lang.Object value,
                              java.lang.String type)

Returns the predecessor of a value of the given type. Creates the last monotonically lesser object. Integral values shrink by a unit decrement, floating point values shrink by a decimal fraction and strings acquire an alphabetically-prior prefix. Collections, if not already empty, reduce in size by one element, and Pairs decrement their wrapped projections. Bottom values and other uninterpreted external types remain unchanged.

Parameters:

value - a non-null value.

type - the model type.

Returns:

the previous smaller value.

getNextList

protected java.lang.Object getNextList(java.util.List<?> list,
                           java.lang.String type,
                           boolean more)

Creates the successor, or predecessor of a list, depending on a flag. If the flag is true, creates the successor list containing one more element, which is the successor element of the last current element (if any). Otherwise, removes the last element of the list (if any).

Parameters:

list - the original list.

type - the parametric type of the list.

more - indicates the successor (true) or predecessor (false).

Returns:

the successor or predecessor of the list, if any.

getNextSet

protected java.lang.Object getNextSet(java.util.Set<?> set,
                          java.lang.String type,
                          boolean more)

Creates the successor, or predecessor of a set, depending on a flag. If the flag is true, creates the successor set containing one more element, which is the first successor of a random element that is not already in the set. Otherwise, removes a random element (if any).

Parameters:

set - the original set.

type - the parametric type of the set.

more - indicates the successor (true) or predecessor (false).

Returns:

the successor or predecessor of the set, if any.

getNextMap

protected java.lang.Object getNextMap(java.util.Map<?,?> map,
                          java.lang.String type,
                          boolean more)

Creates the successor, or predecessor of a map, depending on a flag. If the flag is true, creates the successor map containing one more pair, which is the first successor of a random pair whose key is not already in the map. Otherwise, removes a random pair (if any).

Parameters:

map - the original map.

type - the parametric type of the map.

more - indicates the successor (true) or predecessor (false).

Returns:

the successor or predecessor of the map, if any.

getNextPair

protected java.lang.Object getNextPair(java.util.Map.Entry<?,?> pair,
                           java.lang.String type,
                           boolean more)

Creates the successor, or predecessor of a pair, depending on a flag. If the flag is true, creates the successor pair, consisting of the successors of the first and second projections of the original pair. Otherwise, creates the predecessor pair, consisting of the predecessors of the first and second projections of the original pair.

Parameters:

pair - the original pair.

type - the parametric type of the pair.

more - indicates the successor (true) or predecessor (false).

Returns:

the successor, or predecessor of the pair, if any.