gov.nasa.jpf.symbc.veritesting.ast.transformations

Class DefaultTransformation

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.DefaultTransformation

All Implemented Interfaces:

Transformation

Direct Known Subclasses:

LinearizationTransformation

public abstract class DefaultTransformation
extends java.lang.Object
implements Transformation

Abstract class that defines transformation execution and then checking its invariants.

Constructor Summary

Constructors

Constructor and Description
DefaultTransformation()

Method Summary

Modifier and Type	Method and Description
abstract DynamicRegion	execute(DynamicRegion region)
TransformationData	execute(TransformationData data)
java.lang.String	getName()
java.util.Set<Invariant>	updateInvariants(java.util.Set<Invariant> invariants)

Methods inherited from class java.lang.Object

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

Constructor Detail

DefaultTransformation

public DefaultTransformation()

Method Detail

execute

public TransformationData execute(TransformationData data)
                           throws StaticRegionException

Specified by:

execute in interface Transformation

Throws:

StaticRegionException

execute

public abstract DynamicRegion execute(DynamicRegion region)

updateInvariants

public java.util.Set<Invariant> updateInvariants(java.util.Set<Invariant> invariants)

getName

public java.lang.String getName()

Specified by:

getName in interface Transformation