edu.ksu.cis.projects.bogor.module.value
Interface INonPrimitiveExtValue
- All Superinterfaces:
- Comparable<IValue>, Disposable, IExtValue, INonPrimitiveValue, IValue, Serializable
public interface INonPrimitiveExtValue
- extends INonPrimitiveValue, IExtValue, Serializable
Represents an instance of a new type declared through the extension
mechanism.
Very important: if a INonPrimitiveExtValue
implementation stores a reference to any IModule (usually,
these take the form of core model-checking components such as the
IValueFactory or ISearcher), the reference
must be declared transient. This requirement
facilitates the automatic serialization and transport of a Bogor state object (
IState) to a different Bogor runtime instantiation (either
locally, or on a remote network host). IModule implementations
purposely do not implement Serializable, so the Java Virtual
Machine will throw an exception if the serializer reaches a non-
transient field referencing one of Bogor's core model checking
components or a user-supplied extension module.
Incorrect usage:
// this field cannot be serialized
IValueFactory vf;
public IMessageStore connect(IBogorConfiguration bc)
{
vf = bc.getValueFactory();
....
}
public void dispose()
{
vf = null;
}
Corrected usage:
transient IValueFactory vf;
public IMessageStore connect(IBogorConfiguration bc)
{
vf = bc.getValueFactory();
....
}
public void dispose()
{
vf = null;
}
// called after a state is unmarshalled
public void validate(IBogorConfiguration bc)
{
vf = bc.getValueFactory();
}
- Version:
- CVS $Revision: 1.10 $ $Date: 2005/06/07 02:34:45 $
- Author:
- Robby , Matt Hoosier
|
Nested Class Summary |
static interface |
INonPrimitiveExtValue.Field
A data value contained inside the abstract datatype encapsulation of a
INonPrimitiveExtValue. |
| Methods inherited from interface edu.ksu.cis.projects.bogor.module.value.IExtValue |
visit |
getFields
INonPrimitiveExtValue.Field[] getFields()
- Generate a listing of all the values contained inside the encapsulation
barrier of this abstract datatype. This is used for externalization
purposes (e.g., counterexamples and guided simulations).
- Returns:
- a sequence of named values that convey the internal state of the
data structure.
linearize
byte[][] linearize(int bitsPerNonPrimitiveValue,
ObjectIntTable<INonPrimitiveValue> nonPrimitiveValueIdMap,
int bitsPerThreadId,
IntIntTable threadOrderMap)
- Linearizes the contained values.
- Parameters:
bitsPerNonPrimitiveValue - The number of bits used to encode a non-primitive value.nonPrimitiveValueIdMap - A mapping of non-primitive values to their unique id. Must be
non-null.bitsPerThreadId - The number of bits used to encode a thread descriptor.threadOrderMap - A mapping of thread descriptors to their order number. Must be
non-null.
- Returns:
- The bit-vectors representation of this value.
clone
INonPrimitiveExtValue clone(Map<Object,Object> cloneMap)
- Override to specialize return type
- Specified by:
clone in interface INonPrimitiveValue- Specified by:
clone in interface IValue
- Parameters:
cloneMap - Original values (IValue) to their clones (
IValue) mapping. The clone map to solve
circular references in values. If this value is a key in the
map, then this method returns the value of the key in the map.
Must be non-null.
- Returns:
- The clone of this value. Non-null.