gov.nasa.jpf.symbc

Class Observations

java.lang.Object

gov.nasa.jpf.symbc.Observations

public class Observations
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
static double	lastMeasuredMetricValue Used by MetricListener to propagate last measured metric value.
static double	lastObservedCost Used for user-defined cost.
static int	lastObservedInputSize Used to set current input size in side-channel analysis in order to generate correct input file.
static gov.nasa.jpf.symbc.numeric.Expression	lastObservedSymbolicExpression Used for maximization of user-defined cost.

Constructor Summary

Constructors

Constructor and Description
Observations()

Method Summary

Modifier and Type	Method and Description
static void	reset()

Methods inherited from class java.lang.Object

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

Field Detail

lastObservedCost

public static double lastObservedCost

Used for user-defined cost.

lastObservedSymbolicExpression

public static gov.nasa.jpf.symbc.numeric.Expression lastObservedSymbolicExpression

Used for maximization of user-defined cost.

lastObservedInputSize

public static int lastObservedInputSize

Used to set current input size in side-channel analysis in order to generate correct input file.

lastMeasuredMetricValue

public static double lastMeasuredMetricValue

Used by MetricListener to propagate last measured metric value.

Constructor Detail

Observations

public Observations()

Method Detail

reset

public static void reset()