Public Member Functions
boolean	checkMinimalityHS ()
int	compute (int maxHSSize, int maxNumMinHS)
int	computeMore (int newMaxHSSize, int newMaxNumMinHS)
ArrayList	getConflictsAsAss ()
ArrayList	getMinHS ()
	MinHittingSetsFM (boolean conflictsAreMinimal, ABTheoremProver tp, String assumptionAB, String assumptionNAB) throws IllegalAssumption
Static Public Attributes
static final int	CS_ALL_MIN_DIAGS_COMPUTED = 1
static final int	CS_MAX_HS_SIZE_REACHED = 2
static final int	CS_MAX_NUM_MIN_HS_REACHED = 3
Protected Member Functions
void	attemptPrune (HSNodeFM node)
ConflictSet	callTheoremProver (SortedIntList edgeLabels, ConflictSet label)
boolean	canClose (HSNodeFM node)
void	computeLabel (HSNodeFM node)
int	computeNumUnprunedChildren (HSNodeFM node)
void	expandLastLevel (int lastLevel, LinkedList lastLevelNodes, LinkedList newLevelNodes)
void	expandNode (HSNodeFM node, LinkedList newNodes, int lastLevel)
boolean	nodeInvariant (HSNodeFM node)
void	processLastLevel (int lastLevel, LinkedList lastLevelNodes, LinkedList newLevelNodes, boolean expandNodes)
void	prune (HSNodeFM node, HSNodeFM prunedParent)
void	relabel (HSNodeFM node, HSNodeFM newNode)
int	searchRefutingCS (SortedIntList edgeLabel)
Protected Attributes
HSNodeFM	attemptedPruneNode = null
SortedIntList	componentIdSet = new SortedIntList()
ArrayList	componentList = new ArrayList()
TreeMap	components = new TreeMap()
int	computationState = -1
ArrayList	computedMinHS = new ArrayList()
boolean	conflictsAreMinimal
ArrayList	fmConflictSets = new ArrayList()
ArrayList	levels = new ArrayList()
int	maxHSSize
int	maxNumMinHS
int	numExpansions
int	numPrunings
int	numReuses
int	numTPCalls
HSNodeFM	rootNode = null
ABTheoremProver	theoremProver = null
Static Protected Attributes
static final int	CS_COMPUTING = 0

Detailed Description

This class encapsulates an implementation of Reiter's Hitting Set algorithm which supports fault models.

Definition at line 42 of file MinHittingSetsFM.java.

Constructor & Destructor Documentation

hittingsetalg.MinHittingSetsFM.MinHittingSetsFM	(	boolean	conflictsAreMinimal,
		ABTheoremProver	tp,
		String	assumptionAB,
		String	assumptionNAB
	)		throws IllegalAssumption `[inline]`

Conctructor of MinHittingSets, receiving a theorem prover.

The constructor initializes the object instance. A subsequent call to compute() will compute the min. hitting sets incrementally. If conflictsAreMinimal is true, then the algorithm relies on the theorem prover to compute only minmal conflicts.

Throws IllegalAssumption if an assumption different from the two passed assumptions is used.

Parameters:

maxHSSize	The max. size of min. hitting sets to be computed, -1 means all min. hitting sets are computed.
maxNumMinHS	The max. number of computed hitting sets. The algorithm stops as soon as maxNumMinHS hitting sets have been computed. If -1: all min. hitting sets are computed.
conflictsAreMinimal	If true, then all provided conflicts are minimal. As a consequence, the computationally expensive "Pruning" rule is not required.
assumptionAB	the string identifier of the AB assumption, e.g.: "AB", "N_OK", "ABNORMAL",..
assumptionNAB	e.g.: "NAB", "N_AB", "OK", "GOOD", "NOMINAL",..

Definition at line 122 of file MinHittingSetsFM.java.

Member Function Documentation

void hittingsetalg.MinHittingSetsFM.attemptPrune ( HSNodeFM node ) [inline, protected]

Definition at line 598 of file MinHittingSetsFM.java.

ConflictSet hittingsetalg.MinHittingSetsFM.callTheoremProver	(	SortedIntList	edgeLabels,
		ConflictSet	label
	)		`[inline, protected]`

Definition at line 411 of file MinHittingSetsFM.java.

boolean hittingsetalg.MinHittingSetsFM.canClose ( HSNodeFM node ) [inline, protected]

Definition at line 842 of file MinHittingSetsFM.java.

boolean hittingsetalg.MinHittingSetsFM.checkMinimalityHS ( ) [inline]

Definition at line 1001 of file MinHittingSetsFM.java.

int hittingsetalg.MinHittingSetsFM.compute	(	int	maxHSSize,
		int	maxNumMinHS
	)		`[inline]`

Definition at line 248 of file MinHittingSetsFM.java.

void hittingsetalg.MinHittingSetsFM.computeLabel ( HSNodeFM node ) [inline, protected]

Definition at line 784 of file MinHittingSetsFM.java.

int hittingsetalg.MinHittingSetsFM.computeMore	(	int	newMaxHSSize,
		int	newMaxNumMinHS
	)		`[inline]`

Definition at line 312 of file MinHittingSetsFM.java.

int hittingsetalg.MinHittingSetsFM.computeNumUnprunedChildren ( HSNodeFM node ) [inline, protected]

Definition at line 585 of file MinHittingSetsFM.java.

void hittingsetalg.MinHittingSetsFM.expandLastLevel	(	int	lastLevel,
		LinkedList	lastLevelNodes,
		LinkedList	newLevelNodes
	)		`[inline, protected]`

Definition at line 910 of file MinHittingSetsFM.java.

void hittingsetalg.MinHittingSetsFM.expandNode	(	HSNodeFM	node,
		LinkedList	newNodes,
		int	lastLevel
	)		`[inline, protected]`

Definition at line 942 of file MinHittingSetsFM.java.

ArrayList hittingsetalg.MinHittingSetsFM.getConflictsAsAss ( ) [inline]

Returns an ArrayList of ArrayList of Assumption: the conflict sets.

Each assumption is either a NAB or AB assumption.

Definition at line 214 of file MinHittingSetsFM.java.

ArrayList hittingsetalg.MinHittingSetsFM.getMinHS ( ) [inline]

Returns the computed min. hitting sets.

The return value is an ArrayList of ArrayList of Assumption (only "NAB"-assumptions, no "AB"-assumptions!).

Definition at line 183 of file MinHittingSetsFM.java.

boolean hittingsetalg.MinHittingSetsFM.nodeInvariant ( HSNodeFM node ) [inline, protected]

Definition at line 1025 of file MinHittingSetsFM.java.

void hittingsetalg.MinHittingSetsFM.processLastLevel	(	int	lastLevel,
		LinkedList	lastLevelNodes,
		LinkedList	newLevelNodes,
		boolean	expandNodes
	)		`[inline, protected]`