Class GraphImplementation

java.lang.Object
  |
  +--GraphImplementation
Direct Known Subclasses:
GraphImplementation1, GraphImplementation2
public class GraphImplementation
extends java.lang.Object
implements Graph_Implementor

This class models the reachability graph of a program. The reachability graph is a directed graph that contains all the states of the fault-span of a program. This class is the root of the abstract class hierarchy in the Bridge design pattern.

Since:
 

Constructor Summary
GraphImplementation(java.util.LinkedList inputs)
           
 
Method Summary
 void analyzeImp()
           
 boolean breakCycle(java.util.Hashtable ht)
           
 void closeDebugFile()
           
 boolean containsInvariantImp(java.util.Hashtable ht)
           
 boolean detectCycle(State s, java.util.Hashtable htb)
           
 boolean detectNonProgressCycle(State s, java.util.Hashtable htb)
           
 void dfs_detectCycle(State s, java.util.Hashtable ht)
           
 void emptyHashTable(java.util.Hashtable ht)
           
 void expandImp(Program p, Fault f)
           
 int getNumStates()
           
 State getState(State s)
           
 java.util.Hashtable getStates()
           
 void identify_msImp(SafetySpecification spec)
           
 void markInvariantStatesImp(Invariant inv)
           
 void printHashTable(java.util.Hashtable ht, java.lang.String str)
           
 java.util.Vector printImp(java.lang.String processIndex, java.lang.String actionName)
           
 void printInvariant()
           
 void printViolatingTransitions(SafetySpecification spec)
          This is a test method for debugging.
 void recomputeFaultSpanImp()
           
 boolean removeAnInvariantStateImp(State s)
           
 boolean removeAStateImp(State s)
           
 boolean removeFirstViolatingProgramTransitionImp(SafetySpecification spec)
           
 void removeViolatingProgramTransitionsImp(SafetySpecification spec)
           
 boolean scanAndSolveDeadlocksImp(Program pnew, Program pold, SafetySpecification spec, Invariant inv)
           
 void solveDeadlocksImp(Program pnew, Program pold, SafetySpecification spec, Invariant inv)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

GraphImplementation

public GraphImplementation(java.util.LinkedList inputs)
Method Detail

closeDebugFile

public void closeDebugFile()
Specified by:
closeDebugFile in interface Graph_Implementor

expandImp

public void expandImp(Program p,
                      Fault f)
Specified by:
expandImp in interface Graph_Implementor

identify_msImp

public void identify_msImp(SafetySpecification spec)
Specified by:
identify_msImp in interface Graph_Implementor

recomputeFaultSpanImp

public void recomputeFaultSpanImp()

removeViolatingProgramTransitionsImp

public void removeViolatingProgramTransitionsImp(SafetySpecification spec)
Specified by:
removeViolatingProgramTransitionsImp in interface Graph_Implementor

printViolatingTransitions

public void printViolatingTransitions(SafetySpecification spec)
This is a test method for debugging. We use this method to find program transitions that violate safety.

removeFirstViolatingProgramTransitionImp

public boolean removeFirstViolatingProgramTransitionImp(SafetySpecification spec)

markInvariantStatesImp

public void markInvariantStatesImp(Invariant inv)
Specified by:
markInvariantStatesImp in interface Graph_Implementor

solveDeadlocksImp

public void solveDeadlocksImp(Program pnew,
                              Program pold,
                              SafetySpecification spec,
                              Invariant inv)
Specified by:
solveDeadlocksImp in interface Graph_Implementor

scanAndSolveDeadlocksImp

public boolean scanAndSolveDeadlocksImp(Program pnew,
                                        Program pold,
                                        SafetySpecification spec,
                                        Invariant inv)

containsInvariantImp

public boolean containsInvariantImp(java.util.Hashtable ht)

removeAStateImp

public boolean removeAStateImp(State s)

removeAnInvariantStateImp

public boolean removeAnInvariantStateImp(State s)

printImp

public java.util.Vector printImp(java.lang.String processIndex,
                                 java.lang.String actionName)
Specified by:
printImp in interface Graph_Implementor

analyzeImp

public void analyzeImp()
Specified by:
analyzeImp in interface Graph_Implementor

getNumStates

public int getNumStates()
Specified by:
getNumStates in interface Graph_Implementor

getState

public State getState(State s)
Specified by:
getState in interface Graph_Implementor

getStates

public java.util.Hashtable getStates()

printInvariant

public void printInvariant()
Specified by:
printInvariant in interface Graph_Implementor

emptyHashTable

public void emptyHashTable(java.util.Hashtable ht)

detectNonProgressCycle

public boolean detectNonProgressCycle(State s,
                                      java.util.Hashtable htb)

detectCycle

public boolean detectCycle(State s,
                           java.util.Hashtable htb)

dfs_detectCycle

public void dfs_detectCycle(State s,
                            java.util.Hashtable ht)

breakCycle

public boolean breakCycle(java.util.Hashtable ht)

printHashTable

public void printHashTable(java.util.Hashtable ht,
                           java.lang.String str)