gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class StatisticManager

java.lang.Object

gov.nasa.jpf.symbc.veritesting.VeritestingUtil.StatisticManager

public class StatisticManager
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
static int	ArraySPFCaseCount
static double	avgExecPathCount
static long	constPropTime
static int	hgOrdRegionInstance
static int	ifRemovedCount
static boolean	inializeQueriesFile
static int	instPhaseEx
static java.lang.String	instructionToExec
static int	interestingRegionCount
static int	maxBranchDepth
static long	maxExecPathCount
static int	numMethodSummaries
static int	PCSatSolverCount
static long	PCSatSolverTime
static java.util.HashMap<java.lang.String,RegionStatistics>	regionsStatisticsMap
static int	solverQueriesUnique
static int	staticPhaseEx
static int	thisHighOrdCount
static int	unknownPhaseEx
static boolean	veritestingRunning

Constructor Summary

Constructors

Constructor and Description
StatisticManager()

Method Summary

Modifier and Type	Method and Description
void	collectStaticAnalysisMetrics(java.util.HashMap<java.lang.String,StaticRegion> veriRegions)
int	getConcreteInstNum()
int	getConcreteRegionNum()
int	getDistinctSpfRegionNum()
java.lang.String	getDistinctVeriRegionKeys()
int	getDistinctVeriRegionNum()
int	getFailedInstantiations()
int	getFailNum(FailEntry.FailReason failReason)
int	getInstFailNum(FailEntry.FailReason failReason)
int	getSuccInstantiations()
private boolean	isInterestingRegion(java.lang.String key)
java.lang.String	printAccumulativeStatistics()
java.lang.String	printAllExceptionStatistics()
java.lang.String	printAllRegionStatistics()
void	printHeuristicStatistics()
java.lang.String	printInstantiationStatistics()
java.lang.String	printStaticAnalysisStatistics()
int	regionCount()
void	updateConcreteHitStatForRegion(java.lang.String key)
void	updateSPFHitForRegion(java.lang.String key, java.lang.String failError)
void	updateVeriSuccForRegion(java.lang.String key)

Methods inherited from class java.lang.Object

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

Field Detail

regionsStatisticsMap

public static java.util.HashMap<java.lang.String,RegionStatistics> regionsStatisticsMap

instructionToExec

public static java.lang.String instructionToExec

veritestingRunning

public static boolean veritestingRunning

solverQueriesUnique

public static int solverQueriesUnique

inializeQueriesFile

public static boolean inializeQueriesFile

hgOrdRegionInstance

public static int hgOrdRegionInstance

PCSatSolverCount

public static int PCSatSolverCount

PCSatSolverTime

public static long PCSatSolverTime

constPropTime

public static long constPropTime

ArraySPFCaseCount

public static int ArraySPFCaseCount

ifRemovedCount

public static int ifRemovedCount

maxBranchDepth

public static int maxBranchDepth

maxExecPathCount

public static long maxExecPathCount

avgExecPathCount

public static double avgExecPathCount

numMethodSummaries

public static int numMethodSummaries

interestingRegionCount

public static int interestingRegionCount

staticPhaseEx

public static int staticPhaseEx

instPhaseEx

public static int instPhaseEx

unknownPhaseEx

public static int unknownPhaseEx

thisHighOrdCount

public static int thisHighOrdCount

Constructor Detail

StatisticManager

public StatisticManager()

Method Detail

printHeuristicStatistics

public void printHeuristicStatistics()

updateVeriSuccForRegion

public void updateVeriSuccForRegion(java.lang.String key)

updateSPFHitForRegion

public void updateSPFHitForRegion(java.lang.String key,
                                  java.lang.String failError)

updateConcreteHitStatForRegion

public void updateConcreteHitStatForRegion(java.lang.String key)

printAllRegionStatistics

public java.lang.String printAllRegionStatistics()

printAllExceptionStatistics

public java.lang.String printAllExceptionStatistics()

printAccumulativeStatistics

public java.lang.String printAccumulativeStatistics()

printInstantiationStatistics

public java.lang.String printInstantiationStatistics()

printStaticAnalysisStatistics

public java.lang.String printStaticAnalysisStatistics()

getDistinctVeriRegionNum

public int getDistinctVeriRegionNum()

getDistinctVeriRegionKeys

public java.lang.String getDistinctVeriRegionKeys()

getSuccInstantiations

public int getSuccInstantiations()

getDistinctSpfRegionNum

public int getDistinctSpfRegionNum()

getFailedInstantiations

public int getFailedInstantiations()

getConcreteRegionNum

public int getConcreteRegionNum()

getConcreteInstNum

public int getConcreteInstNum()

getFailNum

public int getFailNum(FailEntry.FailReason failReason)

getInstFailNum

public int getInstFailNum(FailEntry.FailReason failReason)

regionCount

public int regionCount()

collectStaticAnalysisMetrics

public void collectStaticAnalysisMetrics(java.util.HashMap<java.lang.String,StaticRegion> veriRegions)

isInterestingRegion

private boolean isInterestingRegion(java.lang.String key)