gov.nasa.jpf.symbc.veritesting.VeritestingUtil

Class RegionMetricsVisitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

gov.nasa.jpf.symbc.veritesting.VeritestingUtil.RegionMetricsVisitor

All Implemented Interfaces:

AstVisitor<Stmt>, ExprVisitor<za.ac.sun.cs.green.expr.Expression>

public class RegionMetricsVisitor
extends AstMapVisitor

Field Summary

Fields

Modifier and Type	Field and Description
private int	depth
private java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression>	ifCondCache
private int	maxDepth
private long	thisNumPaths
private long	totalNumPaths

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

eva, exprVisitor

Constructor Summary

Constructors

Modifier	Constructor and Description
private	RegionMetricsVisitor()

Method Summary

Modifier and Type	Method and Description
static boolean	execute(DynamicRegion dynRegion)
static boolean	execute(StaticRegion staticRegion)
private void	reset(java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression> oldIfCondCache)
private void	snapshot(java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression> oldIfCondCache)
Stmt	visit(CompositionStmt s)
Stmt	visit(IfThenElseStmt a)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.AstMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.visitors.ExprMapVisitor

visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit

Methods inherited from class java.lang.Object

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

Field Detail

depth

private int depth

maxDepth

private int maxDepth

totalNumPaths

private long totalNumPaths

thisNumPaths

private long thisNumPaths

ifCondCache

private java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression> ifCondCache

Constructor Detail

RegionMetricsVisitor

private RegionMetricsVisitor()

Method Detail

visit

public Stmt visit(CompositionStmt s)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

visit

public Stmt visit(IfThenElseStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

Overrides:

visit in class AstMapVisitor

snapshot

private void snapshot(java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression> oldIfCondCache)

reset

private void reset(java.util.LinkedHashSet<za.ac.sun.cs.green.expr.Expression> oldIfCondCache)

execute

public static boolean execute(StaticRegion staticRegion)

execute

public static boolean execute(DynamicRegion dynRegion)