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.
 
Method Summary
 INonPrimitiveExtValue clone(Map<Object,Object> cloneMap)
          Override to specialize return type
 INonPrimitiveExtValue.Field[] getFields()
          Generate a listing of all the values contained inside the encapsulation barrier of this abstract datatype.
 byte[][] linearize(int bitsPerNonPrimitiveValue, ObjectIntTable<INonPrimitiveValue> nonPrimitiveValueIdMap, int bitsPerThreadId, IntIntTable threadOrderMap)
          Linearizes the contained values.
 
Methods inherited from interface edu.ksu.cis.projects.bogor.module.value.INonPrimitiveValue
getReferenceId
 
Methods inherited from interface edu.ksu.cis.projects.bogor.module.value.IValue
equals, getType, getTypeId, hashCode, toString, validate
 
Methods inherited from interface edu.ksu.cis.projects.bogor.util.Disposable
dispose
 
Methods inherited from interface java.lang.Comparable
compareTo
 
Methods inherited from interface edu.ksu.cis.projects.bogor.module.value.IExtValue
visit
 
Methods inherited from interface edu.ksu.cis.projects.bogor.module.value.IValue
equals, getType, getTypeId, hashCode, toString, validate
 
Methods inherited from interface edu.ksu.cis.projects.bogor.util.Disposable
dispose
 
Methods inherited from interface java.lang.Comparable
compareTo
 

Method Detail

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.